Step | Hyp | Ref
| Expression |
1 | | f1ocnv 6800 |
. . . . 5
β’ (πΉ:πβ1-1-ontoβπ β β‘πΉ:πβ1-1-ontoβπ) |
2 | 1 | adantr 482 |
. . . 4
β’ ((πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β β‘πΉ:πβ1-1-ontoβπ) |
3 | | f1ocnvdm 7235 |
. . . . . . . . . . 11
β’ ((πΉ:πβ1-1-ontoβπ β§ π’ β π) β (β‘πΉβπ’) β π) |
4 | 3 | ex 414 |
. . . . . . . . . 10
β’ (πΉ:πβ1-1-ontoβπ β (π’ β π β (β‘πΉβπ’) β π)) |
5 | | f1ocnvdm 7235 |
. . . . . . . . . . 11
β’ ((πΉ:πβ1-1-ontoβπ β§ π£ β π) β (β‘πΉβπ£) β π) |
6 | 5 | ex 414 |
. . . . . . . . . 10
β’ (πΉ:πβ1-1-ontoβπ β (π£ β π β (β‘πΉβπ£) β π)) |
7 | 4, 6 | anim12d 610 |
. . . . . . . . 9
β’ (πΉ:πβ1-1-ontoβπ β ((π’ β π β§ π£ β π) β ((β‘πΉβπ’) β π β§ (β‘πΉβπ£) β π))) |
8 | 7 | adantr 482 |
. . . . . . . 8
β’ ((πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β ((π’ β π β§ π£ β π) β ((β‘πΉβπ’) β π β§ (β‘πΉβπ£) β π))) |
9 | 8 | imdistani 570 |
. . . . . . 7
β’ (((πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β§ (π’ β π β§ π£ β π)) β ((πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β§ ((β‘πΉβπ’) β π β§ (β‘πΉβπ£) β π))) |
10 | | oveq1 7368 |
. . . . . . . . . . 11
β’ (π₯ = (β‘πΉβπ’) β (π₯ππ¦) = ((β‘πΉβπ’)ππ¦)) |
11 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π₯ = (β‘πΉβπ’) β (πΉβπ₯) = (πΉβ(β‘πΉβπ’))) |
12 | 11 | oveq1d 7376 |
. . . . . . . . . . 11
β’ (π₯ = (β‘πΉβπ’) β ((πΉβπ₯)π(πΉβπ¦)) = ((πΉβ(β‘πΉβπ’))π(πΉβπ¦))) |
13 | 10, 12 | eqeq12d 2749 |
. . . . . . . . . 10
β’ (π₯ = (β‘πΉβπ’) β ((π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)) β ((β‘πΉβπ’)ππ¦) = ((πΉβ(β‘πΉβπ’))π(πΉβπ¦)))) |
14 | | oveq2 7369 |
. . . . . . . . . . 11
β’ (π¦ = (β‘πΉβπ£) β ((β‘πΉβπ’)ππ¦) = ((β‘πΉβπ’)π(β‘πΉβπ£))) |
15 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π¦ = (β‘πΉβπ£) β (πΉβπ¦) = (πΉβ(β‘πΉβπ£))) |
16 | 15 | oveq2d 7377 |
. . . . . . . . . . 11
β’ (π¦ = (β‘πΉβπ£) β ((πΉβ(β‘πΉβπ’))π(πΉβπ¦)) = ((πΉβ(β‘πΉβπ’))π(πΉβ(β‘πΉβπ£)))) |
17 | 14, 16 | eqeq12d 2749 |
. . . . . . . . . 10
β’ (π¦ = (β‘πΉβπ£) β (((β‘πΉβπ’)ππ¦) = ((πΉβ(β‘πΉβπ’))π(πΉβπ¦)) β ((β‘πΉβπ’)π(β‘πΉβπ£)) = ((πΉβ(β‘πΉβπ’))π(πΉβ(β‘πΉβπ£))))) |
18 | 13, 17 | rspc2v 3592 |
. . . . . . . . 9
β’ (((β‘πΉβπ’) β π β§ (β‘πΉβπ£) β π) β (βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)) β ((β‘πΉβπ’)π(β‘πΉβπ£)) = ((πΉβ(β‘πΉβπ’))π(πΉβ(β‘πΉβπ£))))) |
19 | 18 | impcom 409 |
. . . . . . . 8
β’
((βπ₯ β
π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)) β§ ((β‘πΉβπ’) β π β§ (β‘πΉβπ£) β π)) β ((β‘πΉβπ’)π(β‘πΉβπ£)) = ((πΉβ(β‘πΉβπ’))π(πΉβ(β‘πΉβπ£)))) |
20 | 19 | adantll 713 |
. . . . . . 7
β’ (((πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β§ ((β‘πΉβπ’) β π β§ (β‘πΉβπ£) β π)) β ((β‘πΉβπ’)π(β‘πΉβπ£)) = ((πΉβ(β‘πΉβπ’))π(πΉβ(β‘πΉβπ£)))) |
21 | 9, 20 | syl 17 |
. . . . . 6
β’ (((πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β§ (π’ β π β§ π£ β π)) β ((β‘πΉβπ’)π(β‘πΉβπ£)) = ((πΉβ(β‘πΉβπ’))π(πΉβ(β‘πΉβπ£)))) |
22 | | f1ocnvfv2 7227 |
. . . . . . . . 9
β’ ((πΉ:πβ1-1-ontoβπ β§ π’ β π) β (πΉβ(β‘πΉβπ’)) = π’) |
23 | 22 | adantrr 716 |
. . . . . . . 8
β’ ((πΉ:πβ1-1-ontoβπ β§ (π’ β π β§ π£ β π)) β (πΉβ(β‘πΉβπ’)) = π’) |
24 | | f1ocnvfv2 7227 |
. . . . . . . . 9
β’ ((πΉ:πβ1-1-ontoβπ β§ π£ β π) β (πΉβ(β‘πΉβπ£)) = π£) |
25 | 24 | adantrl 715 |
. . . . . . . 8
β’ ((πΉ:πβ1-1-ontoβπ β§ (π’ β π β§ π£ β π)) β (πΉβ(β‘πΉβπ£)) = π£) |
26 | 23, 25 | oveq12d 7379 |
. . . . . . 7
β’ ((πΉ:πβ1-1-ontoβπ β§ (π’ β π β§ π£ β π)) β ((πΉβ(β‘πΉβπ’))π(πΉβ(β‘πΉβπ£))) = (π’ππ£)) |
27 | 26 | adantlr 714 |
. . . . . 6
β’ (((πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β§ (π’ β π β§ π£ β π)) β ((πΉβ(β‘πΉβπ’))π(πΉβ(β‘πΉβπ£))) = (π’ππ£)) |
28 | 21, 27 | eqtr2d 2774 |
. . . . 5
β’ (((πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β§ (π’ β π β§ π£ β π)) β (π’ππ£) = ((β‘πΉβπ’)π(β‘πΉβπ£))) |
29 | 28 | ralrimivva 3194 |
. . . 4
β’ ((πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β βπ’ β π βπ£ β π (π’ππ£) = ((β‘πΉβπ’)π(β‘πΉβπ£))) |
30 | 2, 29 | jca 513 |
. . 3
β’ ((πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β (β‘πΉ:πβ1-1-ontoβπ β§ βπ’ β π βπ£ β π (π’ππ£) = ((β‘πΉβπ’)π(β‘πΉβπ£)))) |
31 | 30 | a1i 11 |
. 2
β’ ((π β (βMetβπ) β§ π β (βMetβπ)) β ((πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β (β‘πΉ:πβ1-1-ontoβπ β§ βπ’ β π βπ£ β π (π’ππ£) = ((β‘πΉβπ’)π(β‘πΉβπ£))))) |
32 | | isismty 36310 |
. 2
β’ ((π β (βMetβπ) β§ π β (βMetβπ)) β (πΉ β (π Ismty π) β (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))))) |
33 | | isismty 36310 |
. . 3
β’ ((π β (βMetβπ) β§ π β (βMetβπ)) β (β‘πΉ β (π Ismty π) β (β‘πΉ:πβ1-1-ontoβπ β§ βπ’ β π βπ£ β π (π’ππ£) = ((β‘πΉβπ’)π(β‘πΉβπ£))))) |
34 | 33 | ancoms 460 |
. 2
β’ ((π β (βMetβπ) β§ π β (βMetβπ)) β (β‘πΉ β (π Ismty π) β (β‘πΉ:πβ1-1-ontoβπ β§ βπ’ β π βπ£ β π (π’ππ£) = ((β‘πΉβπ’)π(β‘πΉβπ£))))) |
35 | 31, 32, 34 | 3imtr4d 294 |
1
β’ ((π β (βMetβπ) β§ π β (βMetβπ)) β (πΉ β (π Ismty π) β β‘πΉ β (π Ismty π))) |