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

Theorem trintALT 43724
Description: The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 43724 is an alternate proof of trint 5283. trintALT 43724 is trintALTVD 43723 without virtual deductions and was automatically derived from trintALTVD 43723 using the tools program translate..without..overwriting.cmd and the Metamath program "MM-PA> MINIMIZE_WITH *" command. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
trintALT (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem trintALT
Dummy variables 𝑞 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 483 . . . . 5 ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦)
21a1i 11 . . . 4 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦))
3 iidn3 43344 . . . . . . 7 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (𝑞𝐴𝑞𝐴)))
4 id 22 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ∀𝑥𝐴 Tr 𝑥)
5 rspsbc 3873 . . . . . . . 8 (𝑞𝐴 → (∀𝑥𝐴 Tr 𝑥[𝑞 / 𝑥]Tr 𝑥))
63, 4, 5ee31 43595 . . . . . . 7 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (𝑞𝐴[𝑞 / 𝑥]Tr 𝑥)))
7 trsbc 43383 . . . . . . . 8 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
87biimpd 228 . . . . . . 7 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
93, 6, 8ee33 43364 . . . . . 6 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (𝑞𝐴 → Tr 𝑞)))
10 simpr 485 . . . . . . . . 9 ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴)
1110a1i 11 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴))
12 elintg 4958 . . . . . . . . 9 (𝑦 𝐴 → (𝑦 𝐴 ↔ ∀𝑞𝐴 𝑦𝑞))
1312ibi 266 . . . . . . . 8 (𝑦 𝐴 → ∀𝑞𝐴 𝑦𝑞)
1411, 13syl6 35 . . . . . . 7 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ∀𝑞𝐴 𝑦𝑞))
15 rsp 3244 . . . . . . 7 (∀𝑞𝐴 𝑦𝑞 → (𝑞𝐴𝑦𝑞))
1614, 15syl6 35 . . . . . 6 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (𝑞𝐴𝑦𝑞)))
17 trel 5274 . . . . . . 7 (Tr 𝑞 → ((𝑧𝑦𝑦𝑞) → 𝑧𝑞))
1817expd 416 . . . . . 6 (Tr 𝑞 → (𝑧𝑦 → (𝑦𝑞𝑧𝑞)))
199, 2, 16, 18ee323 43351 . . . . 5 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (𝑞𝐴𝑧𝑞)))
2019ralrimdv 3152 . . . 4 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ∀𝑞𝐴 𝑧𝑞))
21 elintg 4958 . . . . 5 (𝑧𝑦 → (𝑧 𝐴 ↔ ∀𝑞𝐴 𝑧𝑞))
2221biimprd 247 . . . 4 (𝑧𝑦 → (∀𝑞𝐴 𝑧𝑞𝑧 𝐴))
232, 20, 22syl6c 70 . . 3 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
2423alrimivv 1931 . 2 (∀𝑥𝐴 Tr 𝑥 → ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
25 dftr2 5267 . 2 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
2624, 25sylibr 233 1 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wal 1539  wcel 2106  wral 3061  [wsbc 3777   cint 4950  Tr wtr 5265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-v 3476  df-sbc 3778  df-in 3955  df-ss 3965  df-uni 4909  df-int 4951  df-tr 5266
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator