Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dfon2lem8 Structured version   Unicode version

Theorem dfon2lem8 30223
Description: Lemma for dfon2 30225. The intersection of a nonempty class  A of new ordinals is itself a new ordinal and is contained within  A (Contributed by Scott Fenton, 26-Feb-2011.)
Assertion
Ref Expression
dfon2lem8  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  -> 
( A. z ( ( z  C.  |^| A  /\  Tr  z )  -> 
z  e.  |^| A
)  /\  |^| A  e.  A ) )
Distinct variable group:    x, A, y, z

Proof of Theorem dfon2lem8
Dummy variables  w  t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3090 . . . . . . 7  |-  x  e. 
_V
2 dfon2lem3 30218 . . . . . . 7  |-  ( x  e.  _V  ->  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  ( Tr  x  /\  A. z  e.  x  -.  z  e.  z ) ) )
31, 2ax-mp 5 . . . . . 6  |-  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  ( Tr  x  /\  A. z  e.  x  -.  z  e.  z ) )
43simpld 460 . . . . 5  |-  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  Tr  x )
54ralimi 2825 . . . 4  |-  ( A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  A. x  e.  A  Tr  x
)
6 trint 4535 . . . 4  |-  ( A. x  e.  A  Tr  x  ->  Tr  |^| A )
75, 6syl 17 . . 3  |-  ( A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  Tr  |^| A )
87adantl 467 . 2  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  ->  Tr  |^| A )
91dfon2lem7 30222 . . . . . . 7  |-  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  (
w  e.  x  ->  A. t ( ( t 
C.  w  /\  Tr  t )  ->  t  e.  w ) ) )
109alrimiv 1766 . . . . . 6  |-  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  A. w
( w  e.  x  ->  A. t ( ( t  C.  w  /\  Tr  t )  ->  t  e.  w ) ) )
1110ralimi 2825 . . . . 5  |-  ( A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  A. x  e.  A  A. w
( w  e.  x  ->  A. t ( ( t  C.  w  /\  Tr  t )  ->  t  e.  w ) ) )
12 df-ral 2787 . . . . . . 7  |-  ( A. x  e.  A  A. w ( w  e.  x  ->  A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) )  <->  A. x
( x  e.  A  ->  A. w ( w  e.  x  ->  A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) ) ) )
13 19.21v 1778 . . . . . . . 8  |-  ( A. w ( x  e.  A  ->  ( w  e.  x  ->  A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) ) )  <->  ( x  e.  A  ->  A. w
( w  e.  x  ->  A. t ( ( t  C.  w  /\  Tr  t )  ->  t  e.  w ) ) ) )
1413albii 1687 . . . . . . 7  |-  ( A. x A. w ( x  e.  A  ->  (
w  e.  x  ->  A. t ( ( t 
C.  w  /\  Tr  t )  ->  t  e.  w ) ) )  <->  A. x ( x  e.  A  ->  A. w
( w  e.  x  ->  A. t ( ( t  C.  w  /\  Tr  t )  ->  t  e.  w ) ) ) )
1512, 14bitr4i 255 . . . . . 6  |-  ( A. x  e.  A  A. w ( w  e.  x  ->  A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) )  <->  A. x A. w ( x  e.  A  ->  ( w  e.  x  ->  A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) ) ) )
16 impexp 447 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  w  e.  x
)  ->  A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) )  <->  ( x  e.  A  ->  ( w  e.  x  ->  A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) ) ) )
17162albii 1688 . . . . . . 7  |-  ( A. x A. w ( ( x  e.  A  /\  w  e.  x )  ->  A. t ( ( t  C.  w  /\  Tr  t )  ->  t  e.  w ) )  <->  A. x A. w ( x  e.  A  ->  ( w  e.  x  ->  A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) ) ) )
18 eluni2 4226 . . . . . . . . . . 11  |-  ( w  e.  U. A  <->  E. x  e.  A  w  e.  x )
1918biimpi 197 . . . . . . . . . 10  |-  ( w  e.  U. A  ->  E. x  e.  A  w  e.  x )
2019imim1i 60 . . . . . . . . 9  |-  ( ( E. x  e.  A  w  e.  x  ->  A. t ( ( t 
C.  w  /\  Tr  t )  ->  t  e.  w ) )  -> 
( w  e.  U. A  ->  A. t ( ( t  C.  w  /\  Tr  t )  ->  t  e.  w ) ) )
2120alimi 1680 . . . . . . . 8  |-  ( A. w ( E. x  e.  A  w  e.  x  ->  A. t ( ( t  C.  w  /\  Tr  t )  ->  t  e.  w ) )  ->  A. w ( w  e. 
U. A  ->  A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) ) )
22 alcom 1897 . . . . . . . . 9  |-  ( A. x A. w ( ( x  e.  A  /\  w  e.  x )  ->  A. t ( ( t  C.  w  /\  Tr  t )  ->  t  e.  w ) )  <->  A. w A. x ( ( x  e.  A  /\  w  e.  x )  ->  A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) ) )
23 19.23v 1810 . . . . . . . . . . 11  |-  ( A. x ( ( x  e.  A  /\  w  e.  x )  ->  A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) )  <->  ( E. x ( x  e.  A  /\  w  e.  x )  ->  A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) ) )
24 df-rex 2788 . . . . . . . . . . . 12  |-  ( E. x  e.  A  w  e.  x  <->  E. x
( x  e.  A  /\  w  e.  x
) )
2524imbi1i 326 . . . . . . . . . . 11  |-  ( ( E. x  e.  A  w  e.  x  ->  A. t ( ( t 
C.  w  /\  Tr  t )  ->  t  e.  w ) )  <->  ( E. x ( x  e.  A  /\  w  e.  x )  ->  A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) ) )
2623, 25bitr4i 255 . . . . . . . . . 10  |-  ( A. x ( ( x  e.  A  /\  w  e.  x )  ->  A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) )  <->  ( E. x  e.  A  w  e.  x  ->  A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) ) )
2726albii 1687 . . . . . . . . 9  |-  ( A. w A. x ( ( x  e.  A  /\  w  e.  x )  ->  A. t ( ( t  C.  w  /\  Tr  t )  ->  t  e.  w ) )  <->  A. w
( E. x  e.  A  w  e.  x  ->  A. t ( ( t  C.  w  /\  Tr  t )  ->  t  e.  w ) ) )
2822, 27bitri 252 . . . . . . . 8  |-  ( A. x A. w ( ( x  e.  A  /\  w  e.  x )  ->  A. t ( ( t  C.  w  /\  Tr  t )  ->  t  e.  w ) )  <->  A. w
( E. x  e.  A  w  e.  x  ->  A. t ( ( t  C.  w  /\  Tr  t )  ->  t  e.  w ) ) )
29 df-ral 2787 . . . . . . . 8  |-  ( A. w  e.  U. A A. t ( ( t 
C.  w  /\  Tr  t )  ->  t  e.  w )  <->  A. w
( w  e.  U. A  ->  A. t ( ( t  C.  w  /\  Tr  t )  ->  t  e.  w ) ) )
3021, 28, 293imtr4i 269 . . . . . . 7  |-  ( A. x A. w ( ( x  e.  A  /\  w  e.  x )  ->  A. t ( ( t  C.  w  /\  Tr  t )  ->  t  e.  w ) )  ->  A. w  e.  U. A A. t ( ( t 
C.  w  /\  Tr  t )  ->  t  e.  w ) )
3117, 30sylbir 216 . . . . . 6  |-  ( A. x A. w ( x  e.  A  ->  (
w  e.  x  ->  A. t ( ( t 
C.  w  /\  Tr  t )  ->  t  e.  w ) ) )  ->  A. w  e.  U. A A. t ( ( t  C.  w  /\  Tr  t )  ->  t  e.  w ) )
3215, 31sylbi 198 . . . . 5  |-  ( A. x  e.  A  A. w ( w  e.  x  ->  A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) )  ->  A. w  e.  U. A A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) )
3311, 32syl 17 . . . 4  |-  ( A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  A. w  e.  U. A A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) )
3433adantl 467 . . 3  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  ->  A. w  e.  U. A A. t ( ( t 
C.  w  /\  Tr  t )  ->  t  e.  w ) )
35 intssuni 4281 . . . . 5  |-  ( A  =/=  (/)  ->  |^| A  C_  U. A )
36 ssralv 3531 . . . . 5  |-  ( |^| A  C_  U. A  -> 
( A. w  e. 
U. A A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
)  ->  A. w  e.  |^| A A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) ) )
3735, 36syl 17 . . . 4  |-  ( A  =/=  (/)  ->  ( A. w  e.  U. A A. t ( ( t 
C.  w  /\  Tr  t )  ->  t  e.  w )  ->  A. w  e.  |^| A A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) ) )
3837adantr 466 . . 3  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  -> 
( A. w  e. 
U. A A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
)  ->  A. w  e.  |^| A A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) ) )
3934, 38mpd 15 . 2  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  ->  A. w  e.  |^| A A. t ( ( t 
C.  w  /\  Tr  t )  ->  t  e.  w ) )
40 dfon2lem6 30221 . . 3  |-  ( ( Tr  |^| A  /\  A. w  e.  |^| A A. t ( ( t 
C.  w  /\  Tr  t )  ->  t  e.  w ) )  ->  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )
41 intex 4581 . . . . . . . . . . 11  |-  ( A  =/=  (/)  <->  |^| A  e.  _V )
42 dfon2lem3 30218 . . . . . . . . . . 11  |-  ( |^| A  e.  _V  ->  ( A. z ( ( z  C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A )  -> 
( Tr  |^| A  /\  A. t  e.  |^| A  -.  t  e.  t ) ) )
4341, 42sylbi 198 . . . . . . . . . 10  |-  ( A  =/=  (/)  ->  ( A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A )  -> 
( Tr  |^| A  /\  A. t  e.  |^| A  -.  t  e.  t ) ) )
4443imp 430 . . . . . . . . 9  |-  ( ( A  =/=  (/)  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  ( Tr  |^| A  /\  A. t  e. 
|^| A  -.  t  e.  t ) )
4544simprd 464 . . . . . . . 8  |-  ( ( A  =/=  (/)  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  A. t  e.  |^| A  -.  t  e.  t )
46 untelirr 30123 . . . . . . . 8  |-  ( A. t  e.  |^| A  -.  t  e.  t  ->  -. 
|^| A  e.  |^| A )
4745, 46syl 17 . . . . . . 7  |-  ( ( A  =/=  (/)  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  -.  |^| A  e. 
|^| A )
4847adantlr 719 . . . . . 6  |-  ( ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  -.  |^| A  e. 
|^| A )
49 risset 2960 . . . . . . . . . 10  |-  ( |^| A  e.  A  <->  E. t  e.  A  t  =  |^| A )
5049notbii 297 . . . . . . . . 9  |-  ( -. 
|^| A  e.  A  <->  -. 
E. t  e.  A  t  =  |^| A )
51 ralnex 2878 . . . . . . . . 9  |-  ( A. t  e.  A  -.  t  =  |^| A  <->  -.  E. t  e.  A  t  =  |^| A )
5250, 51bitr4i 255 . . . . . . . 8  |-  ( -. 
|^| A  e.  A  <->  A. t  e.  A  -.  t  =  |^| A )
53 eqcom 2438 . . . . . . . . . . . 12  |-  ( t  =  |^| A  <->  |^| A  =  t )
5453notbii 297 . . . . . . . . . . 11  |-  ( -.  t  =  |^| A  <->  -. 
|^| A  =  t )
5544simpld 460 . . . . . . . . . . . . 13  |-  ( ( A  =/=  (/)  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  Tr  |^| A )
5655adantlr 719 . . . . . . . . . . . 12  |-  ( ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  Tr  |^| A )
57 psseq2 3559 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  t  ->  (
y  C.  x  <->  y  C.  t
) )
5857anbi1d 709 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  t  ->  (
( y  C.  x  /\  Tr  y )  <->  ( y  C.  t  /\  Tr  y
) ) )
59 elequ2 1875 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  t  ->  (
y  e.  x  <->  y  e.  t ) )
6058, 59imbi12d 321 . . . . . . . . . . . . . . . . 17  |-  ( x  =  t  ->  (
( ( y  C.  x  /\  Tr  y )  ->  y  e.  x
)  <->  ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t ) ) )
6160albidv 1760 . . . . . . . . . . . . . . . 16  |-  ( x  =  t  ->  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  <->  A. y
( ( y  C.  t  /\  Tr  y )  ->  y  e.  t ) ) )
6261rspccv 3185 . . . . . . . . . . . . . . 15  |-  ( A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  (
t  e.  A  ->  A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t ) ) )
6362adantl 467 . . . . . . . . . . . . . 14  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  -> 
( t  e.  A  ->  A. y ( ( y  C.  t  /\  Tr  y )  ->  y  e.  t ) ) )
64 intss1 4273 . . . . . . . . . . . . . . . 16  |-  ( t  e.  A  ->  |^| A  C_  t )
65 dfpss2 3556 . . . . . . . . . . . . . . . . . . . 20  |-  ( |^| A  C.  t  <->  ( |^| A  C_  t  /\  -.  |^| A  =  t ) )
66 psseq1 3558 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  |^| A  -> 
( y  C.  t  <->  |^| A  C.  t )
)
67 treq 4526 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  |^| A  -> 
( Tr  y  <->  Tr  |^| A
) )
6866, 67anbi12d 715 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  |^| A  -> 
( ( y  C.  t  /\  Tr  y )  <-> 
( |^| A  C.  t  /\  Tr  |^| A ) ) )
69 eleq1 2501 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  |^| A  -> 
( y  e.  t  <->  |^| A  e.  t ) )
7068, 69imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  |^| A  -> 
( ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  <->  ( ( |^| A  C.  t  /\  Tr  |^| A )  ->  |^| A  e.  t ) ) )
7170spcgv 3172 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( |^| A  e.  _V  ->  ( A. y ( ( y  C.  t  /\  Tr  y )  ->  y  e.  t )  ->  (
( |^| A  C.  t  /\  Tr  |^| A )  ->  |^| A  e.  t ) ) )
7241, 71sylbi 198 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A  =/=  (/)  ->  ( A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  ->  (
( |^| A  C.  t  /\  Tr  |^| A )  ->  |^| A  e.  t ) ) )
7372imp 430 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  =/=  (/)  /\  A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t ) )  -> 
( ( |^| A  C.  t  /\  Tr  |^| A )  ->  |^| A  e.  t ) )
7473expd 437 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  =/=  (/)  /\  A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t ) )  -> 
( |^| A  C.  t  ->  ( Tr  |^| A  ->  |^| A  e.  t ) ) )
7565, 74syl5bir 221 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  =/=  (/)  /\  A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t ) )  -> 
( ( |^| A  C_  t  /\  -.  |^| A  =  t )  ->  ( Tr  |^| A  ->  |^| A  e.  t ) ) )
7675exp4b 610 . . . . . . . . . . . . . . . . . 18  |-  ( A  =/=  (/)  ->  ( A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  ->  ( |^| A  C_  t  ->  ( -.  |^| A  =  t  ->  ( Tr  |^| A  ->  |^| A  e.  t ) ) ) ) )
7776com45 92 . . . . . . . . . . . . . . . . 17  |-  ( A  =/=  (/)  ->  ( A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  ->  ( |^| A  C_  t  ->  ( Tr  |^| A  ->  ( -.  |^| A  =  t  ->  |^| A  e.  t ) ) ) ) )
7877com23 81 . . . . . . . . . . . . . . . 16  |-  ( A  =/=  (/)  ->  ( |^| A  C_  t  ->  ( A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  ->  ( Tr  |^| A  ->  ( -.  |^| A  =  t  ->  |^| A  e.  t ) ) ) ) )
7964, 78syl5 33 . . . . . . . . . . . . . . 15  |-  ( A  =/=  (/)  ->  ( t  e.  A  ->  ( A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  ->  ( Tr  |^| A  ->  ( -.  |^| A  =  t  ->  |^| A  e.  t ) ) ) ) )
8079adantr 466 . . . . . . . . . . . . . 14  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  -> 
( t  e.  A  ->  ( A. y ( ( y  C.  t  /\  Tr  y )  -> 
y  e.  t )  ->  ( Tr  |^| A  ->  ( -.  |^| A  =  t  ->  |^| A  e.  t ) ) ) ) )
8163, 80mpdd 41 . . . . . . . . . . . . 13  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  -> 
( t  e.  A  ->  ( Tr  |^| A  ->  ( -.  |^| A  =  t  ->  |^| A  e.  t ) ) ) )
8281adantr 466 . . . . . . . . . . . 12  |-  ( ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  ( t  e.  A  ->  ( Tr  |^| A  ->  ( -.  |^| A  =  t  ->  |^| A  e.  t ) ) ) )
8356, 82mpid 42 . . . . . . . . . . 11  |-  ( ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  ( t  e.  A  ->  ( -.  |^| A  =  t  ->  |^| A  e.  t ) ) )
8454, 83syl7bi 233 . . . . . . . . . 10  |-  ( ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  ( t  e.  A  ->  ( -.  t  =  |^| A  ->  |^| A  e.  t ) ) )
8584ralrimiv 2844 . . . . . . . . 9  |-  ( ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  A. t  e.  A  ( -.  t  =  |^| A  ->  |^| A  e.  t ) )
86 ralim 2821 . . . . . . . . 9  |-  ( A. t  e.  A  ( -.  t  =  |^| A  ->  |^| A  e.  t )  ->  ( A. t  e.  A  -.  t  =  |^| A  ->  A. t  e.  A  |^| A  e.  t ) )
8785, 86syl 17 . . . . . . . 8  |-  ( ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  ( A. t  e.  A  -.  t  =  |^| A  ->  A. t  e.  A  |^| A  e.  t ) )
8852, 87syl5bi 220 . . . . . . 7  |-  ( ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  ( -.  |^| A  e.  A  ->  A. t  e.  A  |^| A  e.  t )
)
89 elintg 4266 . . . . . . . . 9  |-  ( |^| A  e.  _V  ->  (
|^| A  e.  |^| A 
<-> 
A. t  e.  A  |^| A  e.  t ) )
9041, 89sylbi 198 . . . . . . . 8  |-  ( A  =/=  (/)  ->  ( |^| A  e.  |^| A  <->  A. t  e.  A  |^| A  e.  t ) )
9190ad2antrr 730 . . . . . . 7  |-  ( ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  ( |^| A  e.  |^| A  <->  A. t  e.  A  |^| A  e.  t ) )
9288, 91sylibrd 237 . . . . . 6  |-  ( ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  ( -.  |^| A  e.  A  ->  |^| A  e.  |^| A
) )
9348, 92mt3d 128 . . . . 5  |-  ( ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  |^| A  e.  A
)
9493ex 435 . . . 4  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  -> 
( A. z ( ( z  C.  |^| A  /\  Tr  z )  -> 
z  e.  |^| A
)  ->  |^| A  e.  A ) )
9594ancld 555 . . 3  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  -> 
( A. z ( ( z  C.  |^| A  /\  Tr  z )  -> 
z  e.  |^| A
)  ->  ( A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A )  /\  |^| A  e.  A ) ) )
9640, 95syl5 33 . 2  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  -> 
( ( Tr  |^| A  /\  A. w  e. 
|^| A A. t
( ( t  C.  w  /\  Tr  t )  ->  t  e.  w
) )  ->  ( A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A )  /\  |^| A  e.  A ) ) )
978, 39, 96mp2and 683 1  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  -> 
( A. z ( ( z  C.  |^| A  /\  Tr  z )  -> 
z  e.  |^| A
)  /\  |^| A  e.  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370   A.wal 1435    = wceq 1437   E.wex 1659    e. wcel 1870    =/= wne 2625   A.wral 2782   E.wrex 2783   _Vcvv 3087    C_ wss 3442    C. wpss 3443   (/)c0 3767   U.cuni 4222   |^|cint 4258   Tr wtr 4520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-pw 3987  df-sn 4003  df-pr 4005  df-uni 4223  df-int 4259  df-iun 4304  df-tr 4521  df-suc 5448
This theorem is referenced by:  dfon2lem9  30224
  Copyright terms: Public domain W3C validator