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

Theorem trintALTVD 38638
Description: The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT 38639. 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. trintALT 38639 is trintALTVD 38638 without virtual deductions and was automatically derived from trintALTVD 38638.
1:: (   𝑥𝐴Tr 𝑥   ▶   𝑥𝐴Tr 𝑥   )
2:: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑧𝑦𝑦 𝐴)   )
3:2: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧𝑦   )
4:2: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑦 𝐴   )
5:4: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞𝐴𝑦𝑞   )
6:5: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑞𝐴𝑦𝑞)   )
7:: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴), 𝑞𝐴   ▶   𝑞𝐴   )
8:7,6: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴), 𝑞𝐴   ▶   𝑦𝑞   )
9:7,1: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴), 𝑞𝐴   ▶   [𝑞 / 𝑥]Tr 𝑥   )
10:7,9: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴), 𝑞𝐴   ▶   Tr 𝑞   )
11:10,3,8: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴), 𝑞𝐴   ▶   𝑧𝑞   )
12:11: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑞𝐴𝑧𝑞)   )
13:12: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞(𝑞𝐴𝑧𝑞)   )
14:13: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞𝐴𝑧𝑞   )
15:3,14: (   𝑥𝐴Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧 𝐴   )
16:15: (   𝑥𝐴Tr 𝑥   ▶   ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
17:16: (   𝑥𝐴Tr 𝑥   ▶   𝑧𝑦((𝑧 𝑦𝑦 𝐴) → 𝑧 𝐴)   )
18:17: (   𝑥𝐴Tr 𝑥   ▶   Tr 𝐴   )
qed:18: (∀𝑥𝐴Tr 𝑥 → Tr 𝐴)
(Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
trintALTVD (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem trintALTVD
Dummy variables 𝑞 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idn2 38359 . . . . . . 7 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑧𝑦𝑦 𝐴)   )
2 simpl 473 . . . . . . 7 ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦)
31, 2e2 38377 . . . . . 6 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧𝑦   )
4 idn3 38361 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   𝑞𝐴   )
5 idn1 38311 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ▶   𝑥𝐴 Tr 𝑥   )
6 rspsbc 3504 . . . . . . . . . . . 12 (𝑞𝐴 → (∀𝑥𝐴 Tr 𝑥[𝑞 / 𝑥]Tr 𝑥))
74, 5, 6e31 38499 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   [𝑞 / 𝑥]Tr 𝑥   )
8 trsbc 38271 . . . . . . . . . . . 12 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
98biimpd 219 . . . . . . . . . . 11 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
104, 7, 9e33 38482 . . . . . . . . . 10 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   Tr 𝑞   )
11 simpr 477 . . . . . . . . . . . . . 14 ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴)
121, 11e2 38377 . . . . . . . . . . . . 13 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑦 𝐴   )
13 elintg 4455 . . . . . . . . . . . . . 14 (𝑦 𝐴 → (𝑦 𝐴 ↔ ∀𝑞𝐴 𝑦𝑞))
1413ibi 256 . . . . . . . . . . . . 13 (𝑦 𝐴 → ∀𝑞𝐴 𝑦𝑞)
1512, 14e2 38377 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞𝐴 𝑦𝑞   )
16 rsp 2925 . . . . . . . . . . . 12 (∀𝑞𝐴 𝑦𝑞 → (𝑞𝐴𝑦𝑞))
1715, 16e2 38377 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑞𝐴𝑦𝑞)   )
18 pm2.27 42 . . . . . . . . . . 11 (𝑞𝐴 → ((𝑞𝐴𝑦𝑞) → 𝑦𝑞))
194, 17, 18e32 38506 . . . . . . . . . 10 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   𝑦𝑞   )
20 trel 4729 . . . . . . . . . . 11 (Tr 𝑞 → ((𝑧𝑦𝑦𝑞) → 𝑧𝑞))
2120expd 452 . . . . . . . . . 10 (Tr 𝑞 → (𝑧𝑦 → (𝑦𝑞𝑧𝑞)))
2210, 3, 19, 21e323 38514 . . . . . . . . 9 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   𝑧𝑞   )
2322in3 38355 . . . . . . . 8 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑞𝐴𝑧𝑞)   )
2423gen21 38365 . . . . . . 7 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞(𝑞𝐴𝑧𝑞)   )
25 df-ral 2913 . . . . . . . 8 (∀𝑞𝐴 𝑧𝑞 ↔ ∀𝑞(𝑞𝐴𝑧𝑞))
2625biimpri 218 . . . . . . 7 (∀𝑞(𝑞𝐴𝑧𝑞) → ∀𝑞𝐴 𝑧𝑞)
2724, 26e2 38377 . . . . . 6 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞𝐴 𝑧𝑞   )
28 elintg 4455 . . . . . . 7 (𝑧𝑦 → (𝑧 𝐴 ↔ ∀𝑞𝐴 𝑧𝑞))
2928biimprd 238 . . . . . 6 (𝑧𝑦 → (∀𝑞𝐴 𝑧𝑞𝑧 𝐴))
303, 27, 29e22 38417 . . . . 5 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧 𝐴   )
3130in2 38351 . . . 4 (   𝑥𝐴 Tr 𝑥   ▶   ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
3231gen12 38364 . . 3 (   𝑥𝐴 Tr 𝑥   ▶   𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
33 dftr2 4724 . . . 4 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
3433biimpri 218 . . 3 (∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴) → Tr 𝐴)
3532, 34e1a 38373 . 2 (   𝑥𝐴 Tr 𝑥   ▶   Tr 𝐴   )
3635in1 38308 1 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wal 1478  wcel 1987  wral 2908  [wsbc 3422   cint 4447  Tr wtr 4722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-v 3192  df-sbc 3423  df-in 3567  df-ss 3574  df-uni 4410  df-int 4448  df-tr 4723  df-vd1 38307  df-vd2 38315  df-vd3 38327
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator