Mathbox for Rodolfo Medina < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  prtlem14 Structured version   Visualization version   GIF version

Theorem prtlem14 33978
 Description: Lemma for prter1 33983, prter2 33985 and prtex 33984. (Contributed by Rodolfo Medina, 13-Oct-2010.)
Assertion
Ref Expression
prtlem14 (Prt 𝐴 → ((𝑥𝐴𝑦𝐴) → ((𝑤𝑥𝑤𝑦) → 𝑥 = 𝑦)))
Distinct variable groups:   𝑥,𝑤,𝑦   𝑥,𝐴,𝑦
Allowed substitution hint:   𝐴(𝑤)

Proof of Theorem prtlem14
StepHypRef Expression
1 df-prt 33976 . . 3 (Prt 𝐴 ↔ ∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝑥𝑦) = ∅))
2 rsp2 2933 . . 3 (∀𝑥𝐴𝑦𝐴 (𝑥 = 𝑦 ∨ (𝑥𝑦) = ∅) → ((𝑥𝐴𝑦𝐴) → (𝑥 = 𝑦 ∨ (𝑥𝑦) = ∅)))
31, 2sylbi 207 . 2 (Prt 𝐴 → ((𝑥𝐴𝑦𝐴) → (𝑥 = 𝑦 ∨ (𝑥𝑦) = ∅)))
4 elin 3788 . . . 4 (𝑤 ∈ (𝑥𝑦) ↔ (𝑤𝑥𝑤𝑦))
5 eq0 3921 . . . . . 6 ((𝑥𝑦) = ∅ ↔ ∀𝑤 ¬ 𝑤 ∈ (𝑥𝑦))
6 sp 2051 . . . . . 6 (∀𝑤 ¬ 𝑤 ∈ (𝑥𝑦) → ¬ 𝑤 ∈ (𝑥𝑦))
75, 6sylbi 207 . . . . 5 ((𝑥𝑦) = ∅ → ¬ 𝑤 ∈ (𝑥𝑦))
87pm2.21d 118 . . . 4 ((𝑥𝑦) = ∅ → (𝑤 ∈ (𝑥𝑦) → 𝑥 = 𝑦))
94, 8syl5bir 233 . . 3 ((𝑥𝑦) = ∅ → ((𝑤𝑥𝑤𝑦) → 𝑥 = 𝑦))
109jao1i 824 . 2 ((𝑥 = 𝑦 ∨ (𝑥𝑦) = ∅) → ((𝑤𝑥𝑤𝑦) → 𝑥 = 𝑦))
113, 10syl6 35 1 (Prt 𝐴 → ((𝑥𝐴𝑦𝐴) → ((𝑤𝑥𝑤𝑦) → 𝑥 = 𝑦)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 383   ∧ wa 384  ∀wal 1479   = wceq 1481   ∈ wcel 1988  ∀wral 2909   ∩ cin 3566  ∅c0 3907  Prt wprt 33975 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-v 3197  df-dif 3570  df-in 3574  df-nul 3908  df-prt 33976 This theorem is referenced by:  prtlem15  33979  prtlem17  33980
 Copyright terms: Public domain W3C validator