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 39876
Description: The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT 39877. 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 39877 is trintALTVD 39876 without virtual deductions and was automatically derived from trintALTVD 39876.
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 39608 . . . . . . 7 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑧𝑦𝑦 𝐴)   )
2 simpl 475 . . . . . . 7 ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦)
31, 2e2 39626 . . . . . 6 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧𝑦   )
4 idn3 39610 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   𝑞𝐴   )
5 idn1 39560 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ▶   𝑥𝐴 Tr 𝑥   )
6 rspsbc 3713 . . . . . . . . . . . 12 (𝑞𝐴 → (∀𝑥𝐴 Tr 𝑥[𝑞 / 𝑥]Tr 𝑥))
74, 5, 6e31 39747 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   [𝑞 / 𝑥]Tr 𝑥   )
8 trsbc 39526 . . . . . . . . . . . 12 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
98biimpd 221 . . . . . . . . . . 11 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
104, 7, 9e33 39730 . . . . . . . . . 10 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   Tr 𝑞   )
11 simpr 478 . . . . . . . . . . . . . 14 ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴)
121, 11e2 39626 . . . . . . . . . . . . 13 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑦 𝐴   )
13 elintg 4675 . . . . . . . . . . . . . 14 (𝑦 𝐴 → (𝑦 𝐴 ↔ ∀𝑞𝐴 𝑦𝑞))
1413ibi 259 . . . . . . . . . . . . 13 (𝑦 𝐴 → ∀𝑞𝐴 𝑦𝑞)
1512, 14e2 39626 . . . . . . . . . . . 12 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞𝐴 𝑦𝑞   )
16 rsp 3110 . . . . . . . . . . . 12 (∀𝑞𝐴 𝑦𝑞 → (𝑞𝐴𝑦𝑞))
1715, 16e2 39626 . . . . . . . . . . 11 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑞𝐴𝑦𝑞)   )
18 pm2.27 42 . . . . . . . . . . 11 (𝑞𝐴 → ((𝑞𝐴𝑦𝑞) → 𝑦𝑞))
194, 17, 18e32 39754 . . . . . . . . . 10 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   𝑦𝑞   )
20 trel 4952 . . . . . . . . . . 11 (Tr 𝑞 → ((𝑧𝑦𝑦𝑞) → 𝑧𝑞))
2120expd 405 . . . . . . . . . 10 (Tr 𝑞 → (𝑧𝑦 → (𝑦𝑞𝑧𝑞)))
2210, 3, 19, 21e323 39762 . . . . . . . . 9 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ,   𝑞𝐴   ▶   𝑧𝑞   )
2322in3 39604 . . . . . . . 8 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   (𝑞𝐴𝑧𝑞)   )
2423gen21 39614 . . . . . . 7 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞(𝑞𝐴𝑧𝑞)   )
25 df-ral 3094 . . . . . . . 8 (∀𝑞𝐴 𝑧𝑞 ↔ ∀𝑞(𝑞𝐴𝑧𝑞))
2625biimpri 220 . . . . . . 7 (∀𝑞(𝑞𝐴𝑧𝑞) → ∀𝑞𝐴 𝑧𝑞)
2724, 26e2 39626 . . . . . 6 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑞𝐴 𝑧𝑞   )
28 elintg 4675 . . . . . . 7 (𝑧𝑦 → (𝑧 𝐴 ↔ ∀𝑞𝐴 𝑧𝑞))
2928biimprd 240 . . . . . 6 (𝑧𝑦 → (∀𝑞𝐴 𝑧𝑞𝑧 𝐴))
303, 27, 29e22 39666 . . . . 5 (   𝑥𝐴 Tr 𝑥   ,   (𝑧𝑦𝑦 𝐴)   ▶   𝑧 𝐴   )
3130in2 39600 . . . 4 (   𝑥𝐴 Tr 𝑥   ▶   ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
3231gen12 39613 . . 3 (   𝑥𝐴 Tr 𝑥   ▶   𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴)   )
33 dftr2 4947 . . . 4 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
3433biimpri 220 . . 3 (∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴) → Tr 𝐴)
3532, 34e1a 39622 . 2 (   𝑥𝐴 Tr 𝑥   ▶   Tr 𝐴   )
3635in1 39557 1 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  wal 1651  wcel 2157  wral 3089  [wsbc 3633   cint 4667  Tr wtr 4945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-v 3387  df-sbc 3634  df-in 3776  df-ss 3783  df-uni 4629  df-int 4668  df-tr 4946  df-vd1 39556  df-vd2 39564  df-vd3 39576
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator