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 43941
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 43604 is truniALTVD 43941 without virtual deductions and was automatically derived from truniALTVD 43941.
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 43676 . . . . . . . 8 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑧𝑦𝑦 𝐴)   )
2 simpr 483 . . . . . . . 8 ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴)
31, 2e2 43694 . . . . . . 7 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑦 𝐴   )
4 eluni 4910 . . . . . . . 8 (𝑦 𝐴 ↔ ∃𝑞(𝑦𝑞𝑞𝐴))
54biimpi 215 . . . . . . 7 (𝑦 𝐴 → ∃𝑞(𝑦𝑞𝑞𝐴))
63, 5e2 43694 . . . . . 6 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞(𝑦𝑞𝑞𝐴)   )
7 simpl 481 . . . . . . . . . . . 12 ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦)
81, 7e2 43694 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧𝑦   )
9 idn3 43678 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   (𝑦𝑞𝑞𝐴)   )
10 simpl 481 . . . . . . . . . . . 12 ((𝑦𝑞𝑞𝐴) → 𝑦𝑞)
119, 10e3 43800 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   𝑦𝑞   )
12 simpr 483 . . . . . . . . . . . . 13 ((𝑦𝑞𝑞𝐴) → 𝑞𝐴)
139, 12e3 43800 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   𝑞𝐴   )
14 idn1 43637 . . . . . . . . . . . . 13 (   𝑥𝐴 Tr 𝑥   ▶   𝑥𝐴 Tr 𝑥   )
15 rspsbc 3872 . . . . . . . . . . . . . 14 (𝑞𝐴 → (∀𝑥𝐴 Tr 𝑥[𝑞 / 𝑥]Tr 𝑥))
1615com12 32 . . . . . . . . . . . . 13 (∀𝑥𝐴 Tr 𝑥 → (𝑞𝐴[𝑞 / 𝑥]Tr 𝑥))
1714, 13, 16e13 43811 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   [𝑞 / 𝑥]Tr 𝑥   )
18 trsbc 43603 . . . . . . . . . . . . 13 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
1918biimpd 228 . . . . . . . . . . . 12 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
2013, 17, 19e33 43797 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   Tr 𝑞   )
21 trel 5273 . . . . . . . . . . . 12 (Tr 𝑞 → ((𝑧𝑦𝑦𝑞) → 𝑧𝑞))
2221expdcom 413 . . . . . . . . . . 11 (𝑧𝑦 → (𝑦𝑞 → (Tr 𝑞𝑧𝑞)))
238, 11, 20, 22e233 43828 . . . . . . . . . 10 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   𝑧𝑞   )
24 elunii 4912 . . . . . . . . . . 11 ((𝑧𝑞𝑞𝐴) → 𝑧 𝐴)
2524ex 411 . . . . . . . . . 10 (𝑧𝑞 → (𝑞𝐴𝑧 𝐴))
2623, 13, 25e33 43797 . . . . . . . . 9 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   (𝑦𝑞𝑞𝐴)   ▶   𝑧 𝐴   )
2726in3 43672 . . . . . . . 8 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   ((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
2827gen21 43682 . . . . . . 7 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
29 19.23v 1943 . . . . . . . 8 (∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴) ↔ (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴))
3029biimpi 215 . . . . . . 7 (∀𝑞((𝑦𝑞𝑞𝐴) → 𝑧 𝐴) → (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴))
3128, 30e2 43694 . . . . . 6 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴)   )
32 pm2.27 42 . . . . . 6 (∃𝑞(𝑦𝑞𝑞𝐴) → ((∃𝑞(𝑦𝑞𝑞𝐴) → 𝑧 𝐴) → 𝑧 𝐴))
336, 31, 32e22 43734 . . . . 5 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧 𝐴   )
3433in2 43668 . . . 4 (   𝑥𝐴 Tr 𝑥   ▶   ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
3534gen12 43681 . . 3 (   𝑥𝐴 Tr 𝑥   ▶   𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
36 dftr2 5266 . . . 4 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
3736biimpri 227 . . 3 (∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴) → Tr 𝐴)
3835, 37e1a 43690 . 2 (   𝑥𝐴 Tr 𝑥   ▶   Tr 𝐴   )
3938in1 43634 1 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wal 1537  wex 1779  wcel 2104  wral 3059  [wsbc 3776   cuni 4907  Tr wtr 5264
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-v 3474  df-sbc 3777  df-in 3954  df-ss 3964  df-uni 4908  df-tr 5265  df-vd1 43633  df-vd2 43641  df-vd3 43653
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator