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 44900
Description: The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT 44901. 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 44901 is trintALTVD 44900 without virtual deductions and was automatically derived from trintALTVD 44900.
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 44633 . . . . . . 7 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑧𝑦𝑦 𝐴)   )
2 simpl 482 . . . . . . 7 ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦)
31, 2e2 44651 . . . . . 6 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧𝑦   )
4 idn3 44635 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   𝑞𝐴   )
5 idn1 44594 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ▶   𝑥𝐴 Tr 𝑥   )
6 rspsbc 3879 . . . . . . . . . . . 12 (𝑞𝐴 → (∀𝑥𝐴 Tr 𝑥[𝑞 / 𝑥]Tr 𝑥))
74, 5, 6e31 44771 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   [𝑞 / 𝑥]Tr 𝑥   )
8 trsbc 44560 . . . . . . . . . . . 12 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
98biimpd 229 . . . . . . . . . . 11 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
104, 7, 9e33 44754 . . . . . . . . . 10 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   Tr 𝑞   )
11 simpr 484 . . . . . . . . . . . . . 14 ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴)
121, 11e2 44651 . . . . . . . . . . . . 13 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑦 𝐴   )
13 elintg 4954 . . . . . . . . . . . . . 14 (𝑦 𝐴 → (𝑦 𝐴 ↔ ∀𝑞𝐴 𝑦𝑞))
1413ibi 267 . . . . . . . . . . . . 13 (𝑦 𝐴 → ∀𝑞𝐴 𝑦𝑞)
1512, 14e2 44651 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞𝐴 𝑦𝑞   )
16 rsp 3247 . . . . . . . . . . . 12 (∀𝑞𝐴 𝑦𝑞 → (𝑞𝐴𝑦𝑞))
1715, 16e2 44651 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑞𝐴𝑦𝑞)   )
18 pm2.27 42 . . . . . . . . . . 11 (𝑞𝐴 → ((𝑞𝐴𝑦𝑞) → 𝑦𝑞))
194, 17, 18e32 44778 . . . . . . . . . 10 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   𝑦𝑞   )
20 trel 5268 . . . . . . . . . . 11 (Tr 𝑞 → ((𝑧𝑦𝑦𝑞) → 𝑧𝑞))
2120expd 415 . . . . . . . . . 10 (Tr 𝑞 → (𝑧𝑦 → (𝑦𝑞𝑧𝑞)))
2210, 3, 19, 21e323 44786 . . . . . . . . 9 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   𝑧𝑞   )
2322in3 44629 . . . . . . . 8 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑞𝐴𝑧𝑞)   )
2423gen21 44639 . . . . . . 7 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞(𝑞𝐴𝑧𝑞)   )
25 df-ral 3062 . . . . . . . 8 (∀𝑞𝐴 𝑧𝑞 ↔ ∀𝑞(𝑞𝐴𝑧𝑞))
2625biimpri 228 . . . . . . 7 (∀𝑞(𝑞𝐴𝑧𝑞) → ∀𝑞𝐴 𝑧𝑞)
2724, 26e2 44651 . . . . . 6 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞𝐴 𝑧𝑞   )
28 elintg 4954 . . . . . . 7 (𝑧𝑦 → (𝑧 𝐴 ↔ ∀𝑞𝐴 𝑧𝑞))
2928biimprd 248 . . . . . 6 (𝑧𝑦 → (∀𝑞𝐴 𝑧𝑞𝑧 𝐴))
303, 27, 29e22 44691 . . . . 5 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧 𝐴   )
3130in2 44625 . . . 4 (   𝑥𝐴 Tr 𝑥   ▶   ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
3231gen12 44638 . . 3 (   𝑥𝐴 Tr 𝑥   ▶   𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
33 dftr2 5261 . . . 4 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
3433biimpri 228 . . 3 (∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴) → Tr 𝐴)
3532, 34e1a 44647 . 2 (   𝑥𝐴 Tr 𝑥   ▶   Tr 𝐴   )
3635in1 44591 1 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wal 1538  wcel 2108  wral 3061  [wsbc 3788   cint 4946  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-int 4947  df-tr 5260  df-vd1 44590  df-vd2 44598  df-vd3 44610
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator