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 43292
Description: The union of a class of transitive sets is transitive. Alternate proof of truni 5281. truniALT 43292 is truniALTVD 43629 without virtual deductions and was automatically derived from truniALTVD 43629 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 485 . . . . . 6 ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴)
21a1i 11 . . . . 5 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴))
3 eluni 4911 . . . . 5 (𝑦 𝐴 ↔ ∃𝑞(𝑦𝑞𝑞𝐴))
42, 3imbitrdi 250 . . . 4 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ∃𝑞(𝑦𝑞𝑞𝐴)))
5 simpl 483 . . . . . . . . 9 ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦)
65a1i 11 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦))
7 simpl 483 . . . . . . . . 9 ((𝑦𝑞𝑞𝐴) → 𝑦𝑞)
872a1i 12 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑦𝑞)))
9 simpr 485 . . . . . . . . . 10 ((𝑦𝑞𝑞𝐴) → 𝑞𝐴)
1092a1i 12 . . . . . . . . 9 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑞𝐴)))
11 rspsbc 3873 . . . . . . . . . . 11 (𝑞𝐴 → (∀𝑥𝐴 Tr 𝑥[𝑞 / 𝑥]Tr 𝑥))
1211com12 32 . . . . . . . . . 10 (∀𝑥𝐴 Tr 𝑥 → (𝑞𝐴[𝑞 / 𝑥]Tr 𝑥))
1310, 12syl6d 75 . . . . . . . . 9 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → [𝑞 / 𝑥]Tr 𝑥)))
14 trsbc 43291 . . . . . . . . . 10 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
1514biimpd 228 . . . . . . . . 9 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
1610, 13, 15ee33 43272 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → Tr 𝑞)))
17 trel 5274 . . . . . . . . 9 (Tr 𝑞 → ((𝑧𝑦𝑦𝑞) → 𝑧𝑞))
1817expdcom 415 . . . . . . . 8 (𝑧𝑦 → (𝑦𝑞 → (Tr 𝑞𝑧𝑞)))
196, 8, 16, 18ee233 43270 . . . . . . 7 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑧𝑞)))
20 elunii 4913 . . . . . . . 8 ((𝑧𝑞𝑞𝐴) → 𝑧 𝐴)
2120ex 413 . . . . . . 7 (𝑧𝑞 → (𝑞𝐴𝑧 𝐴))
2219, 10, 21ee33 43272 . . . . . 6 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)))
2322alrimdv 1932 . . . . 5 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)))
24 19.23v 1945 . . . . 5 (∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴) ↔ (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴))
2523, 24imbitrdi 250 . . . 4 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴)))
264, 25mpdd 43 . . 3 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
2726alrimivv 1931 . 2 (∀𝑥𝐴 Tr 𝑥 → ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
28 dftr2 5267 . 2 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
2927, 28sylibr 233 1 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wal 1539  wex 1781  wcel 2106  wral 3061  [wsbc 3777   cuni 4908  Tr wtr 5265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-v 3476  df-sbc 3778  df-in 3955  df-ss 3965  df-uni 4909  df-tr 5266
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator