Step |
Hyp |
Ref |
Expression |
1 |
|
f1ocnv |
β’ ( πΉ : π β1-1-ontoβ π β β‘ πΉ : π β1-1-ontoβ π ) |
2 |
1
|
adantr |
β’ ( ( πΉ : π β1-1-ontoβ π β§ β π₯ β π β π¦ β π ( π₯ π π¦ ) = ( ( πΉ β π₯ ) π ( πΉ β π¦ ) ) ) β β‘ πΉ : π β1-1-ontoβ π ) |
3 |
|
f1ocnvdm |
β’ ( ( πΉ : π β1-1-ontoβ π β§ π’ β π ) β ( β‘ πΉ β π’ ) β π ) |
4 |
3
|
ex |
β’ ( πΉ : π β1-1-ontoβ π β ( π’ β π β ( β‘ πΉ β π’ ) β π ) ) |
5 |
|
f1ocnvdm |
β’ ( ( πΉ : π β1-1-ontoβ π β§ π£ β π ) β ( β‘ πΉ β π£ ) β π ) |
6 |
5
|
ex |
β’ ( πΉ : π β1-1-ontoβ π β ( π£ β π β ( β‘ πΉ β π£ ) β π ) ) |
7 |
4 6
|
anim12d |
β’ ( πΉ : π β1-1-ontoβ π β ( ( π’ β π β§ π£ β π ) β ( ( β‘ πΉ β π’ ) β π β§ ( β‘ πΉ β π£ ) β π ) ) ) |
8 |
7
|
adantr |
β’ ( ( πΉ : π β1-1-ontoβ π β§ β π₯ β π β π¦ β π ( π₯ π π¦ ) = ( ( πΉ β π₯ ) π ( πΉ β π¦ ) ) ) β ( ( π’ β π β§ π£ β π ) β ( ( β‘ πΉ β π’ ) β π β§ ( β‘ πΉ β π£ ) β π ) ) ) |
9 |
8
|
imdistani |
β’ ( ( ( πΉ : π β1-1-ontoβ π β§ β π₯ β π β π¦ β π ( π₯ π π¦ ) = ( ( πΉ β π₯ ) π ( πΉ β π¦ ) ) ) β§ ( π’ β π β§ π£ β π ) ) β ( ( πΉ : π β1-1-ontoβ π β§ β π₯ β π β π¦ β π ( π₯ π π¦ ) = ( ( πΉ β π₯ ) π ( πΉ β π¦ ) ) ) β§ ( ( β‘ πΉ β π’ ) β π β§ ( β‘ πΉ β π£ ) β π ) ) ) |
10 |
|
oveq1 |
β’ ( π₯ = ( β‘ πΉ β π’ ) β ( π₯ π π¦ ) = ( ( β‘ πΉ β π’ ) π π¦ ) ) |
11 |
|
fveq2 |
β’ ( π₯ = ( β‘ πΉ β π’ ) β ( πΉ β π₯ ) = ( πΉ β ( β‘ πΉ β π’ ) ) ) |
12 |
11
|
oveq1d |
β’ ( π₯ = ( β‘ πΉ β π’ ) β ( ( πΉ β π₯ ) π ( πΉ β π¦ ) ) = ( ( πΉ β ( β‘ πΉ β π’ ) ) π ( πΉ β π¦ ) ) ) |
13 |
10 12
|
eqeq12d |
β’ ( π₯ = ( β‘ πΉ β π’ ) β ( ( π₯ π π¦ ) = ( ( πΉ β π₯ ) π ( πΉ β π¦ ) ) β ( ( β‘ πΉ β π’ ) π π¦ ) = ( ( πΉ β ( β‘ πΉ β π’ ) ) π ( πΉ β π¦ ) ) ) ) |
14 |
|
oveq2 |
β’ ( π¦ = ( β‘ πΉ β π£ ) β ( ( β‘ πΉ β π’ ) π π¦ ) = ( ( β‘ πΉ β π’ ) π ( β‘ πΉ β π£ ) ) ) |
15 |
|
fveq2 |
β’ ( π¦ = ( β‘ πΉ β π£ ) β ( πΉ β π¦ ) = ( πΉ β ( β‘ πΉ β π£ ) ) ) |
16 |
15
|
oveq2d |
β’ ( π¦ = ( β‘ πΉ β π£ ) β ( ( πΉ β ( β‘ πΉ β π’ ) ) π ( πΉ β π¦ ) ) = ( ( πΉ β ( β‘ πΉ β π’ ) ) π ( πΉ β ( β‘ πΉ β π£ ) ) ) ) |
17 |
14 16
|
eqeq12d |
β’ ( π¦ = ( β‘ πΉ β π£ ) β ( ( ( β‘ πΉ β π’ ) π π¦ ) = ( ( πΉ β ( β‘ πΉ β π’ ) ) π ( πΉ β π¦ ) ) β ( ( β‘ πΉ β π’ ) π ( β‘ πΉ β π£ ) ) = ( ( πΉ β ( β‘ πΉ β π’ ) ) π ( πΉ β ( β‘ πΉ β π£ ) ) ) ) ) |
18 |
13 17
|
rspc2v |
β’ ( ( ( β‘ πΉ β π’ ) β π β§ ( β‘ πΉ β π£ ) β π ) β ( β π₯ β π β π¦ β π ( π₯ π π¦ ) = ( ( πΉ β π₯ ) π ( πΉ β π¦ ) ) β ( ( β‘ πΉ β π’ ) π ( β‘ πΉ β π£ ) ) = ( ( πΉ β ( β‘ πΉ β π’ ) ) π ( πΉ β ( β‘ πΉ β π£ ) ) ) ) ) |
19 |
18
|
impcom |
β’ ( ( β π₯ β π β π¦ β π ( π₯ π π¦ ) = ( ( πΉ β π₯ ) π ( πΉ β π¦ ) ) β§ ( ( β‘ πΉ β π’ ) β π β§ ( β‘ πΉ β π£ ) β π ) ) β ( ( β‘ πΉ β π’ ) π ( β‘ πΉ β π£ ) ) = ( ( πΉ β ( β‘ πΉ β π’ ) ) π ( πΉ β ( β‘ πΉ β π£ ) ) ) ) |
20 |
19
|
adantll |
β’ ( ( ( πΉ : π β1-1-ontoβ π β§ β π₯ β π β π¦ β π ( π₯ π π¦ ) = ( ( πΉ β π₯ ) π ( πΉ β π¦ ) ) ) β§ ( ( β‘ πΉ β π’ ) β π β§ ( β‘ πΉ β π£ ) β π ) ) β ( ( β‘ πΉ β π’ ) π ( β‘ πΉ β π£ ) ) = ( ( πΉ β ( β‘ πΉ β π’ ) ) π ( πΉ β ( β‘ πΉ β π£ ) ) ) ) |
21 |
9 20
|
syl |
β’ ( ( ( πΉ : π β1-1-ontoβ π β§ β π₯ β π β π¦ β π ( π₯ π π¦ ) = ( ( πΉ β π₯ ) π ( πΉ β π¦ ) ) ) β§ ( π’ β π β§ π£ β π ) ) β ( ( β‘ πΉ β π’ ) π ( β‘ πΉ β π£ ) ) = ( ( πΉ β ( β‘ πΉ β π’ ) ) π ( πΉ β ( β‘ πΉ β π£ ) ) ) ) |
22 |
|
f1ocnvfv2 |
β’ ( ( πΉ : π β1-1-ontoβ π β§ π’ β π ) β ( πΉ β ( β‘ πΉ β π’ ) ) = π’ ) |
23 |
22
|
adantrr |
β’ ( ( πΉ : π β1-1-ontoβ π β§ ( π’ β π β§ π£ β π ) ) β ( πΉ β ( β‘ πΉ β π’ ) ) = π’ ) |
24 |
|
f1ocnvfv2 |
β’ ( ( πΉ : π β1-1-ontoβ π β§ π£ β π ) β ( πΉ β ( β‘ πΉ β π£ ) ) = π£ ) |
25 |
24
|
adantrl |
β’ ( ( πΉ : π β1-1-ontoβ π β§ ( π’ β π β§ π£ β π ) ) β ( πΉ β ( β‘ πΉ β π£ ) ) = π£ ) |
26 |
23 25
|
oveq12d |
β’ ( ( πΉ : π β1-1-ontoβ π β§ ( π’ β π β§ π£ β π ) ) β ( ( πΉ β ( β‘ πΉ β π’ ) ) π ( πΉ β ( β‘ πΉ β π£ ) ) ) = ( π’ π π£ ) ) |
27 |
26
|
adantlr |
β’ ( ( ( πΉ : π β1-1-ontoβ π β§ β π₯ β π β π¦ β π ( π₯ π π¦ ) = ( ( πΉ β π₯ ) π ( πΉ β π¦ ) ) ) β§ ( π’ β π β§ π£ β π ) ) β ( ( πΉ β ( β‘ πΉ β π’ ) ) π ( πΉ β ( β‘ πΉ β π£ ) ) ) = ( π’ π π£ ) ) |
28 |
21 27
|
eqtr2d |
β’ ( ( ( πΉ : π β1-1-ontoβ π β§ β π₯ β π β π¦ β π ( π₯ π π¦ ) = ( ( πΉ β π₯ ) π ( πΉ β π¦ ) ) ) β§ ( π’ β π β§ π£ β π ) ) β ( π’ π π£ ) = ( ( β‘ πΉ β π’ ) π ( β‘ πΉ β π£ ) ) ) |
29 |
28
|
ralrimivva |
β’ ( ( πΉ : π β1-1-ontoβ π β§ β π₯ β π β π¦ β π ( π₯ π π¦ ) = ( ( πΉ β π₯ ) π ( πΉ β π¦ ) ) ) β β π’ β π β π£ β π ( π’ π π£ ) = ( ( β‘ πΉ β π’ ) π ( β‘ πΉ β π£ ) ) ) |
30 |
2 29
|
jca |
β’ ( ( πΉ : π β1-1-ontoβ π β§ β π₯ β π β π¦ β π ( π₯ π π¦ ) = ( ( πΉ β π₯ ) π ( πΉ β π¦ ) ) ) β ( β‘ πΉ : π β1-1-ontoβ π β§ β π’ β π β π£ β π ( π’ π π£ ) = ( ( β‘ πΉ β π’ ) π ( β‘ πΉ β π£ ) ) ) ) |
31 |
30
|
a1i |
β’ ( ( π β ( βMet β π ) β§ π β ( βMet β π ) ) β ( ( πΉ : π β1-1-ontoβ π β§ β π₯ β π β π¦ β π ( π₯ π π¦ ) = ( ( πΉ β π₯ ) π ( πΉ β π¦ ) ) ) β ( β‘ πΉ : π β1-1-ontoβ π β§ β π’ β π β π£ β π ( π’ π π£ ) = ( ( β‘ πΉ β π’ ) π ( β‘ πΉ β π£ ) ) ) ) ) |
32 |
|
isismty |
β’ ( ( π β ( βMet β π ) β§ π β ( βMet β π ) ) β ( πΉ β ( π Ismty π ) β ( πΉ : π β1-1-ontoβ π β§ β π₯ β π β π¦ β π ( π₯ π π¦ ) = ( ( πΉ β π₯ ) π ( πΉ β π¦ ) ) ) ) ) |
33 |
|
isismty |
β’ ( ( π β ( βMet β π ) β§ π β ( βMet β π ) ) β ( β‘ πΉ β ( π Ismty π ) β ( β‘ πΉ : π β1-1-ontoβ π β§ β π’ β π β π£ β π ( π’ π π£ ) = ( ( β‘ πΉ β π’ ) π ( β‘ πΉ β π£ ) ) ) ) ) |
34 |
33
|
ancoms |
β’ ( ( π β ( βMet β π ) β§ π β ( βMet β π ) ) β ( β‘ πΉ β ( π Ismty π ) β ( β‘ πΉ : π β1-1-ontoβ π β§ β π’ β π β π£ β π ( π’ π π£ ) = ( ( β‘ πΉ β π’ ) π ( β‘ πΉ β π£ ) ) ) ) ) |
35 |
31 32 34
|
3imtr4d |
β’ ( ( π β ( βMet β π ) β§ π β ( βMet β π ) ) β ( πΉ β ( π Ismty π ) β β‘ πΉ β ( π Ismty π ) ) ) |