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

Theorem dfon2lem8 25360
Description: Lemma for dfon2 25362. 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 2919 . . . . . . 7  |-  x  e. 
_V
2 dfon2lem3 25355 . . . . . . 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 2741 . . . 4  |-  ( A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  A. x  e.  A  Tr  x
)
6 trint 4277 . . . 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 25359 . . . . . . 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 2741 . . . . 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 2671 . . . . . . 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 1909 . . . . . . . 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 3979 . . . . . . . . . . 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 1748 . . . . . . . . 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 1910 . . . . . . . . . . 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 2672 . . . . . . . . . . . 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 2671 . . . . . . . 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 4032 . . . . 5  |-  ( A  =/=  (/)  ->  |^| A  C_  U. A )
36 ssralv 3367 . . . . 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 25358 . . 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 4316 . . . . . . . . . . 11  |-  ( A  =/=  (/)  <->  |^| A  e.  _V )
42 dfon2lem3 25355 . . . . . . . . . . 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 25110 . . . . . . . 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 2713 . . . . . . . . . 10  |-  ( |^| A  e.  A  <->  E. t  e.  A  t  =  |^| A )
5049notbii 288 . . . . . . . . 9  |-  ( -. 
|^| A  e.  A  <->  -. 
E. t  e.  A  t  =  |^| A )
51 ralnex 2676 . . . . . . . . 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 2406 . . . . . . . . . . . 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 3395 . . . . . . . . . . . . . . . . . . 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 1726 . . . . . . . . . . . . . . . . . 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 3009 . . . . . . . . . . . . . . 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 4025 . . . . . . . . . . . . . . . 16  |-  ( t  e.  A  ->  |^| A  C_  t )
65 dfpss2 3392 . . . . . . . . . . . . . . . . . . . 20  |-  ( |^| A  C.  t  <->  ( |^| A  C_  t  /\  -.  |^| A  =  t ) )
66 psseq1 3394 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  |^| A  -> 
( y  C.  t  <->  |^| A  C.  t ) )
67 treq 4268 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2464 . . . . . . . . . . . . . . . . . . . . . . . . 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 2996 . . . . . . . . . . . . . . . . . . . . . . 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 2748 . . . . . . . . 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 2737 . . . . . . . . 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 4018 . . . . . . . . 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 1721    =/= wne 2567   A.wral 2666   E.wrex 2667   _Vcvv 2916    C_ wss 3280    C. wpss 3281   (/)c0 3588   U.cuni 3975   |^|cint 4010   Tr wtr 4262
This theorem is referenced by:  dfon2lem9  25361
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 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363  ax-un 4660
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-pw 3761  df-sn 3780  df-pr 3781  df-uni 3976  df-int 4011  df-iun 4055  df-tr 4263  df-suc 4547
  Copyright terms: Public domain W3C validator