ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  acexmidlemcase Unicode version

Theorem acexmidlemcase 5848
Description: Lemma for acexmid 5852. Here we divide the proof into cases (based on the disjunction implicit in an unordered pair, not the sort of case elimination which relies on excluded middle).

The cases are (1) the choice function evaluated at  A equals  { (/) }, (2) the choice function evaluated at  B equals  (/), and (3) the choice function evaluated at  A equals 
(/) and the choice function evaluated at  B equals  { (/) }.

Because of the way we represent the choice function  y, the choice function evaluated at  A is  ( iota_ v  e.  A E. u  e.  y ( A  e.  u  /\  v  e.  u ) ) and the choice function evaluated at  B is  ( iota_ v  e.  B E. u  e.  y ( B  e.  u  /\  v  e.  u ) ). Other than the difference in notation these work just as  ( y `  A ) and  ( y `  B ) would if  y were a function as defined by df-fun 5200.

Although it isn't exactly about the division into cases, it is also convenient for this lemma to also include the step that if the choice function evaluated at  A equals  { (/) }, then  { (/) }  e.  A and likewise for  B.

(Contributed by Jim Kingdon, 7-Aug-2019.)

Hypotheses
Ref Expression
acexmidlem.a  |-  A  =  { x  e.  { (/)
,  { (/) } }  |  ( x  =  (/)  \/  ph ) }
acexmidlem.b  |-  B  =  { x  e.  { (/)
,  { (/) } }  |  ( x  =  { (/) }  \/  ph ) }
acexmidlem.c  |-  C  =  { A ,  B }
Assertion
Ref Expression
acexmidlemcase  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  ( { (/) }  e.  A  \/  (/)  e.  B  \/  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } ) ) )
Distinct variable groups:    x, y, z, v, u, A    x, B, y, z, v, u   
x, C, y, z, v, u    ph, x, y, z, v, u

Proof of Theorem acexmidlemcase
StepHypRef Expression
1 acexmidlem.a . . . . . . . . . . . . . 14  |-  A  =  { x  e.  { (/)
,  { (/) } }  |  ( x  =  (/)  \/  ph ) }
2 onsucelsucexmidlem 4513 . . . . . . . . . . . . . 14  |-  { x  e.  { (/) ,  { (/) } }  |  ( x  =  (/)  \/  ph ) }  e.  On
31, 2eqeltri 2243 . . . . . . . . . . . . 13  |-  A  e.  On
4 prid1g 3687 . . . . . . . . . . . . 13  |-  ( A  e.  On  ->  A  e.  { A ,  B } )
53, 4ax-mp 5 . . . . . . . . . . . 12  |-  A  e. 
{ A ,  B }
6 acexmidlem.c . . . . . . . . . . . 12  |-  C  =  { A ,  B }
75, 6eleqtrri 2246 . . . . . . . . . . 11  |-  A  e.  C
8 eleq1 2233 . . . . . . . . . . . . . . 15  |-  ( z  =  A  ->  (
z  e.  u  <->  A  e.  u ) )
98anbi1d 462 . . . . . . . . . . . . . 14  |-  ( z  =  A  ->  (
( z  e.  u  /\  v  e.  u
)  <->  ( A  e.  u  /\  v  e.  u ) ) )
109rexbidv 2471 . . . . . . . . . . . . 13  |-  ( z  =  A  ->  ( E. u  e.  y 
( z  e.  u  /\  v  e.  u
)  <->  E. u  e.  y  ( A  e.  u  /\  v  e.  u
) ) )
1110reueqd 2675 . . . . . . . . . . . 12  |-  ( z  =  A  ->  ( E! v  e.  z  E. u  e.  y 
( z  e.  u  /\  v  e.  u
)  <->  E! v  e.  A  E. u  e.  y 
( A  e.  u  /\  v  e.  u
) ) )
1211rspcv 2830 . . . . . . . . . . 11  |-  ( A  e.  C  ->  ( A. z  e.  C  E! v  e.  z  E. u  e.  y 
( z  e.  u  /\  v  e.  u
)  ->  E! v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) ) )
137, 12ax-mp 5 . . . . . . . . . 10  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  E! v  e.  A  E. u  e.  y 
( A  e.  u  /\  v  e.  u
) )
14 riotacl 5823 . . . . . . . . . 10  |-  ( E! v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u )  ->  ( iota_ v  e.  A  E. u  e.  y 
( A  e.  u  /\  v  e.  u
) )  e.  A
)
1513, 14syl 14 . . . . . . . . 9  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  ( iota_ v  e.  A  E. u  e.  y 
( A  e.  u  /\  v  e.  u
) )  e.  A
)
16 elrabi 2883 . . . . . . . . . 10  |-  ( (
iota_ v  e.  A  E. u  e.  y 
( A  e.  u  /\  v  e.  u
) )  e.  {
x  e.  { (/) ,  { (/) } }  | 
( x  =  (/)  \/ 
ph ) }  ->  (
iota_ v  e.  A  E. u  e.  y 
( A  e.  u  /\  v  e.  u
) )  e.  { (/)
,  { (/) } }
)
1716, 1eleq2s 2265 . . . . . . . . 9  |-  ( (
iota_ v  e.  A  E. u  e.  y 
( A  e.  u  /\  v  e.  u
) )  e.  A  ->  ( iota_ v  e.  A  E. u  e.  y 
( A  e.  u  /\  v  e.  u
) )  e.  { (/)
,  { (/) } }
)
18 elpri 3606 . . . . . . . . 9  |-  ( (
iota_ v  e.  A  E. u  e.  y 
( A  e.  u  /\  v  e.  u
) )  e.  { (/)
,  { (/) } }  ->  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  \/  ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  { (/) } ) )
1915, 17, 183syl 17 . . . . . . . 8  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  \/  ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  { (/) } ) )
20 eleq1 2233 . . . . . . . . . 10  |-  ( (
iota_ v  e.  A  E. u  e.  y 
( A  e.  u  /\  v  e.  u
) )  =  { (/)
}  ->  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u )
)  e.  A  <->  { (/) }  e.  A ) )
2115, 20syl5ibcom 154 . . . . . . . . 9  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  { (/) }  ->  { (/) }  e.  A ) )
2221orim2d 783 . . . . . . . 8  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  ( ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  \/  ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  { (/) } )  -> 
( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  \/  { (/) }  e.  A ) ) )
2319, 22mpd 13 . . . . . . 7  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  \/  { (/) }  e.  A ) )
24 acexmidlem.b . . . . . . . . . . . . . 14  |-  B  =  { x  e.  { (/)
,  { (/) } }  |  ( x  =  { (/) }  \/  ph ) }
25 pp0ex 4175 . . . . . . . . . . . . . . 15  |-  { (/) ,  { (/) } }  e.  _V
2625rabex 4133 . . . . . . . . . . . . . 14  |-  { x  e.  { (/) ,  { (/) } }  |  ( x  =  { (/) }  \/  ph ) }  e.  _V
2724, 26eqeltri 2243 . . . . . . . . . . . . 13  |-  B  e. 
_V
2827prid2 3690 . . . . . . . . . . . 12  |-  B  e. 
{ A ,  B }
2928, 6eleqtrri 2246 . . . . . . . . . . 11  |-  B  e.  C
30 eleq1 2233 . . . . . . . . . . . . . . 15  |-  ( z  =  B  ->  (
z  e.  u  <->  B  e.  u ) )
3130anbi1d 462 . . . . . . . . . . . . . 14  |-  ( z  =  B  ->  (
( z  e.  u  /\  v  e.  u
)  <->  ( B  e.  u  /\  v  e.  u ) ) )
3231rexbidv 2471 . . . . . . . . . . . . 13  |-  ( z  =  B  ->  ( E. u  e.  y 
( z  e.  u  /\  v  e.  u
)  <->  E. u  e.  y  ( B  e.  u  /\  v  e.  u
) ) )
3332reueqd 2675 . . . . . . . . . . . 12  |-  ( z  =  B  ->  ( E! v  e.  z  E. u  e.  y 
( z  e.  u  /\  v  e.  u
)  <->  E! v  e.  B  E. u  e.  y 
( B  e.  u  /\  v  e.  u
) ) )
3433rspcv 2830 . . . . . . . . . . 11  |-  ( B  e.  C  ->  ( A. z  e.  C  E! v  e.  z  E. u  e.  y 
( z  e.  u  /\  v  e.  u
)  ->  E! v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) ) )
3529, 34ax-mp 5 . . . . . . . . . 10  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  E! v  e.  B  E. u  e.  y 
( B  e.  u  /\  v  e.  u
) )
36 riotacl 5823 . . . . . . . . . 10  |-  ( E! v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u )  ->  ( iota_ v  e.  B  E. u  e.  y 
( B  e.  u  /\  v  e.  u
) )  e.  B
)
3735, 36syl 14 . . . . . . . . 9  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  ( iota_ v  e.  B  E. u  e.  y 
( B  e.  u  /\  v  e.  u
) )  e.  B
)
38 elrabi 2883 . . . . . . . . . 10  |-  ( (
iota_ v  e.  B  E. u  e.  y 
( B  e.  u  /\  v  e.  u
) )  e.  {
x  e.  { (/) ,  { (/) } }  | 
( x  =  { (/)
}  \/  ph ) }  ->  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  e. 
{ (/) ,  { (/) } } )
3938, 24eleq2s 2265 . . . . . . . . 9  |-  ( (
iota_ v  e.  B  E. u  e.  y 
( B  e.  u  /\  v  e.  u
) )  e.  B  ->  ( iota_ v  e.  B  E. u  e.  y 
( B  e.  u  /\  v  e.  u
) )  e.  { (/)
,  { (/) } }
)
40 elpri 3606 . . . . . . . . 9  |-  ( (
iota_ v  e.  B  E. u  e.  y 
( B  e.  u  /\  v  e.  u
) )  e.  { (/)
,  { (/) } }  ->  ( ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  (/)  \/  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } ) )
4137, 39, 403syl 17 . . . . . . . 8  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  ( ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  (/)  \/  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } ) )
42 eleq1 2233 . . . . . . . . . 10  |-  ( (
iota_ v  e.  B  E. u  e.  y 
( B  e.  u  /\  v  e.  u
) )  =  (/)  ->  ( ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  e.  B  <->  (/)  e.  B ) )
4337, 42syl5ibcom 154 . . . . . . . . 9  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  ( ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  (/)  ->  (/)  e.  B ) )
4443orim1d 782 . . . . . . . 8  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  ( ( ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  (/)  \/  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } )  -> 
( (/)  e.  B  \/  ( iota_ v  e.  B  E. u  e.  y 
( B  e.  u  /\  v  e.  u
) )  =  { (/)
} ) ) )
4541, 44mpd 13 . . . . . . 7  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  ( (/)  e.  B  \/  ( iota_ v  e.  B  E. u  e.  y 
( B  e.  u  /\  v  e.  u
) )  =  { (/)
} ) )
4623, 45jca 304 . . . . . 6  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  ( ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  \/  { (/) }  e.  A )  /\  ( (/) 
e.  B  \/  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u )
)  =  { (/) } ) ) )
47 anddi 816 . . . . . 6  |-  ( ( ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  \/  { (/) }  e.  A )  /\  ( (/) 
e.  B  \/  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u )
)  =  { (/) } ) )  <->  ( (
( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  (/)  e.  B )  \/  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } ) )  \/  ( ( {
(/) }  e.  A  /\  (/)  e.  B )  \/  ( { (/) }  e.  A  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u )
)  =  { (/) } ) ) ) )
4846, 47sylib 121 . . . . 5  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  ( ( ( (
iota_ v  e.  A  E. u  e.  y 
( A  e.  u  /\  v  e.  u
) )  =  (/)  /\  (/)  e.  B )  \/  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } ) )  \/  ( ( {
(/) }  e.  A  /\  (/)  e.  B )  \/  ( { (/) }  e.  A  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u )
)  =  { (/) } ) ) ) )
49 simpl 108 . . . . . . 7  |-  ( ( { (/) }  e.  A  /\  (/)  e.  B )  ->  { (/) }  e.  A )
50 simpl 108 . . . . . . 7  |-  ( ( { (/) }  e.  A  /\  ( iota_ v  e.  B  E. u  e.  y 
( B  e.  u  /\  v  e.  u
) )  =  { (/)
} )  ->  { (/) }  e.  A )
5149, 50jaoi 711 . . . . . 6  |-  ( ( ( { (/) }  e.  A  /\  (/)  e.  B )  \/  ( { (/) }  e.  A  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u )
)  =  { (/) } ) )  ->  { (/) }  e.  A )
5251orim2i 756 . . . . 5  |-  ( ( ( ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  (/)  e.  B )  \/  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } ) )  \/  ( ( {
(/) }  e.  A  /\  (/)  e.  B )  \/  ( { (/) }  e.  A  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u )
)  =  { (/) } ) ) )  -> 
( ( ( (
iota_ v  e.  A  E. u  e.  y 
( A  e.  u  /\  v  e.  u
) )  =  (/)  /\  (/)  e.  B )  \/  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } ) )  \/  { (/) }  e.  A ) )
5348, 52syl 14 . . . 4  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  ( ( ( (
iota_ v  e.  A  E. u  e.  y 
( A  e.  u  /\  v  e.  u
) )  =  (/)  /\  (/)  e.  B )  \/  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } ) )  \/  { (/) }  e.  A ) )
5453orcomd 724 . . 3  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  ( { (/) }  e.  A  \/  ( (
( iota_ v  e.  A  E. u  e.  y 
( A  e.  u  /\  v  e.  u
) )  =  (/)  /\  (/)  e.  B )  \/  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } ) ) ) )
55 simpr 109 . . . . 5  |-  ( ( ( iota_ v  e.  A  E. u  e.  y 
( A  e.  u  /\  v  e.  u
) )  =  (/)  /\  (/)  e.  B )  ->  (/) 
e.  B )
5655orim1i 755 . . . 4  |-  ( ( ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  (/)  e.  B )  \/  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } ) )  ->  ( (/)  e.  B  \/  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } ) ) )
5756orim2i 756 . . 3  |-  ( ( { (/) }  e.  A  \/  ( ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  (/)  e.  B )  \/  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } ) ) )  ->  ( { (/)
}  e.  A  \/  ( (/)  e.  B  \/  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } ) ) ) )
5854, 57syl 14 . 2  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  ( { (/) }  e.  A  \/  ( (/)  e.  B  \/  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } ) ) ) )
59 3orass 976 . 2  |-  ( ( { (/) }  e.  A  \/  (/)  e.  B  \/  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } ) )  <-> 
( { (/) }  e.  A  \/  ( (/)  e.  B  \/  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } ) ) ) )
6058, 59sylibr 133 1  |-  ( A. z  e.  C  E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  ->  ( { (/) }  e.  A  \/  (/)  e.  B  \/  ( ( iota_ v  e.  A  E. u  e.  y  ( A  e.  u  /\  v  e.  u ) )  =  (/)  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u ) )  =  { (/) } ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    \/ wo 703    \/ w3o 972    = wceq 1348    e. wcel 2141   A.wral 2448   E.wrex 2449   E!wreu 2450   {crab 2452   _Vcvv 2730   (/)c0 3414   {csn 3583   {cpr 3584   Oncon0 4348   iota_crio 5808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-nul 4115  ax-pow 4160
This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-eu 2022  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3568  df-sn 3589  df-pr 3590  df-uni 3797  df-tr 4088  df-iord 4351  df-on 4353  df-suc 4356  df-iota 5160  df-riota 5809
This theorem is referenced by:  acexmidlem1  5849
  Copyright terms: Public domain W3C validator