Step |
Hyp |
Ref |
Expression |
1 |
|
simp3 |
|- ( ( A e. X /\ B e. Y /\ X ~~ Y ) -> X ~~ Y ) |
2 |
|
bren |
|- ( X ~~ Y <-> E. g g : X -1-1-onto-> Y ) |
3 |
1 2
|
sylib |
|- ( ( A e. X /\ B e. Y /\ X ~~ Y ) -> E. g g : X -1-1-onto-> Y ) |
4 |
|
relen |
|- Rel ~~ |
5 |
4
|
brrelex2i |
|- ( X ~~ Y -> Y e. _V ) |
6 |
5
|
3ad2ant3 |
|- ( ( A e. X /\ B e. Y /\ X ~~ Y ) -> Y e. _V ) |
7 |
6
|
adantr |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> Y e. _V ) |
8 |
|
f1of |
|- ( g : X -1-1-onto-> Y -> g : X --> Y ) |
9 |
8
|
adantl |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> g : X --> Y ) |
10 |
|
simpl1 |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> A e. X ) |
11 |
9 10
|
ffvelrnd |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> ( g ` A ) e. Y ) |
12 |
|
simpl2 |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> B e. Y ) |
13 |
|
difsnen |
|- ( ( Y e. _V /\ ( g ` A ) e. Y /\ B e. Y ) -> ( Y \ { ( g ` A ) } ) ~~ ( Y \ { B } ) ) |
14 |
7 11 12 13
|
syl3anc |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> ( Y \ { ( g ` A ) } ) ~~ ( Y \ { B } ) ) |
15 |
|
bren |
|- ( ( Y \ { ( g ` A ) } ) ~~ ( Y \ { B } ) <-> E. h h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) |
16 |
14 15
|
sylib |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> E. h h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) |
17 |
|
fvex |
|- ( g ` A ) e. _V |
18 |
17
|
a1i |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( g ` A ) e. _V ) |
19 |
|
simpl2 |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> B e. Y ) |
20 |
|
f1osng |
|- ( ( ( g ` A ) e. _V /\ B e. Y ) -> { <. ( g ` A ) , B >. } : { ( g ` A ) } -1-1-onto-> { B } ) |
21 |
18 19 20
|
syl2anc |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> { <. ( g ` A ) , B >. } : { ( g ` A ) } -1-1-onto-> { B } ) |
22 |
|
simprr |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) |
23 |
|
disjdif |
|- ( { ( g ` A ) } i^i ( Y \ { ( g ` A ) } ) ) = (/) |
24 |
23
|
a1i |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( { ( g ` A ) } i^i ( Y \ { ( g ` A ) } ) ) = (/) ) |
25 |
|
disjdif |
|- ( { B } i^i ( Y \ { B } ) ) = (/) |
26 |
25
|
a1i |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( { B } i^i ( Y \ { B } ) ) = (/) ) |
27 |
|
f1oun |
|- ( ( ( { <. ( g ` A ) , B >. } : { ( g ` A ) } -1-1-onto-> { B } /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) /\ ( ( { ( g ` A ) } i^i ( Y \ { ( g ` A ) } ) ) = (/) /\ ( { B } i^i ( Y \ { B } ) ) = (/) ) ) -> ( { <. ( g ` A ) , B >. } u. h ) : ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) -1-1-onto-> ( { B } u. ( Y \ { B } ) ) ) |
28 |
21 22 24 26 27
|
syl22anc |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( { <. ( g ` A ) , B >. } u. h ) : ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) -1-1-onto-> ( { B } u. ( Y \ { B } ) ) ) |
29 |
8
|
ad2antrl |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> g : X --> Y ) |
30 |
|
simpl1 |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> A e. X ) |
31 |
29 30
|
ffvelrnd |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( g ` A ) e. Y ) |
32 |
|
uncom |
|- ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) = ( ( Y \ { ( g ` A ) } ) u. { ( g ` A ) } ) |
33 |
|
difsnid |
|- ( ( g ` A ) e. Y -> ( ( Y \ { ( g ` A ) } ) u. { ( g ` A ) } ) = Y ) |
34 |
32 33
|
eqtrid |
|- ( ( g ` A ) e. Y -> ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) = Y ) |
35 |
31 34
|
syl |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) = Y ) |
36 |
|
uncom |
|- ( { B } u. ( Y \ { B } ) ) = ( ( Y \ { B } ) u. { B } ) |
37 |
|
difsnid |
|- ( B e. Y -> ( ( Y \ { B } ) u. { B } ) = Y ) |
38 |
36 37
|
eqtrid |
|- ( B e. Y -> ( { B } u. ( Y \ { B } ) ) = Y ) |
39 |
19 38
|
syl |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( { B } u. ( Y \ { B } ) ) = Y ) |
40 |
|
f1oeq23 |
|- ( ( ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) = Y /\ ( { B } u. ( Y \ { B } ) ) = Y ) -> ( ( { <. ( g ` A ) , B >. } u. h ) : ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) -1-1-onto-> ( { B } u. ( Y \ { B } ) ) <-> ( { <. ( g ` A ) , B >. } u. h ) : Y -1-1-onto-> Y ) ) |
41 |
35 39 40
|
syl2anc |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( ( { <. ( g ` A ) , B >. } u. h ) : ( { ( g ` A ) } u. ( Y \ { ( g ` A ) } ) ) -1-1-onto-> ( { B } u. ( Y \ { B } ) ) <-> ( { <. ( g ` A ) , B >. } u. h ) : Y -1-1-onto-> Y ) ) |
42 |
28 41
|
mpbid |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( { <. ( g ` A ) , B >. } u. h ) : Y -1-1-onto-> Y ) |
43 |
|
simprl |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> g : X -1-1-onto-> Y ) |
44 |
|
f1oco |
|- ( ( ( { <. ( g ` A ) , B >. } u. h ) : Y -1-1-onto-> Y /\ g : X -1-1-onto-> Y ) -> ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) : X -1-1-onto-> Y ) |
45 |
42 43 44
|
syl2anc |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) : X -1-1-onto-> Y ) |
46 |
|
f1ofn |
|- ( g : X -1-1-onto-> Y -> g Fn X ) |
47 |
46
|
ad2antrl |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> g Fn X ) |
48 |
|
fvco2 |
|- ( ( g Fn X /\ A e. X ) -> ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) ` A ) = ( ( { <. ( g ` A ) , B >. } u. h ) ` ( g ` A ) ) ) |
49 |
47 30 48
|
syl2anc |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) ` A ) = ( ( { <. ( g ` A ) , B >. } u. h ) ` ( g ` A ) ) ) |
50 |
|
f1ofn |
|- ( { <. ( g ` A ) , B >. } : { ( g ` A ) } -1-1-onto-> { B } -> { <. ( g ` A ) , B >. } Fn { ( g ` A ) } ) |
51 |
21 50
|
syl |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> { <. ( g ` A ) , B >. } Fn { ( g ` A ) } ) |
52 |
|
f1ofn |
|- ( h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) -> h Fn ( Y \ { ( g ` A ) } ) ) |
53 |
52
|
ad2antll |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> h Fn ( Y \ { ( g ` A ) } ) ) |
54 |
17
|
snid |
|- ( g ` A ) e. { ( g ` A ) } |
55 |
54
|
a1i |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( g ` A ) e. { ( g ` A ) } ) |
56 |
|
fvun1 |
|- ( ( { <. ( g ` A ) , B >. } Fn { ( g ` A ) } /\ h Fn ( Y \ { ( g ` A ) } ) /\ ( ( { ( g ` A ) } i^i ( Y \ { ( g ` A ) } ) ) = (/) /\ ( g ` A ) e. { ( g ` A ) } ) ) -> ( ( { <. ( g ` A ) , B >. } u. h ) ` ( g ` A ) ) = ( { <. ( g ` A ) , B >. } ` ( g ` A ) ) ) |
57 |
51 53 24 55 56
|
syl112anc |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( ( { <. ( g ` A ) , B >. } u. h ) ` ( g ` A ) ) = ( { <. ( g ` A ) , B >. } ` ( g ` A ) ) ) |
58 |
|
fvsng |
|- ( ( ( g ` A ) e. _V /\ B e. Y ) -> ( { <. ( g ` A ) , B >. } ` ( g ` A ) ) = B ) |
59 |
18 19 58
|
syl2anc |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( { <. ( g ` A ) , B >. } ` ( g ` A ) ) = B ) |
60 |
49 57 59
|
3eqtrd |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) ` A ) = B ) |
61 |
|
snex |
|- { <. ( g ` A ) , B >. } e. _V |
62 |
|
vex |
|- h e. _V |
63 |
61 62
|
unex |
|- ( { <. ( g ` A ) , B >. } u. h ) e. _V |
64 |
|
vex |
|- g e. _V |
65 |
63 64
|
coex |
|- ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) e. _V |
66 |
|
f1oeq1 |
|- ( f = ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) -> ( f : X -1-1-onto-> Y <-> ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) : X -1-1-onto-> Y ) ) |
67 |
|
fveq1 |
|- ( f = ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) -> ( f ` A ) = ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) ` A ) ) |
68 |
67
|
eqeq1d |
|- ( f = ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) -> ( ( f ` A ) = B <-> ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) ` A ) = B ) ) |
69 |
66 68
|
anbi12d |
|- ( f = ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) -> ( ( f : X -1-1-onto-> Y /\ ( f ` A ) = B ) <-> ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) : X -1-1-onto-> Y /\ ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) ` A ) = B ) ) ) |
70 |
65 69
|
spcev |
|- ( ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) : X -1-1-onto-> Y /\ ( ( ( { <. ( g ` A ) , B >. } u. h ) o. g ) ` A ) = B ) -> E. f ( f : X -1-1-onto-> Y /\ ( f ` A ) = B ) ) |
71 |
45 60 70
|
syl2anc |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ ( g : X -1-1-onto-> Y /\ h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) ) ) -> E. f ( f : X -1-1-onto-> Y /\ ( f ` A ) = B ) ) |
72 |
71
|
expr |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> ( h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) -> E. f ( f : X -1-1-onto-> Y /\ ( f ` A ) = B ) ) ) |
73 |
72
|
exlimdv |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> ( E. h h : ( Y \ { ( g ` A ) } ) -1-1-onto-> ( Y \ { B } ) -> E. f ( f : X -1-1-onto-> Y /\ ( f ` A ) = B ) ) ) |
74 |
16 73
|
mpd |
|- ( ( ( A e. X /\ B e. Y /\ X ~~ Y ) /\ g : X -1-1-onto-> Y ) -> E. f ( f : X -1-1-onto-> Y /\ ( f ` A ) = B ) ) |
75 |
3 74
|
exlimddv |
|- ( ( A e. X /\ B e. Y /\ X ~~ Y ) -> E. f ( f : X -1-1-onto-> Y /\ ( f ` A ) = B ) ) |