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

Theorem dfon2lem8 24146
Description: Lemma for dfon2 24148. The intersection of a non-empty 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 2791 . . . . . . 7  |-  x  e. 
_V
2 dfon2lem3 24141 . . . . . . 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 8 . . . . . 6  |-  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  ( Tr  x  /\  A. z  e.  x  -.  z  e.  z ) )
43simpld 445 . . . . 5  |-  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  Tr  x )
54ralimi 2618 . . . 4  |-  ( A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  A. x  e.  A  Tr  x
)
6 trint 4128 . . . 4  |-  ( A. x  e.  A  Tr  x  ->  Tr  |^| A )
75, 6syl 15 . . 3  |-  ( A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  Tr  |^| A )
87adantl 452 . 2  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  ->  Tr  |^| A )
91dfon2lem7 24145 . . . . . . 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 1617 . . . . . 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 2618 . . . . 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 2548 . . . . . . 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 1831 . . . . . . . 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 1553 . . . . . . 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 243 . . . . . 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 433 . . . . . . . 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 1554 . . . . . . 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 3831 . . . . . . . . . . 11  |-  ( w  e.  U. A  <->  E. x  e.  A  w  e.  x )
1918biimpi 186 . . . . . . . . . 10  |-  ( w  e.  U. A  ->  E. x  e.  A  w  e.  x )
2019imim1i 54 . . . . . . . . 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 1546 . . . . . . . 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 1711 . . . . . . . . 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 1832 . . . . . . . . . . 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 2549 . . . . . . . . . . . 12  |-  ( E. x  e.  A  w  e.  x  <->  E. x
( x  e.  A  /\  w  e.  x
) )
2524imbi1i 315 . . . . . . . . . . 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 243 . . . . . . . . . 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 1553 . . . . . . . . 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 240 . . . . . . . 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 2548 . . . . . . . 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 257 . . . . . . 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 204 . . . . . 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 187 . . . . 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 15 . . . 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 452 . . 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 3884 . . . . 5  |-  ( A  =/=  (/)  ->  |^| A  C_  U. A )
36 ssralv 3237 . . . . 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 15 . . . 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 451 . . 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 14 . 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 24144 . . 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 4167 . . . . . . . . . . 11  |-  ( A  =/=  (/)  <->  |^| A  e.  _V )
42 dfon2lem3 24141 . . . . . . . . . . 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 187 . . . . . . . . . 10  |-  ( A  =/=  (/)  ->  ( A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A )  -> 
( Tr  |^| A  /\  A. t  e.  |^| A  -.  t  e.  t ) ) )
4443imp 418 . . . . . . . . 9  |-  ( ( A  =/=  (/)  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  ( Tr  |^| A  /\  A. t  e. 
|^| A  -.  t  e.  t ) )
4544simprd 449 . . . . . . . 8  |-  ( ( A  =/=  (/)  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  A. t  e.  |^| A  -.  t  e.  t )
46 untelirr 24054 . . . . . . . 8  |-  ( A. t  e.  |^| A  -.  t  e.  t  ->  -. 
|^| A  e.  |^| A )
4745, 46syl 15 . . . . . . 7  |-  ( ( A  =/=  (/)  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  -.  |^| A  e. 
|^| A )
4847adantlr 695 . . . . . 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 2590 . . . . . . . . . 10  |-  ( |^| A  e.  A  <->  E. t  e.  A  t  =  |^| A )
5049notbii 287 . . . . . . . . 9  |-  ( -. 
|^| A  e.  A  <->  -. 
E. t  e.  A  t  =  |^| A )
51 ralnex 2553 . . . . . . . . 9  |-  ( A. t  e.  A  -.  t  =  |^| A  <->  -.  E. t  e.  A  t  =  |^| A )
5250, 51bitr4i 243 . . . . . . . 8  |-  ( -. 
|^| A  e.  A  <->  A. t  e.  A  -.  t  =  |^| A )
53 eqcom 2285 . . . . . . . . . . . 12  |-  ( t  =  |^| A  <->  |^| A  =  t )
5453notbii 287 . . . . . . . . . . 11  |-  ( -.  t  =  |^| A  <->  -. 
|^| A  =  t )
5544simpld 445 . . . . . . . . . . . . 13  |-  ( ( A  =/=  (/)  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  Tr  |^| A )
5655adantlr 695 . . . . . . . . . . . 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 3264 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  t  ->  (
y  C.  x  <->  y  C.  t ) )
5857anbi1d 685 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  t  ->  (
( y  C.  x  /\  Tr  y )  <->  ( y  C.  t  /\  Tr  y
) ) )
59 elequ2 1689 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  t  ->  (
y  e.  x  <->  y  e.  t ) )
6058, 59imbi12d 311 . . . . . . . . . . . . . . . . 17  |-  ( x  =  t  ->  (
( ( y  C.  x  /\  Tr  y )  ->  y  e.  x
)  <->  ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t ) ) )
6160albidv 1611 . . . . . . . . . . . . . . . 16  |-  ( x  =  t  ->  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  <->  A. y
( ( y  C.  t  /\  Tr  y )  ->  y  e.  t ) ) )
6261rspccv 2881 . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . 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 3877 . . . . . . . . . . . . . . . 16  |-  ( t  e.  A  ->  |^| A  C_  t )
65 dfpss2 3261 . . . . . . . . . . . . . . . . . . . 20  |-  ( |^| A  C.  t  <->  ( |^| A  C_  t  /\  -.  |^| A  =  t ) )
66 psseq1 3263 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  |^| A  -> 
( y  C.  t  <->  |^| A  C.  t ) )
67 treq 4119 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  |^| A  -> 
( Tr  y  <->  Tr  |^| A
) )
6866, 67anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  |^| A  -> 
( ( y  C.  t  /\  Tr  y )  <-> 
( |^| A  C.  t  /\  Tr  |^| A ) ) )
69 eleq1 2343 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  |^| A  -> 
( y  e.  t  <->  |^| A  e.  t ) )
7068, 69imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  |^| A  -> 
( ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  <->  ( ( |^| A  C.  t  /\  Tr  |^| A )  ->  |^| A  e.  t ) ) )
7170spcgv 2868 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( |^| A  e.  _V  ->  ( A. y ( ( y  C.  t  /\  Tr  y )  ->  y  e.  t )  ->  (
( |^| A  C.  t  /\  Tr  |^| A )  ->  |^| A  e.  t ) ) )
7241, 71sylbi 187 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A  =/=  (/)  ->  ( A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  ->  (
( |^| A  C.  t  /\  Tr  |^| A )  ->  |^| A  e.  t ) ) )
7372imp 418 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  =/=  (/)  /\  A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t ) )  -> 
( ( |^| A  C.  t  /\  Tr  |^| A )  ->  |^| A  e.  t ) )
7473exp3a 425 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  =/=  (/)  /\  A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t ) )  -> 
( |^| A  C.  t  ->  ( Tr  |^| A  ->  |^| A  e.  t ) ) )
7565, 74syl5bir 209 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  =/=  (/)  /\  A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t ) )  -> 
( ( |^| A  C_  t  /\  -.  |^| A  =  t )  ->  ( Tr  |^| A  ->  |^| A  e.  t ) ) )
7675exp4b 590 . . . . . . . . . . . . . . . . . 18  |-  ( A  =/=  (/)  ->  ( A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  ->  ( |^| A  C_  t  ->  ( -.  |^| A  =  t  ->  ( Tr  |^| A  ->  |^| A  e.  t ) ) ) ) )
7776com45 83 . . . . . . . . . . . . . . . . 17  |-  ( A  =/=  (/)  ->  ( A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  ->  ( |^| A  C_  t  ->  ( Tr  |^| A  ->  ( -.  |^| A  =  t  ->  |^| A  e.  t ) ) ) ) )
7877com23 72 . . . . . . . . . . . . . . . 16  |-  ( A  =/=  (/)  ->  ( |^| A  C_  t  ->  ( A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  ->  ( Tr  |^| A  ->  ( -.  |^| A  =  t  ->  |^| A  e.  t ) ) ) ) )
7964, 78syl5 28 . . . . . . . . . . . . . . 15  |-  ( A  =/=  (/)  ->  ( t  e.  A  ->  ( A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  ->  ( Tr  |^| A  ->  ( -.  |^| A  =  t  ->  |^| A  e.  t ) ) ) ) )
8079adantr 451 . . . . . . . . . . . . . 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 36 . . . . . . . . . . . . 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 451 . . . . . . . . . . . 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 37 . . . . . . . . . . 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 221 . . . . . . . . . 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 2625 . . . . . . . . 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 2614 . . . . . . . . 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 15 . . . . . . . 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 208 . . . . . . 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 3870 . . . . . . . . 9  |-  ( |^| A  e.  _V  ->  (
|^| A  e.  |^| A 
<-> 
A. t  e.  A  |^| A  e.  t ) )
9041, 89sylbi 187 . . . . . . . 8  |-  ( A  =/=  (/)  ->  ( |^| A  e.  |^| A  <->  A. t  e.  A  |^| A  e.  t ) )
9190ad2antrr 706 . . . . . . 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 225 . . . . . 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 117 . . . . 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 423 . . . 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 536 . . 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 28 . 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 660 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 set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527   E.wex 1528    = wceq 1623    e. wcel 1684    =/= wne 2446   A.wral 2543   E.wrex 2544   _Vcvv 2788    C_ wss 3152    C. wpss 3153   (/)c0 3455   U.cuni 3827   |^|cint 3862   Tr wtr 4113
This theorem is referenced by:  dfon2lem9  24147
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-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  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-ne 2448  df-ral 2548  df-rex 2549  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-pw 3627  df-sn 3646  df-pr 3647  df-uni 3828  df-int 3863  df-iun 3907  df-tr 4114  df-suc 4398
  Copyright terms: Public domain W3C validator