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

Theorem trintALT 28730
Description: The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 28730 is an alternative proof of trint 4130. trintALT 28730 is trintALTVD 28729 without virtual deductions and was automatically derived from trintALTVD 28729 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 28318 . . . . . . 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 3071 . . . . . . . 8  |-  ( q  e.  A  ->  ( A. x  e.  A  Tr  x  ->  [. q  /  x ]. Tr  x
) )
63, 4, 5ee31 28598 . . . . . . 7  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  |^| A )  -> 
( q  e.  A  ->  [. q  /  x ]. Tr  x ) ) )
7 trsbc 28360 . . . . . . . 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 28340 . . . . . 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 3872 . . . . . . . . 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 2605 . . . . . . 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 4122 . . . . . . 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 28325 . . . . 5  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  |^| A )  -> 
( q  e.  A  ->  z  e.  q ) ) )
2019ralrimdv 2634 . . . 4  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  |^| A )  ->  A. q  e.  A  z  e.  q )
)
21 elintg 3872 . . . . 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 1620 . 2  |-  ( A. x  e.  A  Tr  x  ->  A. z A. y
( ( z  e.  y  /\  y  e. 
|^| A )  -> 
z  e.  |^| A
) )
25 dftr2 4117 . 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 1529    e. wcel 1686   A.wral 2545   [.wsbc 2993   |^|cint 3864   Tr wtr 4115
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ral 2550  df-v 2792  df-sbc 2994  df-in 3161  df-ss 3168  df-uni 3830  df-int 3865  df-tr 4116
  Copyright terms: Public domain W3C validator