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 44462
Description: The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 44462 is an alternate proof of trint 5284. trintALT 44462 is trintALTVD 44461 without virtual deductions and was automatically derived from trintALTVD 44461 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 481 . . . . 5 ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦)
21a1i 11 . . . 4 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦))
3 iidn3 44082 . . . . . . 7 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (𝑞𝐴𝑞𝐴)))
4 id 22 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ∀𝑥𝐴 Tr 𝑥)
5 rspsbc 3869 . . . . . . . 8 (𝑞𝐴 → (∀𝑥𝐴 Tr 𝑥[𝑞 / 𝑥]Tr 𝑥))
63, 4, 5ee31 44333 . . . . . . 7 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (𝑞𝐴[𝑞 / 𝑥]Tr 𝑥)))
7 trsbc 44121 . . . . . . . 8 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
87biimpd 228 . . . . . . 7 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
93, 6, 8ee33 44102 . . . . . 6 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (𝑞𝐴 → Tr 𝑞)))
10 simpr 483 . . . . . . . . 9 ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴)
1110a1i 11 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴))
12 elintg 4958 . . . . . . . . 9 (𝑦 𝐴 → (𝑦 𝐴 ↔ ∀𝑞𝐴 𝑦𝑞))
1312ibi 266 . . . . . . . 8 (𝑦 𝐴 → ∀𝑞𝐴 𝑦𝑞)
1411, 13syl6 35 . . . . . . 7 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ∀𝑞𝐴 𝑦𝑞))
15 rsp 3234 . . . . . . 7 (∀𝑞𝐴 𝑦𝑞 → (𝑞𝐴𝑦𝑞))
1614, 15syl6 35 . . . . . 6 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (𝑞𝐴𝑦𝑞)))
17 trel 5275 . . . . . . 7 (Tr 𝑞 → ((𝑧𝑦𝑦𝑞) → 𝑧𝑞))
1817expd 414 . . . . . 6 (Tr 𝑞 → (𝑧𝑦 → (𝑦𝑞𝑧𝑞)))
199, 2, 16, 18ee323 44089 . . . . 5 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (𝑞𝐴𝑧𝑞)))
2019ralrimdv 3141 . . . 4 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ∀𝑞𝐴 𝑧𝑞))
21 elintg 4958 . . . . 5 (𝑧𝑦 → (𝑧 𝐴 ↔ ∀𝑞𝐴 𝑧𝑞))
2221biimprd 247 . . . 4 (𝑧𝑦 → (∀𝑞𝐴 𝑧𝑞𝑧 𝐴))
232, 20, 22syl6c 70 . . 3 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
2423alrimivv 1923 . 2 (∀𝑥𝐴 Tr 𝑥 → ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
25 dftr2 5268 . 2 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
2624, 25sylibr 233 1 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wal 1531  wcel 2098  wral 3050  [wsbc 3773   cint 4950  Tr wtr 5266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-v 3463  df-sbc 3774  df-ss 3961  df-uni 4910  df-int 4951  df-tr 5267
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator