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 44459
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 44122 is truniALTVD 44459 without virtual deductions and was automatically derived from truniALTVD 44459.
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 44194 . . . . . . . 8 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑧𝑦𝑦 𝐴)   )
2 simpr 483 . . . . . . . 8 ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴)
31, 2e2 44212 . . . . . . 7 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑦 𝐴   )
4 eluni 4912 . . . . . . . 8 (𝑦 𝐴 ↔ ∃𝑞(𝑦𝑞𝑞𝐴))
54biimpi 215 . . . . . . 7 (𝑦 𝐴 → ∃𝑞(𝑦𝑞𝑞𝐴))
63, 5e2 44212 . . . . . 6 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞(𝑦𝑞𝑞𝐴)   )
7 simpl 481 . . . . . . . . . . . 12 ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦)
81, 7e2 44212 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧𝑦   )
9 idn3 44196 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   (𝑦𝑞𝑞𝐴)   )
10 simpl 481 . . . . . . . . . . . 12 ((𝑦𝑞𝑞𝐴) → 𝑦𝑞)
119, 10e3 44318 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   𝑦𝑞   )
12 simpr 483 . . . . . . . . . . . . 13 ((𝑦𝑞𝑞𝐴) → 𝑞𝐴)
139, 12e3 44318 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   𝑞𝐴   )
14 idn1 44155 . . . . . . . . . . . . 13 (   𝑥𝐴 Tr 𝑥   ▶   𝑥𝐴 Tr 𝑥   )
15 rspsbc 3869 . . . . . . . . . . . . . 14 (𝑞𝐴 → (∀𝑥𝐴 Tr 𝑥[𝑞 / 𝑥]Tr 𝑥))
1615com12 32 . . . . . . . . . . . . 13 (∀𝑥𝐴 Tr 𝑥 → (𝑞𝐴[𝑞 / 𝑥]Tr 𝑥))
1714, 13, 16e13 44329 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   [𝑞 / 𝑥]Tr 𝑥   )
18 trsbc 44121 . . . . . . . . . . . . 13 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
1918biimpd 228 . . . . . . . . . . . 12 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
2013, 17, 19e33 44315 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   Tr 𝑞   )
21 trel 5275 . . . . . . . . . . . 12 (Tr 𝑞 → ((𝑧𝑦𝑦𝑞) → 𝑧𝑞))
2221expdcom 413 . . . . . . . . . . 11 (𝑧𝑦 → (𝑦𝑞 → (Tr 𝑞𝑧𝑞)))
238, 11, 20, 22e233 44346 . . . . . . . . . 10 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   𝑧𝑞   )
24 elunii 4914 . . . . . . . . . . 11 ((𝑧𝑞𝑞𝐴) → 𝑧 𝐴)
2524ex 411 . . . . . . . . . 10 (𝑧𝑞 → (𝑞𝐴𝑧 𝐴))
2623, 13, 25e33 44315 . . . . . . . . 9 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   𝑧 𝐴   )
2726in3 44190 . . . . . . . 8 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   ((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
2827gen21 44200 . . . . . . 7 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
29 19.23v 1937 . . . . . . . 8 (∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴) ↔ (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴))
3029biimpi 215 . . . . . . 7 (∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴) → (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴))
3128, 30e2 44212 . . . . . 6 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
32 pm2.27 42 . . . . . 6 (∃𝑞(𝑦𝑞𝑞𝐴) → ((∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴) → 𝑧 𝐴))
336, 31, 32e22 44252 . . . . 5 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧 𝐴   )
3433in2 44186 . . . 4 (   𝑥𝐴 Tr 𝑥   ▶   ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
3534gen12 44199 . . 3 (   𝑥𝐴 Tr 𝑥   ▶   𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
36 dftr2 5268 . . . 4 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
3736biimpri 227 . . 3 (∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴) → Tr 𝐴)
3835, 37e1a 44208 . 2 (   𝑥𝐴 Tr 𝑥   ▶   Tr 𝐴   )
3938in1 44152 1 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wal 1531  wex 1773  wcel 2098  wral 3050  [wsbc 3773   cuni 4909  Tr wtr 5266
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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-v 3463  df-sbc 3774  df-ss 3961  df-uni 4910  df-tr 5267  df-vd1 44151  df-vd2 44159  df-vd3 44171
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator