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

Theorem trintALT 28421
Description: The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 28421 is an alternative proof of trint 4230. trintALT 28421 is trintALTVD 28420 without virtual deductions and was automatically derived from trintALTVD 28420 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  |-  ( A. x  e.  A  Tr  x  ->  Tr  |^| A )
Distinct variable group:    x, A

Proof of Theorem trintALT
Dummy variables  q 
y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 443 . . . . 5  |-  ( ( z  e.  y  /\  y  e.  |^| A )  ->  z  e.  y )
21a1i 10 . . . 4  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  |^| A )  -> 
z  e.  y ) )
3 iidn3 28009 . . . . . . 7  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  |^| A )  -> 
( q  e.  A  ->  q  e.  A ) ) )
4 id 19 . . . . . . . 8  |-  ( A. x  e.  A  Tr  x  ->  A. x  e.  A  Tr  x )
5 rspsbc 3155 . . . . . . . 8  |-  ( q  e.  A  ->  ( A. x  e.  A  Tr  x  ->  [. q  /  x ]. Tr  x
) )
63, 4, 5ee31 28289 . . . . . . 7  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  |^| A )  -> 
( q  e.  A  ->  [. q  /  x ]. Tr  x ) ) )
7 trsbc 28051 . . . . . . . 8  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  <->  Tr  q
) )
87biimpd 198 . . . . . . 7  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  ->  Tr  q ) )
93, 6, 8ee33 28031 . . . . . 6  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  |^| A )  -> 
( q  e.  A  ->  Tr  q ) ) )
10 simpr 447 . . . . . . . . 9  |-  ( ( z  e.  y  /\  y  e.  |^| A )  ->  y  e.  |^| A )
1110a1i 10 . . . . . . . 8  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  |^| A )  -> 
y  e.  |^| A
) )
12 elintg 3972 . . . . . . . . 9  |-  ( y  e.  |^| A  ->  (
y  e.  |^| A  <->  A. q  e.  A  y  e.  q ) )
1312ibi 232 . . . . . . . 8  |-  ( y  e.  |^| A  ->  A. q  e.  A  y  e.  q )
1411, 13syl6 29 . . . . . . 7  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  |^| A )  ->  A. q  e.  A  y  e.  q )
)
15 rsp 2688 . . . . . . 7  |-  ( A. q  e.  A  y  e.  q  ->  ( q  e.  A  ->  y  e.  q ) )
1614, 15syl6 29 . . . . . 6  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  |^| A )  -> 
( q  e.  A  ->  y  e.  q ) ) )
17 trel 4222 . . . . . . 7  |-  ( Tr  q  ->  ( (
z  e.  y  /\  y  e.  q )  ->  z  e.  q ) )
1817exp3a 425 . . . . . 6  |-  ( Tr  q  ->  ( z  e.  y  ->  ( y  e.  q  ->  z  e.  q ) ) )
199, 2, 16, 18ee323 28016 . . . . 5  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  |^| A )  -> 
( q  e.  A  ->  z  e.  q ) ) )
2019ralrimdv 2717 . . . 4  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  |^| A )  ->  A. q  e.  A  z  e.  q )
)
21 elintg 3972 . . . . 5  |-  ( z  e.  y  ->  (
z  e.  |^| A  <->  A. q  e.  A  z  e.  q ) )
2221biimprd 214 . . . 4  |-  ( z  e.  y  ->  ( A. q  e.  A  z  e.  q  ->  z  e.  |^| A ) )
232, 20, 22ee22 1367 . . 3  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  |^| A )  -> 
z  e.  |^| A
) )
2423alrimivv 1637 . 2  |-  ( A. x  e.  A  Tr  x  ->  A. z A. y
( ( z  e.  y  /\  y  e. 
|^| A )  -> 
z  e.  |^| A
) )
25 dftr2 4217 . 2  |-  ( Tr 
|^| A  <->  A. z A. y ( ( z  e.  y  /\  y  e.  |^| A )  -> 
z  e.  |^| A
) )
2624, 25sylibr 203 1  |-  ( A. x  e.  A  Tr  x  ->  Tr  |^| A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1545    e. wcel 1715   A.wral 2628   [.wsbc 3077   |^|cint 3964   Tr wtr 4215
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ral 2633  df-v 2875  df-sbc 3078  df-in 3245  df-ss 3252  df-uni 3930  df-int 3965  df-tr 4216
  Copyright terms: Public domain W3C validator