Step |
Hyp |
Ref |
Expression |
1 |
|
snnzg |
|- ( B e. V -> { B } =/= (/) ) |
2 |
|
fo1stres |
|- ( { B } =/= (/) -> ( 1st |` ( A X. { B } ) ) : ( A X. { B } ) -onto-> A ) |
3 |
1 2
|
syl |
|- ( B e. V -> ( 1st |` ( A X. { B } ) ) : ( A X. { B } ) -onto-> A ) |
4 |
|
moeq |
|- E* x x = <. y , B >. |
5 |
4
|
moani |
|- E* x ( y e. A /\ x = <. y , B >. ) |
6 |
|
vex |
|- y e. _V |
7 |
6
|
brresi |
|- ( x ( 1st |` ( A X. { B } ) ) y <-> ( x e. ( A X. { B } ) /\ x 1st y ) ) |
8 |
|
fo1st |
|- 1st : _V -onto-> _V |
9 |
|
fofn |
|- ( 1st : _V -onto-> _V -> 1st Fn _V ) |
10 |
8 9
|
ax-mp |
|- 1st Fn _V |
11 |
|
vex |
|- x e. _V |
12 |
|
fnbrfvb |
|- ( ( 1st Fn _V /\ x e. _V ) -> ( ( 1st ` x ) = y <-> x 1st y ) ) |
13 |
10 11 12
|
mp2an |
|- ( ( 1st ` x ) = y <-> x 1st y ) |
14 |
13
|
anbi2i |
|- ( ( x e. ( A X. { B } ) /\ ( 1st ` x ) = y ) <-> ( x e. ( A X. { B } ) /\ x 1st y ) ) |
15 |
|
elxp7 |
|- ( x e. ( A X. { B } ) <-> ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. { B } ) ) ) |
16 |
|
eleq1 |
|- ( ( 1st ` x ) = y -> ( ( 1st ` x ) e. A <-> y e. A ) ) |
17 |
16
|
biimpac |
|- ( ( ( 1st ` x ) e. A /\ ( 1st ` x ) = y ) -> y e. A ) |
18 |
17
|
adantlr |
|- ( ( ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. { B } ) /\ ( 1st ` x ) = y ) -> y e. A ) |
19 |
18
|
adantll |
|- ( ( ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. { B } ) ) /\ ( 1st ` x ) = y ) -> y e. A ) |
20 |
|
elsni |
|- ( ( 2nd ` x ) e. { B } -> ( 2nd ` x ) = B ) |
21 |
|
eqopi |
|- ( ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) = y /\ ( 2nd ` x ) = B ) ) -> x = <. y , B >. ) |
22 |
21
|
anass1rs |
|- ( ( ( x e. ( _V X. _V ) /\ ( 2nd ` x ) = B ) /\ ( 1st ` x ) = y ) -> x = <. y , B >. ) |
23 |
20 22
|
sylanl2 |
|- ( ( ( x e. ( _V X. _V ) /\ ( 2nd ` x ) e. { B } ) /\ ( 1st ` x ) = y ) -> x = <. y , B >. ) |
24 |
23
|
adantlrl |
|- ( ( ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. { B } ) ) /\ ( 1st ` x ) = y ) -> x = <. y , B >. ) |
25 |
19 24
|
jca |
|- ( ( ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. { B } ) ) /\ ( 1st ` x ) = y ) -> ( y e. A /\ x = <. y , B >. ) ) |
26 |
15 25
|
sylanb |
|- ( ( x e. ( A X. { B } ) /\ ( 1st ` x ) = y ) -> ( y e. A /\ x = <. y , B >. ) ) |
27 |
26
|
adantl |
|- ( ( B e. V /\ ( x e. ( A X. { B } ) /\ ( 1st ` x ) = y ) ) -> ( y e. A /\ x = <. y , B >. ) ) |
28 |
|
simprr |
|- ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> x = <. y , B >. ) |
29 |
|
simprl |
|- ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> y e. A ) |
30 |
|
snidg |
|- ( B e. V -> B e. { B } ) |
31 |
30
|
adantr |
|- ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> B e. { B } ) |
32 |
29 31
|
opelxpd |
|- ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> <. y , B >. e. ( A X. { B } ) ) |
33 |
28 32
|
eqeltrd |
|- ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> x e. ( A X. { B } ) ) |
34 |
28
|
fveq2d |
|- ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> ( 1st ` x ) = ( 1st ` <. y , B >. ) ) |
35 |
|
simpl |
|- ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> B e. V ) |
36 |
|
op1stg |
|- ( ( y e. A /\ B e. V ) -> ( 1st ` <. y , B >. ) = y ) |
37 |
29 35 36
|
syl2anc |
|- ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> ( 1st ` <. y , B >. ) = y ) |
38 |
34 37
|
eqtrd |
|- ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> ( 1st ` x ) = y ) |
39 |
33 38
|
jca |
|- ( ( B e. V /\ ( y e. A /\ x = <. y , B >. ) ) -> ( x e. ( A X. { B } ) /\ ( 1st ` x ) = y ) ) |
40 |
27 39
|
impbida |
|- ( B e. V -> ( ( x e. ( A X. { B } ) /\ ( 1st ` x ) = y ) <-> ( y e. A /\ x = <. y , B >. ) ) ) |
41 |
14 40
|
bitr3id |
|- ( B e. V -> ( ( x e. ( A X. { B } ) /\ x 1st y ) <-> ( y e. A /\ x = <. y , B >. ) ) ) |
42 |
7 41
|
syl5bb |
|- ( B e. V -> ( x ( 1st |` ( A X. { B } ) ) y <-> ( y e. A /\ x = <. y , B >. ) ) ) |
43 |
42
|
mobidv |
|- ( B e. V -> ( E* x x ( 1st |` ( A X. { B } ) ) y <-> E* x ( y e. A /\ x = <. y , B >. ) ) ) |
44 |
5 43
|
mpbiri |
|- ( B e. V -> E* x x ( 1st |` ( A X. { B } ) ) y ) |
45 |
44
|
alrimiv |
|- ( B e. V -> A. y E* x x ( 1st |` ( A X. { B } ) ) y ) |
46 |
|
funcnv2 |
|- ( Fun `' ( 1st |` ( A X. { B } ) ) <-> A. y E* x x ( 1st |` ( A X. { B } ) ) y ) |
47 |
45 46
|
sylibr |
|- ( B e. V -> Fun `' ( 1st |` ( A X. { B } ) ) ) |
48 |
|
dff1o3 |
|- ( ( 1st |` ( A X. { B } ) ) : ( A X. { B } ) -1-1-onto-> A <-> ( ( 1st |` ( A X. { B } ) ) : ( A X. { B } ) -onto-> A /\ Fun `' ( 1st |` ( A X. { B } ) ) ) ) |
49 |
3 47 48
|
sylanbrc |
|- ( B e. V -> ( 1st |` ( A X. { B } ) ) : ( A X. { B } ) -1-1-onto-> A ) |