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

Theorem dfon2lem8 25163
Description: Lemma for dfon2 25165. 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 2895 . . . . . . 7  |-  x  e. 
_V
2 dfon2lem3 25158 . . . . . . 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 446 . . . . 5  |-  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  Tr  x )
54ralimi 2717 . . . 4  |-  ( A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  A. x  e.  A  Tr  x
)
6 trint 4251 . . . 4  |-  ( A. x  e.  A  Tr  x  ->  Tr  |^| A )
75, 6syl 16 . . 3  |-  ( A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  Tr  |^| A )
87adantl 453 . 2  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  ->  Tr  |^| A )
91dfon2lem7 25162 . . . . . . 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 1638 . . . . . 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 2717 . . . . 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 2647 . . . . . . 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 1902 . . . . . . . 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 1572 . . . . . . 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 244 . . . . . 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 434 . . . . . . . 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 1573 . . . . . . 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 3954 . . . . . . . . . . 11  |-  ( w  e.  U. A  <->  E. x  e.  A  w  e.  x )
1918biimpi 187 . . . . . . . . . 10  |-  ( w  e.  U. A  ->  E. x  e.  A  w  e.  x )
2019imim1i 56 . . . . . . . . 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 1565 . . . . . . . 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 1744 . . . . . . . . 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 1903 . . . . . . . . . . 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 2648 . . . . . . . . . . . 12  |-  ( E. x  e.  A  w  e.  x  <->  E. x
( x  e.  A  /\  w  e.  x
) )
2524imbi1i 316 . . . . . . . . . . 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 244 . . . . . . . . . 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 1572 . . . . . . . . 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 241 . . . . . . . 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 2647 . . . . . . . 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 258 . . . . . . 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 205 . . . . . 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 188 . . . . 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 16 . . . 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 453 . . 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 4007 . . . . 5  |-  ( A  =/=  (/)  ->  |^| A  C_  U. A )
36 ssralv 3343 . . . . 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 16 . . . 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 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
)  ->  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 25161 . . 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 4290 . . . . . . . . . . 11  |-  ( A  =/=  (/)  <->  |^| A  e.  _V )
42 dfon2lem3 25158 . . . . . . . . . . 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 188 . . . . . . . . . 10  |-  ( A  =/=  (/)  ->  ( A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A )  -> 
( Tr  |^| A  /\  A. t  e.  |^| A  -.  t  e.  t ) ) )
4443imp 419 . . . . . . . . 9  |-  ( ( A  =/=  (/)  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  ( Tr  |^| A  /\  A. t  e. 
|^| A  -.  t  e.  t ) )
4544simprd 450 . . . . . . . 8  |-  ( ( A  =/=  (/)  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  A. t  e.  |^| A  -.  t  e.  t )
46 untelirr 24929 . . . . . . . 8  |-  ( A. t  e.  |^| A  -.  t  e.  t  ->  -. 
|^| A  e.  |^| A )
4745, 46syl 16 . . . . . . 7  |-  ( ( A  =/=  (/)  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  -.  |^| A  e. 
|^| A )
4847adantlr 696 . . . . . 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 2689 . . . . . . . . . 10  |-  ( |^| A  e.  A  <->  E. t  e.  A  t  =  |^| A )
5049notbii 288 . . . . . . . . 9  |-  ( -. 
|^| A  e.  A  <->  -. 
E. t  e.  A  t  =  |^| A )
51 ralnex 2652 . . . . . . . . 9  |-  ( A. t  e.  A  -.  t  =  |^| A  <->  -.  E. t  e.  A  t  =  |^| A )
5250, 51bitr4i 244 . . . . . . . 8  |-  ( -. 
|^| A  e.  A  <->  A. t  e.  A  -.  t  =  |^| A )
53 eqcom 2382 . . . . . . . . . . . 12  |-  ( t  =  |^| A  <->  |^| A  =  t )
5453notbii 288 . . . . . . . . . . 11  |-  ( -.  t  =  |^| A  <->  -. 
|^| A  =  t )
5544simpld 446 . . . . . . . . . . . . 13  |-  ( ( A  =/=  (/)  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  Tr  |^| A )
5655adantlr 696 . . . . . . . . . . . 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 3371 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  t  ->  (
y  C.  x  <->  y  C.  t ) )
5857anbi1d 686 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  t  ->  (
( y  C.  x  /\  Tr  y )  <->  ( y  C.  t  /\  Tr  y
) ) )
59 elequ2 1722 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  t  ->  (
y  e.  x  <->  y  e.  t ) )
6058, 59imbi12d 312 . . . . . . . . . . . . . . . . 17  |-  ( x  =  t  ->  (
( ( y  C.  x  /\  Tr  y )  ->  y  e.  x
)  <->  ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t ) ) )
6160albidv 1632 . . . . . . . . . . . . . . . 16  |-  ( x  =  t  ->  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  <->  A. y
( ( y  C.  t  /\  Tr  y )  ->  y  e.  t ) ) )
6261rspccv 2985 . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . 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 4000 . . . . . . . . . . . . . . . 16  |-  ( t  e.  A  ->  |^| A  C_  t )
65 dfpss2 3368 . . . . . . . . . . . . . . . . . . . 20  |-  ( |^| A  C.  t  <->  ( |^| A  C_  t  /\  -.  |^| A  =  t ) )
66 psseq1 3370 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  |^| A  -> 
( y  C.  t  <->  |^| A  C.  t ) )
67 treq 4242 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  |^| A  -> 
( Tr  y  <->  Tr  |^| A
) )
6866, 67anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  |^| A  -> 
( ( y  C.  t  /\  Tr  y )  <-> 
( |^| A  C.  t  /\  Tr  |^| A ) ) )
69 eleq1 2440 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  |^| A  -> 
( y  e.  t  <->  |^| A  e.  t ) )
7068, 69imbi12d 312 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  |^| A  -> 
( ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  <->  ( ( |^| A  C.  t  /\  Tr  |^| A )  ->  |^| A  e.  t ) ) )
7170spcgv 2972 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( |^| A  e.  _V  ->  ( A. y ( ( y  C.  t  /\  Tr  y )  ->  y  e.  t )  ->  (
( |^| A  C.  t  /\  Tr  |^| A )  ->  |^| A  e.  t ) ) )
7241, 71sylbi 188 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A  =/=  (/)  ->  ( A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  ->  (
( |^| A  C.  t  /\  Tr  |^| A )  ->  |^| A  e.  t ) ) )
7372imp 419 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  =/=  (/)  /\  A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t ) )  -> 
( ( |^| A  C.  t  /\  Tr  |^| A )  ->  |^| A  e.  t ) )
7473exp3a 426 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  =/=  (/)  /\  A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t ) )  -> 
( |^| A  C.  t  ->  ( Tr  |^| A  ->  |^| A  e.  t ) ) )
7565, 74syl5bir 210 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  =/=  (/)  /\  A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t ) )  -> 
( ( |^| A  C_  t  /\  -.  |^| A  =  t )  ->  ( Tr  |^| A  ->  |^| A  e.  t ) ) )
7675exp4b 591 . . . . . . . . . . . . . . . . . 18  |-  ( A  =/=  (/)  ->  ( A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  ->  ( |^| A  C_  t  ->  ( -.  |^| A  =  t  ->  ( Tr  |^| A  ->  |^| A  e.  t ) ) ) ) )
7776com45 85 . . . . . . . . . . . . . . . . 17  |-  ( A  =/=  (/)  ->  ( A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  ->  ( |^| A  C_  t  ->  ( Tr  |^| A  ->  ( -.  |^| A  =  t  ->  |^| A  e.  t ) ) ) ) )
7877com23 74 . . . . . . . . . . . . . . . 16  |-  ( A  =/=  (/)  ->  ( |^| A  C_  t  ->  ( A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  ->  ( Tr  |^| A  ->  ( -.  |^| A  =  t  ->  |^| A  e.  t ) ) ) ) )
7964, 78syl5 30 . . . . . . . . . . . . . . 15  |-  ( A  =/=  (/)  ->  ( t  e.  A  ->  ( A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  ->  ( Tr  |^| A  ->  ( -.  |^| A  =  t  ->  |^| A  e.  t ) ) ) ) )
8079adantr 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 )  ->  ( Tr  |^| A  ->  ( -.  |^| A  =  t  ->  |^| A  e.  t ) ) ) ) )
8163, 80mpdd 38 . . . . . . . . . . . . 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 452 . . . . . . . . . . . 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 39 . . . . . . . . . . 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 222 . . . . . . . . . 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 2724 . . . . . . . . 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 2713 . . . . . . . . 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 16 . . . . . . . 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 209 . . . . . . 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 3993 . . . . . . . . 9  |-  ( |^| A  e.  _V  ->  (
|^| A  e.  |^| A 
<-> 
A. t  e.  A  |^| A  e.  t ) )
9041, 89sylbi 188 . . . . . . . 8  |-  ( A  =/=  (/)  ->  ( |^| A  e.  |^| A  <->  A. t  e.  A  |^| A  e.  t ) )
9190ad2antrr 707 . . . . . . 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 226 . . . . . 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 119 . . . . 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 424 . . . 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 537 . . 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 30 . 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 661 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 177    /\ wa 359   A.wal 1546   E.wex 1547    = wceq 1649    e. wcel 1717    =/= wne 2543   A.wral 2642   E.wrex 2643   _Vcvv 2892    C_ wss 3256    C. wpss 3257   (/)c0 3564   U.cuni 3950   |^|cint 3985   Tr wtr 4236
This theorem is referenced by:  dfon2lem9  25164
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-sep 4264  ax-nul 4272  ax-pr 4337  ax-un 4634
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-ral 2647  df-rex 2648  df-v 2894  df-sbc 3098  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-pss 3272  df-nul 3565  df-pw 3737  df-sn 3756  df-pr 3757  df-uni 3951  df-int 3986  df-iun 4030  df-tr 4237  df-suc 4521
  Copyright terms: Public domain W3C validator