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

Theorem trintALT 28657
Description: The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 28657 is an alternative proof of trint 4128. trintALT 28657 is trintALTVD 28656 without virtual deductions and was automatically derived from trintALTVD 28656 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 28262 . . . . . . 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 3069 . . . . . . . 8  |-  ( q  e.  A  ->  ( A. x  e.  A  Tr  x  ->  [. q  /  x ]. Tr  x
) )
63, 4, 5ee31 28527 . . . . . . 7  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  |^| A )  -> 
( q  e.  A  ->  [. q  /  x ]. Tr  x ) ) )
7 trsbc 28304 . . . . . . . 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 28284 . . . . . 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 3870 . . . . . . . . 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 2603 . . . . . . 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 4120 . . . . . . 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 28269 . . . . 5  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  |^| A )  -> 
( q  e.  A  ->  z  e.  q ) ) )
2019ralrimdv 2632 . . . 4  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  |^| A )  ->  A. q  e.  A  z  e.  q )
)
21 elintg 3870 . . . . 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 1352 . . 3  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  |^| A )  -> 
z  e.  |^| A
) )
2423alrimivv 1618 . 2  |-  ( A. x  e.  A  Tr  x  ->  A. z A. y
( ( z  e.  y  /\  y  e. 
|^| A )  -> 
z  e.  |^| A
) )
25 dftr2 4115 . 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 1527    e. wcel 1684   A.wral 2543   [.wsbc 2991   |^|cint 3862   Tr wtr 4113
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790  df-sbc 2992  df-in 3159  df-ss 3166  df-uni 3828  df-int 3863  df-tr 4114
  Copyright terms: Public domain W3C validator