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 39609
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 39249 is truniALTVD 39609 without virtual deductions and was automatically derived from truniALTVD 39609.
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 39336 . . . . . . . 8 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑧𝑦𝑦 𝐴)   )
2 simpr 479 . . . . . . . 8 ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴)
31, 2e2 39354 . . . . . . 7 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑦 𝐴   )
4 eluni 4587 . . . . . . . 8 (𝑦 𝐴 ↔ ∃𝑞(𝑦𝑞𝑞𝐴))
54biimpi 206 . . . . . . 7 (𝑦 𝐴 → ∃𝑞(𝑦𝑞𝑞𝐴))
63, 5e2 39354 . . . . . 6 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞(𝑦𝑞𝑞𝐴)   )
7 simpl 474 . . . . . . . . . . . 12 ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦)
81, 7e2 39354 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧𝑦   )
9 idn3 39338 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   (𝑦𝑞𝑞𝐴)   )
10 simpl 474 . . . . . . . . . . . 12 ((𝑦𝑞𝑞𝐴) → 𝑦𝑞)
119, 10e3 39462 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   𝑦𝑞   )
12 simpr 479 . . . . . . . . . . . . 13 ((𝑦𝑞𝑞𝐴) → 𝑞𝐴)
139, 12e3 39462 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   𝑞𝐴   )
14 idn1 39288 . . . . . . . . . . . . 13 (   𝑥𝐴 Tr 𝑥   ▶   𝑥𝐴 Tr 𝑥   )
15 rspsbc 3655 . . . . . . . . . . . . . 14 (𝑞𝐴 → (∀𝑥𝐴 Tr 𝑥[𝑞 / 𝑥]Tr 𝑥))
1615com12 32 . . . . . . . . . . . . 13 (∀𝑥𝐴 Tr 𝑥 → (𝑞𝐴[𝑞 / 𝑥]Tr 𝑥))
1714, 13, 16e13 39473 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   [𝑞 / 𝑥]Tr 𝑥   )
18 trsbc 39248 . . . . . . . . . . . . 13 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
1918biimpd 219 . . . . . . . . . . . 12 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
2013, 17, 19e33 39459 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   Tr 𝑞   )
21 trel 4907 . . . . . . . . . . . 12 (Tr 𝑞 → ((𝑧𝑦𝑦𝑞) → 𝑧𝑞))
2221expdcom 454 . . . . . . . . . . 11 (𝑧𝑦 → (𝑦𝑞 → (Tr 𝑞𝑧𝑞)))
238, 11, 20, 22e233 39490 . . . . . . . . . 10 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   𝑧𝑞   )
24 elunii 4589 . . . . . . . . . . 11 ((𝑧𝑞𝑞𝐴) → 𝑧 𝐴)
2524ex 449 . . . . . . . . . 10 (𝑧𝑞 → (𝑞𝐴𝑧 𝐴))
2623, 13, 25e33 39459 . . . . . . . . 9 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   𝑧 𝐴   )
2726in3 39332 . . . . . . . 8 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   ((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
2827gen21 39342 . . . . . . 7 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
29 19.23v 2016 . . . . . . . 8 (∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴) ↔ (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴))
3029biimpi 206 . . . . . . 7 (∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴) → (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴))
3128, 30e2 39354 . . . . . 6 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
32 pm2.27 42 . . . . . 6 (∃𝑞(𝑦𝑞𝑞𝐴) → ((∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴) → 𝑧 𝐴))
336, 31, 32e22 39394 . . . . 5 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧 𝐴   )
3433in2 39328 . . . 4 (   𝑥𝐴 Tr 𝑥   ▶   ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
3534gen12 39341 . . 3 (   𝑥𝐴 Tr 𝑥   ▶   𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
36 dftr2 4902 . . . 4 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
3736biimpri 218 . . 3 (∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴) → Tr 𝐴)
3835, 37e1a 39350 . 2 (   𝑥𝐴 Tr 𝑥   ▶   Tr 𝐴   )
3938in1 39285 1 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wal 1626  wex 1849  wcel 2135  wral 3046  [wsbc 3572   cuni 4584  Tr wtr 4900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ral 3051  df-v 3338  df-sbc 3573  df-in 3718  df-ss 3725  df-uni 4585  df-tr 4901  df-vd1 39284  df-vd2 39292  df-vd3 39304
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator