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 39633
Description: The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT 39634. 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 39634 is trintALTVD 39633 without virtual deductions and was automatically derived from trintALTVD 39633.
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 39358 . . . . . . 7 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑧𝑦𝑦 𝐴)   )
2 simpl 474 . . . . . . 7 ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦)
31, 2e2 39376 . . . . . 6 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧𝑦   )
4 idn3 39360 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   𝑞𝐴   )
5 idn1 39310 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ▶   𝑥𝐴 Tr 𝑥   )
6 rspsbc 3659 . . . . . . . . . . . 12 (𝑞𝐴 → (∀𝑥𝐴 Tr 𝑥[𝑞 / 𝑥]Tr 𝑥))
74, 5, 6e31 39498 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   [𝑞 / 𝑥]Tr 𝑥   )
8 trsbc 39270 . . . . . . . . . . . 12 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
98biimpd 219 . . . . . . . . . . 11 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
104, 7, 9e33 39481 . . . . . . . . . 10 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   Tr 𝑞   )
11 simpr 479 . . . . . . . . . . . . . 14 ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴)
121, 11e2 39376 . . . . . . . . . . . . 13 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑦 𝐴   )
13 elintg 4635 . . . . . . . . . . . . . 14 (𝑦 𝐴 → (𝑦 𝐴 ↔ ∀𝑞𝐴 𝑦𝑞))
1413ibi 256 . . . . . . . . . . . . 13 (𝑦 𝐴 → ∀𝑞𝐴 𝑦𝑞)
1512, 14e2 39376 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞𝐴 𝑦𝑞   )
16 rsp 3067 . . . . . . . . . . . 12 (∀𝑞𝐴 𝑦𝑞 → (𝑞𝐴𝑦𝑞))
1715, 16e2 39376 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑞𝐴𝑦𝑞)   )
18 pm2.27 42 . . . . . . . . . . 11 (𝑞𝐴 → ((𝑞𝐴𝑦𝑞) → 𝑦𝑞))
194, 17, 18e32 39505 . . . . . . . . . 10 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   𝑦𝑞   )
20 trel 4911 . . . . . . . . . . 11 (Tr 𝑞 → ((𝑧𝑦𝑦𝑞) → 𝑧𝑞))
2120expd 451 . . . . . . . . . 10 (Tr 𝑞 → (𝑧𝑦 → (𝑦𝑞𝑧𝑞)))
2210, 3, 19, 21e323 39513 . . . . . . . . 9 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   𝑧𝑞   )
2322in3 39354 . . . . . . . 8 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑞𝐴𝑧𝑞)   )
2423gen21 39364 . . . . . . 7 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞(𝑞𝐴𝑧𝑞)   )
25 df-ral 3055 . . . . . . . 8 (∀𝑞𝐴 𝑧𝑞 ↔ ∀𝑞(𝑞𝐴𝑧𝑞))
2625biimpri 218 . . . . . . 7 (∀𝑞(𝑞𝐴𝑧𝑞) → ∀𝑞𝐴 𝑧𝑞)
2724, 26e2 39376 . . . . . 6 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞𝐴 𝑧𝑞   )
28 elintg 4635 . . . . . . 7 (𝑧𝑦 → (𝑧 𝐴 ↔ ∀𝑞𝐴 𝑧𝑞))
2928biimprd 238 . . . . . 6 (𝑧𝑦 → (∀𝑞𝐴 𝑧𝑞𝑧 𝐴))
303, 27, 29e22 39416 . . . . 5 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧 𝐴   )
3130in2 39350 . . . 4 (   𝑥𝐴 Tr 𝑥   ▶   ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
3231gen12 39363 . . 3 (   𝑥𝐴 Tr 𝑥   ▶   𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
33 dftr2 4906 . . . 4 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
3433biimpri 218 . . 3 (∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴) → Tr 𝐴)
3532, 34e1a 39372 . 2 (   𝑥𝐴 Tr 𝑥   ▶   Tr 𝐴   )
3635in1 39307 1 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wal 1630  wcel 2139  wral 3050  [wsbc 3576   cint 4627  Tr wtr 4904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-v 3342  df-sbc 3577  df-in 3722  df-ss 3729  df-uni 4589  df-int 4628  df-tr 4905  df-vd1 39306  df-vd2 39314  df-vd3 39326
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator