Step |
Hyp |
Ref |
Expression |
1 |
|
fmpt.1 |
|- F = ( x e. A |-> C ) |
2 |
|
ffn |
|- ( F : A --> B -> F Fn A ) |
3 |
|
dff1o4 |
|- ( F : A -1-1-onto-> B <-> ( F Fn A /\ `' F Fn B ) ) |
4 |
3
|
baib |
|- ( F Fn A -> ( F : A -1-1-onto-> B <-> `' F Fn B ) ) |
5 |
2 4
|
syl |
|- ( F : A --> B -> ( F : A -1-1-onto-> B <-> `' F Fn B ) ) |
6 |
|
fnres |
|- ( ( `' F |` B ) Fn B <-> A. y e. B E! z y `' F z ) |
7 |
|
nfcv |
|- F/_ x z |
8 |
|
nfmpt1 |
|- F/_ x ( x e. A |-> C ) |
9 |
1 8
|
nfcxfr |
|- F/_ x F |
10 |
|
nfcv |
|- F/_ x y |
11 |
7 9 10
|
nfbr |
|- F/ x z F y |
12 |
|
nfv |
|- F/ z ( x e. A /\ y = C ) |
13 |
|
breq1 |
|- ( z = x -> ( z F y <-> x F y ) ) |
14 |
|
df-mpt |
|- ( x e. A |-> C ) = { <. x , y >. | ( x e. A /\ y = C ) } |
15 |
1 14
|
eqtri |
|- F = { <. x , y >. | ( x e. A /\ y = C ) } |
16 |
15
|
breqi |
|- ( x F y <-> x { <. x , y >. | ( x e. A /\ y = C ) } y ) |
17 |
|
df-br |
|- ( x { <. x , y >. | ( x e. A /\ y = C ) } y <-> <. x , y >. e. { <. x , y >. | ( x e. A /\ y = C ) } ) |
18 |
|
opabidw |
|- ( <. x , y >. e. { <. x , y >. | ( x e. A /\ y = C ) } <-> ( x e. A /\ y = C ) ) |
19 |
17 18
|
bitri |
|- ( x { <. x , y >. | ( x e. A /\ y = C ) } y <-> ( x e. A /\ y = C ) ) |
20 |
16 19
|
bitri |
|- ( x F y <-> ( x e. A /\ y = C ) ) |
21 |
13 20
|
bitrdi |
|- ( z = x -> ( z F y <-> ( x e. A /\ y = C ) ) ) |
22 |
11 12 21
|
cbveuw |
|- ( E! z z F y <-> E! x ( x e. A /\ y = C ) ) |
23 |
|
vex |
|- y e. _V |
24 |
|
vex |
|- z e. _V |
25 |
23 24
|
brcnv |
|- ( y `' F z <-> z F y ) |
26 |
25
|
eubii |
|- ( E! z y `' F z <-> E! z z F y ) |
27 |
|
df-reu |
|- ( E! x e. A y = C <-> E! x ( x e. A /\ y = C ) ) |
28 |
22 26 27
|
3bitr4i |
|- ( E! z y `' F z <-> E! x e. A y = C ) |
29 |
28
|
ralbii |
|- ( A. y e. B E! z y `' F z <-> A. y e. B E! x e. A y = C ) |
30 |
6 29
|
bitri |
|- ( ( `' F |` B ) Fn B <-> A. y e. B E! x e. A y = C ) |
31 |
|
relcnv |
|- Rel `' F |
32 |
|
df-rn |
|- ran F = dom `' F |
33 |
|
frn |
|- ( F : A --> B -> ran F C_ B ) |
34 |
32 33
|
eqsstrrid |
|- ( F : A --> B -> dom `' F C_ B ) |
35 |
|
relssres |
|- ( ( Rel `' F /\ dom `' F C_ B ) -> ( `' F |` B ) = `' F ) |
36 |
31 34 35
|
sylancr |
|- ( F : A --> B -> ( `' F |` B ) = `' F ) |
37 |
36
|
fneq1d |
|- ( F : A --> B -> ( ( `' F |` B ) Fn B <-> `' F Fn B ) ) |
38 |
30 37
|
bitr3id |
|- ( F : A --> B -> ( A. y e. B E! x e. A y = C <-> `' F Fn B ) ) |
39 |
5 38
|
bitr4d |
|- ( F : A --> B -> ( F : A -1-1-onto-> B <-> A. y e. B E! x e. A y = C ) ) |
40 |
39
|
pm5.32i |
|- ( ( F : A --> B /\ F : A -1-1-onto-> B ) <-> ( F : A --> B /\ A. y e. B E! x e. A y = C ) ) |
41 |
|
f1of |
|- ( F : A -1-1-onto-> B -> F : A --> B ) |
42 |
41
|
pm4.71ri |
|- ( F : A -1-1-onto-> B <-> ( F : A --> B /\ F : A -1-1-onto-> B ) ) |
43 |
1
|
fmpt |
|- ( A. x e. A C e. B <-> F : A --> B ) |
44 |
43
|
anbi1i |
|- ( ( A. x e. A C e. B /\ A. y e. B E! x e. A y = C ) <-> ( F : A --> B /\ A. y e. B E! x e. A y = C ) ) |
45 |
40 42 44
|
3bitr4i |
|- ( F : A -1-1-onto-> B <-> ( A. x e. A C e. B /\ A. y e. B E! x e. A y = C ) ) |