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 39351
Description: The union of a class of transitive sets is transitive. Alternate proof of truni 4925. truniALT 39351 is truniALTVD 39698 without virtual deductions and was automatically derived from truniALTVD 39698 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 477 . . . . . 6 ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴)
21a1i 11 . . . . 5 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴))
3 eluni 4597 . . . . 5 (𝑦 𝐴 ↔ ∃𝑞(𝑦𝑞𝑞𝐴))
42, 3syl6ib 242 . . . 4 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ∃𝑞(𝑦𝑞𝑞𝐴)))
5 simpl 474 . . . . . . . . 9 ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦)
65a1i 11 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦))
7 simpl 474 . . . . . . . . 9 ((𝑦𝑞𝑞𝐴) → 𝑦𝑞)
872a1i 12 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑦𝑞)))
9 simpr 477 . . . . . . . . . 10 ((𝑦𝑞𝑞𝐴) → 𝑞𝐴)
1092a1i 12 . . . . . . . . 9 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑞𝐴)))
11 rspsbc 3676 . . . . . . . . . . 11 (𝑞𝐴 → (∀𝑥𝐴 Tr 𝑥[𝑞 / 𝑥]Tr 𝑥))
1211com12 32 . . . . . . . . . 10 (∀𝑥𝐴 Tr 𝑥 → (𝑞𝐴[𝑞 / 𝑥]Tr 𝑥))
1310, 12syl6d 75 . . . . . . . . 9 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → [𝑞 / 𝑥]Tr 𝑥)))
14 trsbc 39350 . . . . . . . . . 10 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
1514biimpd 220 . . . . . . . . 9 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
1610, 13, 15ee33 39331 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → Tr 𝑞)))
17 trel 4918 . . . . . . . . 9 (Tr 𝑞 → ((𝑧𝑦𝑦𝑞) → 𝑧𝑞))
1817expdcom 403 . . . . . . . 8 (𝑧𝑦 → (𝑦𝑞 → (Tr 𝑞𝑧𝑞)))
196, 8, 16, 18ee233 39329 . . . . . . 7 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑧𝑞)))
20 elunii 4599 . . . . . . . 8 ((𝑧𝑞𝑞𝐴) → 𝑧 𝐴)
2120ex 401 . . . . . . 7 (𝑧𝑞 → (𝑞𝐴𝑧 𝐴))
2219, 10, 21ee33 39331 . . . . . 6 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)))
2322alrimdv 2024 . . . . 5 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)))
24 19.23v 2037 . . . . 5 (∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴) ↔ (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴))
2523, 24syl6ib 242 . . . 4 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴)))
264, 25mpdd 43 . . 3 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
2726alrimivv 2023 . 2 (∀𝑥𝐴 Tr 𝑥 → ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
28 dftr2 4913 . 2 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
2927, 28sylibr 225 1 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wal 1650  wex 1874  wcel 2155  wral 3055  [wsbc 3596   cuni 4594  Tr wtr 4911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-v 3352  df-sbc 3597  df-in 3739  df-ss 3746  df-uni 4595  df-tr 4912
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator