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

Theorem truniALTVD 44898
Description: The union of a class of transitive sets is transitive. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. truniALT 44561 is truniALTVD 44898 without virtual deductions and was automatically derived from truniALTVD 44898.
1:: (   𝑥𝐴Tr 𝑥   ▶   𝑥𝐴 Tr 𝑥   )
2:: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴)   ▶   (𝑧𝑦𝑦 𝐴)   )
3:2: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴)   ▶   𝑧𝑦   )
4:2: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴)   ▶   𝑦 𝐴   )
5:4: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴)   ▶   𝑞(𝑦𝑞𝑞𝐴)   )
6:: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴), (𝑦𝑞𝑞𝐴)   ▶   (𝑦𝑞𝑞𝐴)   )
7:6: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴), (𝑦𝑞𝑞𝐴)   ▶   𝑦𝑞   )
8:6: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴), (𝑦𝑞𝑞𝐴)   ▶   𝑞𝐴   )
9:1,8: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴), (𝑦𝑞𝑞𝐴)   ▶   [𝑞 / 𝑥]Tr 𝑥   )
10:8,9: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴), (𝑦𝑞𝑞𝐴)   ▶   Tr 𝑞   )
11:3,7,10: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴), (𝑦𝑞𝑞𝐴)   ▶   𝑧𝑞   )
12:11,8: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴), (𝑦𝑞𝑞𝐴)   ▶   𝑧 𝐴   )
13:12: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴)   ▶   ((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
14:13: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴)   ▶   𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
15:14: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴)   ▶   (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
16:5,15: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦 𝑦 𝐴)   ▶   𝑧 𝐴   )
17:16: (   𝑥𝐴Tr 𝑥   ▶   ((𝑧𝑦 𝑦 𝐴) → 𝑧 𝐴)   )
18:17: (   𝑥𝐴Tr 𝑥    ▶   𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
19:18: (   𝑥𝐴Tr 𝑥   ▶   Tr 𝐴   )
qed:19: (∀𝑥𝐴Tr 𝑥 → Tr 𝐴)
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
truniALTVD (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem truniALTVD
Dummy variables 𝑞 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idn2 44633 . . . . . . . 8 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑧𝑦𝑦 𝐴)   )
2 simpr 484 . . . . . . . 8 ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴)
31, 2e2 44651 . . . . . . 7 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑦 𝐴   )
4 eluni 4910 . . . . . . . 8 (𝑦 𝐴 ↔ ∃𝑞(𝑦𝑞𝑞𝐴))
54biimpi 216 . . . . . . 7 (𝑦 𝐴 → ∃𝑞(𝑦𝑞𝑞𝐴))
63, 5e2 44651 . . . . . 6 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞(𝑦𝑞𝑞𝐴)   )
7 simpl 482 . . . . . . . . . . . 12 ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦)
81, 7e2 44651 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧𝑦   )
9 idn3 44635 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   (𝑦𝑞𝑞𝐴)   )
10 simpl 482 . . . . . . . . . . . 12 ((𝑦𝑞𝑞𝐴) → 𝑦𝑞)
119, 10e3 44757 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   𝑦𝑞   )
12 simpr 484 . . . . . . . . . . . . 13 ((𝑦𝑞𝑞𝐴) → 𝑞𝐴)
139, 12e3 44757 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   𝑞𝐴   )
14 idn1 44594 . . . . . . . . . . . . 13 (   𝑥𝐴 Tr 𝑥   ▶   𝑥𝐴 Tr 𝑥   )
15 rspsbc 3879 . . . . . . . . . . . . . 14 (𝑞𝐴 → (∀𝑥𝐴 Tr 𝑥[𝑞 / 𝑥]Tr 𝑥))
1615com12 32 . . . . . . . . . . . . 13 (∀𝑥𝐴 Tr 𝑥 → (𝑞𝐴[𝑞 / 𝑥]Tr 𝑥))
1714, 13, 16e13 44768 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   [𝑞 / 𝑥]Tr 𝑥   )
18 trsbc 44560 . . . . . . . . . . . . 13 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
1918biimpd 229 . . . . . . . . . . . 12 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
2013, 17, 19e33 44754 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   Tr 𝑞   )
21 trel 5268 . . . . . . . . . . . 12 (Tr 𝑞 → ((𝑧𝑦𝑦𝑞) → 𝑧𝑞))
2221expdcom 414 . . . . . . . . . . 11 (𝑧𝑦 → (𝑦𝑞 → (Tr 𝑞𝑧𝑞)))
238, 11, 20, 22e233 44785 . . . . . . . . . 10 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   𝑧𝑞   )
24 elunii 4912 . . . . . . . . . . 11 ((𝑧𝑞𝑞𝐴) → 𝑧 𝐴)
2524ex 412 . . . . . . . . . 10 (𝑧𝑞 → (𝑞𝐴𝑧 𝐴))
2623, 13, 25e33 44754 . . . . . . . . 9 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   𝑧 𝐴   )
2726in3 44629 . . . . . . . 8 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   ((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
2827gen21 44639 . . . . . . 7 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
29 19.23v 1942 . . . . . . . 8 (∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴) ↔ (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴))
3029biimpi 216 . . . . . . 7 (∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴) → (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴))
3128, 30e2 44651 . . . . . 6 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
32 pm2.27 42 . . . . . 6 (∃𝑞(𝑦𝑞𝑞𝐴) → ((∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴) → 𝑧 𝐴))
336, 31, 32e22 44691 . . . . 5 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧 𝐴   )
3433in2 44625 . . . 4 (   𝑥𝐴 Tr 𝑥   ▶   ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
3534gen12 44638 . . 3 (   𝑥𝐴 Tr 𝑥   ▶   𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
36 dftr2 5261 . . . 4 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
3736biimpri 228 . . 3 (∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴) → Tr 𝐴)
3835, 37e1a 44647 . 2 (   𝑥𝐴 Tr 𝑥   ▶   Tr 𝐴   )
3938in1 44591 1 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wal 1538  wex 1779  wcel 2108  wral 3061  [wsbc 3788   cuni 4907  Tr wtr 5259
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-sbc 3789  df-ss 3968  df-uni 4908  df-tr 5260  df-vd1 44590  df-vd2 44598  df-vd3 44610
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator