Step |
Hyp |
Ref |
Expression |
1 |
|
f1ofn |
|- ( F : A -1-1-onto-> A -> F Fn A ) |
2 |
1
|
ad2antrr |
|- ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) -> F Fn A ) |
3 |
|
f1ofn |
|- ( G : A -1-1-onto-> A -> G Fn A ) |
4 |
3
|
ad2antlr |
|- ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) -> G Fn A ) |
5 |
|
1onn |
|- 1o e. _om |
6 |
|
simplrr |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> dom ( G \ _I ) = dom ( F \ _I ) ) |
7 |
|
simplrl |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> dom ( F \ _I ) ~~ 2o ) |
8 |
|
df-2o |
|- 2o = suc 1o |
9 |
7 8
|
breqtrdi |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> dom ( F \ _I ) ~~ suc 1o ) |
10 |
6 9
|
eqbrtrd |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> dom ( G \ _I ) ~~ suc 1o ) |
11 |
|
simpr |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> x e. dom ( G \ _I ) ) |
12 |
|
dif1en |
|- ( ( 1o e. _om /\ dom ( G \ _I ) ~~ suc 1o /\ x e. dom ( G \ _I ) ) -> ( dom ( G \ _I ) \ { x } ) ~~ 1o ) |
13 |
5 10 11 12
|
mp3an2i |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> ( dom ( G \ _I ) \ { x } ) ~~ 1o ) |
14 |
|
euen1b |
|- ( ( dom ( G \ _I ) \ { x } ) ~~ 1o <-> E! y y e. ( dom ( G \ _I ) \ { x } ) ) |
15 |
|
eumo |
|- ( E! y y e. ( dom ( G \ _I ) \ { x } ) -> E* y y e. ( dom ( G \ _I ) \ { x } ) ) |
16 |
14 15
|
sylbi |
|- ( ( dom ( G \ _I ) \ { x } ) ~~ 1o -> E* y y e. ( dom ( G \ _I ) \ { x } ) ) |
17 |
13 16
|
syl |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> E* y y e. ( dom ( G \ _I ) \ { x } ) ) |
18 |
|
f1omvdmvd |
|- ( ( F : A -1-1-onto-> A /\ x e. dom ( F \ _I ) ) -> ( F ` x ) e. ( dom ( F \ _I ) \ { x } ) ) |
19 |
18
|
ex |
|- ( F : A -1-1-onto-> A -> ( x e. dom ( F \ _I ) -> ( F ` x ) e. ( dom ( F \ _I ) \ { x } ) ) ) |
20 |
19
|
ad2antrr |
|- ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) -> ( x e. dom ( F \ _I ) -> ( F ` x ) e. ( dom ( F \ _I ) \ { x } ) ) ) |
21 |
|
eleq2 |
|- ( dom ( G \ _I ) = dom ( F \ _I ) -> ( x e. dom ( G \ _I ) <-> x e. dom ( F \ _I ) ) ) |
22 |
21
|
ad2antll |
|- ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) -> ( x e. dom ( G \ _I ) <-> x e. dom ( F \ _I ) ) ) |
23 |
|
difeq1 |
|- ( dom ( G \ _I ) = dom ( F \ _I ) -> ( dom ( G \ _I ) \ { x } ) = ( dom ( F \ _I ) \ { x } ) ) |
24 |
23
|
eleq2d |
|- ( dom ( G \ _I ) = dom ( F \ _I ) -> ( ( F ` x ) e. ( dom ( G \ _I ) \ { x } ) <-> ( F ` x ) e. ( dom ( F \ _I ) \ { x } ) ) ) |
25 |
24
|
ad2antll |
|- ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) -> ( ( F ` x ) e. ( dom ( G \ _I ) \ { x } ) <-> ( F ` x ) e. ( dom ( F \ _I ) \ { x } ) ) ) |
26 |
20 22 25
|
3imtr4d |
|- ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) -> ( x e. dom ( G \ _I ) -> ( F ` x ) e. ( dom ( G \ _I ) \ { x } ) ) ) |
27 |
26
|
imp |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> ( F ` x ) e. ( dom ( G \ _I ) \ { x } ) ) |
28 |
|
f1omvdmvd |
|- ( ( G : A -1-1-onto-> A /\ x e. dom ( G \ _I ) ) -> ( G ` x ) e. ( dom ( G \ _I ) \ { x } ) ) |
29 |
28
|
ad4ant24 |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> ( G ` x ) e. ( dom ( G \ _I ) \ { x } ) ) |
30 |
|
fvex |
|- ( F ` x ) e. _V |
31 |
|
fvex |
|- ( G ` x ) e. _V |
32 |
30 31
|
pm3.2i |
|- ( ( F ` x ) e. _V /\ ( G ` x ) e. _V ) |
33 |
|
eleq1 |
|- ( y = ( F ` x ) -> ( y e. ( dom ( G \ _I ) \ { x } ) <-> ( F ` x ) e. ( dom ( G \ _I ) \ { x } ) ) ) |
34 |
|
eleq1 |
|- ( y = ( G ` x ) -> ( y e. ( dom ( G \ _I ) \ { x } ) <-> ( G ` x ) e. ( dom ( G \ _I ) \ { x } ) ) ) |
35 |
33 34
|
moi |
|- ( ( ( ( F ` x ) e. _V /\ ( G ` x ) e. _V ) /\ E* y y e. ( dom ( G \ _I ) \ { x } ) /\ ( ( F ` x ) e. ( dom ( G \ _I ) \ { x } ) /\ ( G ` x ) e. ( dom ( G \ _I ) \ { x } ) ) ) -> ( F ` x ) = ( G ` x ) ) |
36 |
32 35
|
mp3an1 |
|- ( ( E* y y e. ( dom ( G \ _I ) \ { x } ) /\ ( ( F ` x ) e. ( dom ( G \ _I ) \ { x } ) /\ ( G ` x ) e. ( dom ( G \ _I ) \ { x } ) ) ) -> ( F ` x ) = ( G ` x ) ) |
37 |
17 27 29 36
|
syl12anc |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. dom ( G \ _I ) ) -> ( F ` x ) = ( G ` x ) ) |
38 |
37
|
adantlr |
|- ( ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) /\ x e. dom ( G \ _I ) ) -> ( F ` x ) = ( G ` x ) ) |
39 |
|
simplrr |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) -> dom ( G \ _I ) = dom ( F \ _I ) ) |
40 |
39
|
eleq2d |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) -> ( x e. dom ( G \ _I ) <-> x e. dom ( F \ _I ) ) ) |
41 |
|
fnelnfp |
|- ( ( F Fn A /\ x e. A ) -> ( x e. dom ( F \ _I ) <-> ( F ` x ) =/= x ) ) |
42 |
2 41
|
sylan |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) -> ( x e. dom ( F \ _I ) <-> ( F ` x ) =/= x ) ) |
43 |
40 42
|
bitrd |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) -> ( x e. dom ( G \ _I ) <-> ( F ` x ) =/= x ) ) |
44 |
43
|
necon2bbid |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) -> ( ( F ` x ) = x <-> -. x e. dom ( G \ _I ) ) ) |
45 |
44
|
biimpar |
|- ( ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) /\ -. x e. dom ( G \ _I ) ) -> ( F ` x ) = x ) |
46 |
|
fnelnfp |
|- ( ( G Fn A /\ x e. A ) -> ( x e. dom ( G \ _I ) <-> ( G ` x ) =/= x ) ) |
47 |
4 46
|
sylan |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) -> ( x e. dom ( G \ _I ) <-> ( G ` x ) =/= x ) ) |
48 |
47
|
necon2bbid |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) -> ( ( G ` x ) = x <-> -. x e. dom ( G \ _I ) ) ) |
49 |
48
|
biimpar |
|- ( ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) /\ -. x e. dom ( G \ _I ) ) -> ( G ` x ) = x ) |
50 |
45 49
|
eqtr4d |
|- ( ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) /\ -. x e. dom ( G \ _I ) ) -> ( F ` x ) = ( G ` x ) ) |
51 |
38 50
|
pm2.61dan |
|- ( ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) /\ x e. A ) -> ( F ` x ) = ( G ` x ) ) |
52 |
2 4 51
|
eqfnfvd |
|- ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) ~~ 2o /\ dom ( G \ _I ) = dom ( F \ _I ) ) ) -> F = G ) |