Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  truniALT Structured version   Visualization version   GIF version

Theorem truniALT 39068
Description: The union of a class of transitive sets is transitive. Alternate proof of truni 4800. truniALT 39068 is truniALTVD 39428 without virtual deductions and was automatically derived from truniALTVD 39428 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
truniALT (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem truniALT
Dummy variables 𝑞 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 476 . . . . . 6 ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴)
21a1i 11 . . . . 5 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴))
3 eluni 4471 . . . . 5 (𝑦 𝐴 ↔ ∃𝑞(𝑦𝑞𝑞𝐴))
42, 3syl6ib 241 . . . 4 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ∃𝑞(𝑦𝑞𝑞𝐴)))
5 simpl 472 . . . . . . . . 9 ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦)
65a1i 11 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦))
7 simpl 472 . . . . . . . . 9 ((𝑦𝑞𝑞𝐴) → 𝑦𝑞)
872a1i 12 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑦𝑞)))
9 simpr 476 . . . . . . . . . 10 ((𝑦𝑞𝑞𝐴) → 𝑞𝐴)
1092a1i 12 . . . . . . . . 9 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑞𝐴)))
11 rspsbc 3551 . . . . . . . . . . 11 (𝑞𝐴 → (∀𝑥𝐴 Tr 𝑥[𝑞 / 𝑥]Tr 𝑥))
1211com12 32 . . . . . . . . . 10 (∀𝑥𝐴 Tr 𝑥 → (𝑞𝐴[𝑞 / 𝑥]Tr 𝑥))
1310, 12syl6d 75 . . . . . . . . 9 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → [𝑞 / 𝑥]Tr 𝑥)))
14 trsbc 39067 . . . . . . . . . 10 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
1514biimpd 219 . . . . . . . . 9 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
1610, 13, 15ee33 39044 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → Tr 𝑞)))
17 trel 4792 . . . . . . . . 9 (Tr 𝑞 → ((𝑧𝑦𝑦𝑞) → 𝑧𝑞))
1817expdcom 454 . . . . . . . 8 (𝑧𝑦 → (𝑦𝑞 → (Tr 𝑞𝑧𝑞)))
196, 8, 16, 18ee233 39042 . . . . . . 7 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑧𝑞)))
20 elunii 4473 . . . . . . . 8 ((𝑧𝑞𝑞𝐴) → 𝑧 𝐴)
2120ex 449 . . . . . . 7 (𝑧𝑞 → (𝑞𝐴𝑧 𝐴))
2219, 10, 21ee33 39044 . . . . . 6 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)))
2322alrimdv 1897 . . . . 5 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)))
24 19.23v 1911 . . . . 5 (∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴) ↔ (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴))
2523, 24syl6ib 241 . . . 4 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴)))
264, 25mpdd 43 . . 3 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
2726alrimivv 1896 . 2 (∀𝑥𝐴 Tr 𝑥 → ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
28 dftr2 4787 . 2 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
2927, 28sylibr 224 1 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wal 1521  wex 1744  wcel 2030  wral 2941  [wsbc 3468   cuni 4468  Tr wtr 4785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-v 3233  df-sbc 3469  df-in 3614  df-ss 3621  df-uni 4469  df-tr 4786
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator