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 39245
Description: The union of a class of transitive sets is transitive. Alternate proof of truni 4911. truniALT 39245 is truniALTVD 39605 without virtual deductions and was automatically derived from truniALTVD 39605 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 479 . . . . . 6 ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴)
21a1i 11 . . . . 5 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴))
3 eluni 4583 . . . . 5 (𝑦 𝐴 ↔ ∃𝑞(𝑦𝑞𝑞𝐴))
42, 3syl6ib 241 . . . 4 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ∃𝑞(𝑦𝑞𝑞𝐴)))
5 simpl 474 . . . . . . . . 9 ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦)
65a1i 11 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦))
7 simpl 474 . . . . . . . . 9 ((𝑦𝑞𝑞𝐴) → 𝑦𝑞)
872a1i 12 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑦𝑞)))
9 simpr 479 . . . . . . . . . 10 ((𝑦𝑞𝑞𝐴) → 𝑞𝐴)
1092a1i 12 . . . . . . . . 9 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑞𝐴)))
11 rspsbc 3651 . . . . . . . . . . 11 (𝑞𝐴 → (∀𝑥𝐴 Tr 𝑥[𝑞 / 𝑥]Tr 𝑥))
1211com12 32 . . . . . . . . . 10 (∀𝑥𝐴 Tr 𝑥 → (𝑞𝐴[𝑞 / 𝑥]Tr 𝑥))
1310, 12syl6d 75 . . . . . . . . 9 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → [𝑞 / 𝑥]Tr 𝑥)))
14 trsbc 39244 . . . . . . . . . 10 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
1514biimpd 219 . . . . . . . . 9 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
1610, 13, 15ee33 39221 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → Tr 𝑞)))
17 trel 4903 . . . . . . . . 9 (Tr 𝑞 → ((𝑧𝑦𝑦𝑞) → 𝑧𝑞))
1817expdcom 454 . . . . . . . 8 (𝑧𝑦 → (𝑦𝑞 → (Tr 𝑞𝑧𝑞)))
196, 8, 16, 18ee233 39219 . . . . . . 7 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑧𝑞)))
20 elunii 4585 . . . . . . . 8 ((𝑧𝑞𝑞𝐴) → 𝑧 𝐴)
2120ex 449 . . . . . . 7 (𝑧𝑞 → (𝑞𝐴𝑧 𝐴))
2219, 10, 21ee33 39221 . . . . . 6 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)))
2322alrimdv 1998 . . . . 5 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)))
24 19.23v 2012 . . . . 5 (∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴) ↔ (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴))
2523, 24syl6ib 241 . . . 4 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴)))
264, 25mpdd 43 . . 3 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
2726alrimivv 1997 . 2 (∀𝑥𝐴 Tr 𝑥 → ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
28 dftr2 4898 . 2 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
2927, 28sylibr 224 1 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wal 1622  wex 1845  wcel 2131  wral 3042  [wsbc 3568   cuni 4580  Tr wtr 4896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-v 3334  df-sbc 3569  df-in 3714  df-ss 3721  df-uni 4581  df-tr 4897
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator