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

Theorem acexmidlemcase 5820
Description: Lemma for acexmid 5824. 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 5173.

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 4489 . . . . . . . . . . . . . 14  |-  { x  e.  { (/) ,  { (/) } }  |  ( x  =  (/)  \/  ph ) }  e.  On
31, 2eqeltri 2230 . . . . . . . . . . . . 13  |-  A  e.  On
4 prid1g 3664 . . . . . . . . . . . . 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 2233 . . . . . . . . . . 11  |-  A  e.  C
8 eleq1 2220 . . . . . . . . . . . . . . 15  |-  ( z  =  A  ->  (
z  e.  u  <->  A  e.  u ) )
98anbi1d 461 . . . . . . . . . . . . . 14  |-  ( z  =  A  ->  (
( z  e.  u  /\  v  e.  u
)  <->  ( A  e.  u  /\  v  e.  u ) ) )
109rexbidv 2458 . . . . . . . . . . . . 13  |-  ( z  =  A  ->  ( E. u  e.  y 
( z  e.  u  /\  v  e.  u
)  <->  E. u  e.  y  ( A  e.  u  /\  v  e.  u
) ) )
1110reueqd 2662 . . . . . . . . . . . 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 2812 . . . . . . . . . . 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 5795 . . . . . . . . . 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 2865 . . . . . . . . . 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 2252 . . . . . . . . 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 3583 . . . . . . . . 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 2220 . . . . . . . . . 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 778 . . . . . . . 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 4151 . . . . . . . . . . . . . . 15  |-  { (/) ,  { (/) } }  e.  _V
2625rabex 4109 . . . . . . . . . . . . . 14  |-  { x  e.  { (/) ,  { (/) } }  |  ( x  =  { (/) }  \/  ph ) }  e.  _V
2724, 26eqeltri 2230 . . . . . . . . . . . . 13  |-  B  e. 
_V
2827prid2 3667 . . . . . . . . . . . 12  |-  B  e. 
{ A ,  B }
2928, 6eleqtrri 2233 . . . . . . . . . . 11  |-  B  e.  C
30 eleq1 2220 . . . . . . . . . . . . . . 15  |-  ( z  =  B  ->  (
z  e.  u  <->  B  e.  u ) )
3130anbi1d 461 . . . . . . . . . . . . . 14  |-  ( z  =  B  ->  (
( z  e.  u  /\  v  e.  u
)  <->  ( B  e.  u  /\  v  e.  u ) ) )
3231rexbidv 2458 . . . . . . . . . . . . 13  |-  ( z  =  B  ->  ( E. u  e.  y 
( z  e.  u  /\  v  e.  u
)  <->  E. u  e.  y  ( B  e.  u  /\  v  e.  u
) ) )
3332reueqd 2662 . . . . . . . . . . . 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 2812 . . . . . . . . . . 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 5795 . . . . . . . . . 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 2865 . . . . . . . . . 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 2252 . . . . . . . . 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 3583 . . . . . . . . 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 2220 . . . . . . . . . 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 777 . . . . . . . 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 811 . . . . . 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 706 . . . . . 6  |-  ( ( ( { (/) }  e.  A  /\  (/)  e.  B )  \/  ( { (/) }  e.  A  /\  ( iota_ v  e.  B  E. u  e.  y  ( B  e.  u  /\  v  e.  u )
)  =  { (/) } ) )  ->  { (/) }  e.  A )
5251orim2i 751 . . . . 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 719 . . 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 750 . . . 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 751 . . 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 966 . 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 698    \/ w3o 962    = wceq 1335    e. wcel 2128   A.wral 2435   E.wrex 2436   E!wreu 2437   {crab 2439   _Vcvv 2712   (/)c0 3394   {csn 3560   {cpr 3561   Oncon0 4324   iota_crio 5780
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 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4083  ax-nul 4091  ax-pow 4136
This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-eu 2009  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-pw 3545  df-sn 3566  df-pr 3567  df-uni 3774  df-tr 4064  df-iord 4327  df-on 4329  df-suc 4332  df-iota 5136  df-riota 5781
This theorem is referenced by:  acexmidlem1  5821
  Copyright terms: Public domain W3C validator