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 40740
Description: The union of a class of transitive sets is transitive. Alternate proof of truni 5183. truniALT 40740 is truniALTVD 41077 without virtual deductions and was automatically derived from truniALTVD 41077 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 4840 . . . . 5 (𝑦 𝐴 ↔ ∃𝑞(𝑦𝑞𝑞𝐴))
42, 3syl6ib 252 . . . 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 3866 . . . . . . . . . . 11 (𝑞𝐴 → (∀𝑥𝐴 Tr 𝑥[𝑞 / 𝑥]Tr 𝑥))
1211com12 32 . . . . . . . . . 10 (∀𝑥𝐴 Tr 𝑥 → (𝑞𝐴[𝑞 / 𝑥]Tr 𝑥))
1310, 12syl6d 75 . . . . . . . . 9 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → [𝑞 / 𝑥]Tr 𝑥)))
14 trsbc 40739 . . . . . . . . . 10 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
1514biimpd 230 . . . . . . . . 9 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
1610, 13, 15ee33 40720 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → Tr 𝑞)))
17 trel 5176 . . . . . . . . 9 (Tr 𝑞 → ((𝑧𝑦𝑦𝑞) → 𝑧𝑞))
1817expdcom 415 . . . . . . . 8 (𝑧𝑦 → (𝑦𝑞 → (Tr 𝑞𝑧𝑞)))
196, 8, 16, 18ee233 40718 . . . . . . 7 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑧𝑞)))
20 elunii 4842 . . . . . . . 8 ((𝑧𝑞𝑞𝐴) → 𝑧 𝐴)
2120ex 413 . . . . . . 7 (𝑧𝑞 → (𝑞𝐴𝑧 𝐴))
2219, 10, 21ee33 40720 . . . . . 6 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)))
2322alrimdv 1923 . . . . 5 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)))
24 19.23v 1936 . . . . 5 (∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴) ↔ (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴))
2523, 24syl6ib 252 . . . 4 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴)))
264, 25mpdd 43 . . 3 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
2726alrimivv 1922 . 2 (∀𝑥𝐴 Tr 𝑥 → ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
28 dftr2 5171 . 2 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
2927, 28sylibr 235 1 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wal 1528  wex 1773  wcel 2107  wral 3143  [wsbc 3776   cuni 4837  Tr wtr 5169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-v 3502  df-sbc 3777  df-in 3947  df-ss 3956  df-uni 4838  df-tr 5170
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator