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

Theorem dfon2lem8 30429
Description: Lemma for dfon2 30431. 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 3047 . . . . . . 7  |-  x  e. 
_V
2 dfon2lem3 30424 . . . . . . 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 461 . . . . 5  |-  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  Tr  x )
54ralimi 2780 . . . 4  |-  ( A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  A. x  e.  A  Tr  x
)
6 trint 4511 . . . 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 468 . 2  |-  ( ( A  =/=  (/)  /\  A. x  e.  A  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) )  ->  Tr  |^| A )
91dfon2lem7 30428 . . . . . . 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 1772 . . . . . 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 2780 . . . . 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 2741 . . . . . . 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 1785 . . . . . . . 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 1690 . . . . . . 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 256 . . . . . 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 448 . . . . . . . 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 1691 . . . . . . 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 4201 . . . . . . . . . . 11  |-  ( w  e.  U. A  <->  E. x  e.  A  w  e.  x )
1918biimpi 198 . . . . . . . . . 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 1683 . . . . . . . 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 1922 . . . . . . . . 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 1817 . . . . . . . . . . 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 2742 . . . . . . . . . . . 12  |-  ( E. x  e.  A  w  e.  x  <->  E. x
( x  e.  A  /\  w  e.  x
) )
2524imbi1i 327 . . . . . . . . . . 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 256 . . . . . . . . . 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 1690 . . . . . . . . 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 253 . . . . . . . 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 2741 . . . . . . . 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 270 . . . . . . 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 217 . . . . . 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 199 . . . . 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 468 . . 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 4256 . . . . 5  |-  ( A  =/=  (/)  ->  |^| A  C_  U. A )
36 ssralv 3492 . . . . 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 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
)  ->  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 30427 . . 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 4558 . . . . . . . . . . 11  |-  ( A  =/=  (/)  <->  |^| A  e.  _V )
42 dfon2lem3 30424 . . . . . . . . . . 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 199 . . . . . . . . . 10  |-  ( A  =/=  (/)  ->  ( A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A )  -> 
( Tr  |^| A  /\  A. t  e.  |^| A  -.  t  e.  t ) ) )
4443imp 431 . . . . . . . . 9  |-  ( ( A  =/=  (/)  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  ( Tr  |^| A  /\  A. t  e. 
|^| A  -.  t  e.  t ) )
4544simprd 465 . . . . . . . 8  |-  ( ( A  =/=  (/)  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  A. t  e.  |^| A  -.  t  e.  t )
46 untelirr 30328 . . . . . . . 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 720 . . . . . 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 2914 . . . . . . . . . 10  |-  ( |^| A  e.  A  <->  E. t  e.  A  t  =  |^| A )
5049notbii 298 . . . . . . . . 9  |-  ( -. 
|^| A  e.  A  <->  -. 
E. t  e.  A  t  =  |^| A )
51 ralnex 2833 . . . . . . . . 9  |-  ( A. t  e.  A  -.  t  =  |^| A  <->  -.  E. t  e.  A  t  =  |^| A )
5250, 51bitr4i 256 . . . . . . . 8  |-  ( -. 
|^| A  e.  A  <->  A. t  e.  A  -.  t  =  |^| A )
53 eqcom 2457 . . . . . . . . . . . 12  |-  ( t  =  |^| A  <->  |^| A  =  t )
5453notbii 298 . . . . . . . . . . 11  |-  ( -.  t  =  |^| A  <->  -. 
|^| A  =  t )
5544simpld 461 . . . . . . . . . . . . 13  |-  ( ( A  =/=  (/)  /\  A. z ( ( z 
C.  |^| A  /\  Tr  z )  ->  z  e.  |^| A ) )  ->  Tr  |^| A )
5655adantlr 720 . . . . . . . . . . . 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 3520 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  t  ->  (
y  C.  x  <->  y  C.  t
) )
5857anbi1d 710 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  t  ->  (
( y  C.  x  /\  Tr  y )  <->  ( y  C.  t  /\  Tr  y
) ) )
59 elequ2 1900 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  t  ->  (
y  e.  x  <->  y  e.  t ) )
6058, 59imbi12d 322 . . . . . . . . . . . . . . . . 17  |-  ( x  =  t  ->  (
( ( y  C.  x  /\  Tr  y )  ->  y  e.  x
)  <->  ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t ) ) )
6160albidv 1766 . . . . . . . . . . . . . . . 16  |-  ( x  =  t  ->  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  <->  A. y
( ( y  C.  t  /\  Tr  y )  ->  y  e.  t ) ) )
6261rspccv 3146 . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . 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 4248 . . . . . . . . . . . . . . . 16  |-  ( t  e.  A  ->  |^| A  C_  t )
65 dfpss2 3517 . . . . . . . . . . . . . . . . . . . 20  |-  ( |^| A  C.  t  <->  ( |^| A  C_  t  /\  -.  |^| A  =  t ) )
66 psseq1 3519 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  |^| A  -> 
( y  C.  t  <->  |^| A  C.  t )
)
67 treq 4502 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  |^| A  -> 
( Tr  y  <->  Tr  |^| A
) )
6866, 67anbi12d 716 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  |^| A  -> 
( ( y  C.  t  /\  Tr  y )  <-> 
( |^| A  C.  t  /\  Tr  |^| A ) ) )
69 eleq1 2516 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  |^| A  -> 
( y  e.  t  <->  |^| A  e.  t ) )
7068, 69imbi12d 322 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  |^| A  -> 
( ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  <->  ( ( |^| A  C.  t  /\  Tr  |^| A )  ->  |^| A  e.  t ) ) )
7170spcgv 3133 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( |^| A  e.  _V  ->  ( A. y ( ( y  C.  t  /\  Tr  y )  ->  y  e.  t )  ->  (
( |^| A  C.  t  /\  Tr  |^| A )  ->  |^| A  e.  t ) ) )
7241, 71sylbi 199 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A  =/=  (/)  ->  ( A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t )  ->  (
( |^| A  C.  t  /\  Tr  |^| A )  ->  |^| A  e.  t ) ) )
7372imp 431 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  =/=  (/)  /\  A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t ) )  -> 
( ( |^| A  C.  t  /\  Tr  |^| A )  ->  |^| A  e.  t ) )
7473expd 438 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  =/=  (/)  /\  A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t ) )  -> 
( |^| A  C.  t  ->  ( Tr  |^| A  ->  |^| A  e.  t ) ) )
7565, 74syl5bir 222 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  =/=  (/)  /\  A. y ( ( y 
C.  t  /\  Tr  y )  ->  y  e.  t ) )  -> 
( ( |^| A  C_  t  /\  -.  |^| A  =  t )  ->  ( Tr  |^| A  ->  |^| A  e.  t ) ) )
7675exp4b 611 . . . . . . . . . . . . . . . . . 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 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 )  ->  ( 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 467 . . . . . . . . . . . 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 234 . . . . . . . . . 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 2799 . . . . . . . . 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 2776 . . . . . . . . 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 221 . . . . . . 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 4241 . . . . . . . . 9  |-  ( |^| A  e.  _V  ->  (
|^| A  e.  |^| A 
<-> 
A. t  e.  A  |^| A  e.  t ) )
9041, 89sylbi 199 . . . . . . . 8  |-  ( A  =/=  (/)  ->  ( |^| A  e.  |^| A  <->  A. t  e.  A  |^| A  e.  t ) )
9190ad2antrr 731 . . . . . . 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 238 . . . . . 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 129 . . . . 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 436 . . . 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 556 . . 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 684 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 188    /\ wa 371   A.wal 1441    = wceq 1443   E.wex 1662    e. wcel 1886    =/= wne 2621   A.wral 2736   E.wrex 2737   _Vcvv 3044    C_ wss 3403    C. wpss 3404   (/)c0 3730   U.cuni 4197   |^|cint 4233   Tr wtr 4496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638  ax-un 6580
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-pw 3952  df-sn 3968  df-pr 3970  df-uni 4198  df-int 4234  df-iun 4279  df-tr 4497  df-suc 5428
This theorem is referenced by:  dfon2lem9  30430
  Copyright terms: Public domain W3C validator