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

Theorem trintALT 39639
 Description: The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 39639 is an alternate proof of trint 4902. trintALT 39639 is trintALTVD 39638 without virtual deductions and was automatically derived from trintALTVD 39638 using the tools program translate..without..overwriting.cmd and Metamath's minimize 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 468 . . . . 5 ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦)
21a1i 11 . . . 4 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑧𝑦))
3 iidn3 39232 . . . . . . 7 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (𝑞𝐴𝑞𝐴)))
4 id 22 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ∀𝑥𝐴 Tr 𝑥)
5 rspsbc 3667 . . . . . . . 8 (𝑞𝐴 → (∀𝑥𝐴 Tr 𝑥[𝑞 / 𝑥]Tr 𝑥))
63, 4, 5ee31 39504 . . . . . . 7 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (𝑞𝐴[𝑞 / 𝑥]Tr 𝑥)))
7 trsbc 39275 . . . . . . . 8 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
87biimpd 219 . . . . . . 7 (𝑞𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
93, 6, 8ee33 39252 . . . . . 6 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (𝑞𝐴 → Tr 𝑞)))
10 simpr 471 . . . . . . . . 9 ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴)
1110a1i 11 . . . . . . . 8 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑦 𝐴))
12 elintg 4620 . . . . . . . . 9 (𝑦 𝐴 → (𝑦 𝐴 ↔ ∀𝑞𝐴 𝑦𝑞))
1312ibi 256 . . . . . . . 8 (𝑦 𝐴 → ∀𝑞𝐴 𝑦𝑞)
1411, 13syl6 35 . . . . . . 7 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ∀𝑞𝐴 𝑦𝑞))
15 rsp 3078 . . . . . . 7 (∀𝑞𝐴 𝑦𝑞 → (𝑞𝐴𝑦𝑞))
1614, 15syl6 35 . . . . . 6 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (𝑞𝐴𝑦𝑞)))
17 trel 4894 . . . . . . 7 (Tr 𝑞 → ((𝑧𝑦𝑦𝑞) → 𝑧𝑞))
1817expd 400 . . . . . 6 (Tr 𝑞 → (𝑧𝑦 → (𝑦𝑞𝑧𝑞)))
199, 2, 16, 18ee323 39239 . . . . 5 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → (𝑞𝐴𝑧𝑞)))
2019ralrimdv 3117 . . . 4 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → ∀𝑞𝐴 𝑧𝑞))
21 elintg 4620 . . . . 5 (𝑧𝑦 → (𝑧 𝐴 ↔ ∀𝑞𝐴 𝑧𝑞))
2221biimprd 238 . . . 4 (𝑧𝑦 → (∀𝑞𝐴 𝑧𝑞𝑧 𝐴))
232, 20, 22syl6c 70 . . 3 (∀𝑥𝐴 Tr 𝑥 → ((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
2423alrimivv 2008 . 2 (∀𝑥𝐴 Tr 𝑥 → ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
25 dftr2 4889 . 2 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 𝐴) → 𝑧 𝐴))
2624, 25sylibr 224 1 (∀𝑥𝐴 Tr 𝑥 → Tr 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 382  ∀wal 1629   ∈ wcel 2145  ∀wral 3061  [wsbc 3587  ∩ cint 4612  Tr wtr 4887 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-v 3353  df-sbc 3588  df-in 3730  df-ss 3737  df-uni 4576  df-int 4613  df-tr 4888 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator