Step | Hyp | Ref
| Expression |
1 | | isismty 36289 |
. . . . . 6
β’ ((π β (βMetβπ) β§ π β (βMetβπ)) β (πΉ β (π Ismty π) β (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))))) |
2 | 1 | simprbda 500 |
. . . . 5
β’ (((π β (βMetβπ) β§ π β (βMetβπ)) β§ πΉ β (π Ismty π)) β πΉ:πβ1-1-ontoβπ) |
3 | 2 | adantrr 716 |
. . . 4
β’ (((π β (βMetβπ) β§ π β (βMetβπ)) β§ (πΉ β (π Ismty π) β§ π΄ β π)) β πΉ:πβ1-1-ontoβπ) |
4 | | f1of1 6788 |
. . . 4
β’ (πΉ:πβ1-1-ontoβπ β πΉ:πβ1-1βπ) |
5 | 3, 4 | syl 17 |
. . 3
β’ (((π β (βMetβπ) β§ π β (βMetβπ)) β§ (πΉ β (π Ismty π) β§ π΄ β π)) β πΉ:πβ1-1βπ) |
6 | | simprr 772 |
. . 3
β’ (((π β (βMetβπ) β§ π β (βMetβπ)) β§ (πΉ β (π Ismty π) β§ π΄ β π)) β π΄ β π) |
7 | | f1ores 6803 |
. . 3
β’ ((πΉ:πβ1-1βπ β§ π΄ β π) β (πΉ βΎ π΄):π΄β1-1-ontoβ(πΉ β π΄)) |
8 | 5, 6, 7 | syl2anc 585 |
. 2
β’ (((π β (βMetβπ) β§ π β (βMetβπ)) β§ (πΉ β (π Ismty π) β§ π΄ β π)) β (πΉ βΎ π΄):π΄β1-1-ontoβ(πΉ β π΄)) |
9 | 1 | biimpa 478 |
. . . 4
β’ (((π β (βMetβπ) β§ π β (βMetβπ)) β§ πΉ β (π Ismty π)) β (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)))) |
10 | 9 | adantrr 716 |
. . 3
β’ (((π β (βMetβπ) β§ π β (βMetβπ)) β§ (πΉ β (π Ismty π) β§ π΄ β π)) β (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)))) |
11 | | ssel 3942 |
. . . . . . . . . . . . 13
β’ (π΄ β π β (π’ β π΄ β π’ β π)) |
12 | | ssel 3942 |
. . . . . . . . . . . . 13
β’ (π΄ β π β (π£ β π΄ β π£ β π)) |
13 | 11, 12 | anim12d 610 |
. . . . . . . . . . . 12
β’ (π΄ β π β ((π’ β π΄ β§ π£ β π΄) β (π’ β π β§ π£ β π))) |
14 | 13 | imp 408 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ β π β§ π£ β π)) |
15 | | oveq1 7369 |
. . . . . . . . . . . . 13
β’ (π₯ = π’ β (π₯ππ¦) = (π’ππ¦)) |
16 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π₯ = π’ β (πΉβπ₯) = (πΉβπ’)) |
17 | 16 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (π₯ = π’ β ((πΉβπ₯)π(πΉβπ¦)) = ((πΉβπ’)π(πΉβπ¦))) |
18 | 15, 17 | eqeq12d 2753 |
. . . . . . . . . . . 12
β’ (π₯ = π’ β ((π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)) β (π’ππ¦) = ((πΉβπ’)π(πΉβπ¦)))) |
19 | | oveq2 7370 |
. . . . . . . . . . . . 13
β’ (π¦ = π£ β (π’ππ¦) = (π’ππ£)) |
20 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π¦ = π£ β (πΉβπ¦) = (πΉβπ£)) |
21 | 20 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (π¦ = π£ β ((πΉβπ’)π(πΉβπ¦)) = ((πΉβπ’)π(πΉβπ£))) |
22 | 19, 21 | eqeq12d 2753 |
. . . . . . . . . . . 12
β’ (π¦ = π£ β ((π’ππ¦) = ((πΉβπ’)π(πΉβπ¦)) β (π’ππ£) = ((πΉβπ’)π(πΉβπ£)))) |
23 | 18, 22 | rspc2v 3593 |
. . . . . . . . . . 11
β’ ((π’ β π β§ π£ β π) β (βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)) β (π’ππ£) = ((πΉβπ’)π(πΉβπ£)))) |
24 | 14, 23 | syl 17 |
. . . . . . . . . 10
β’ ((π΄ β π β§ (π’ β π΄ β§ π£ β π΄)) β (βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)) β (π’ππ£) = ((πΉβπ’)π(πΉβπ£)))) |
25 | 24 | imp 408 |
. . . . . . . . 9
β’ (((π΄ β π β§ (π’ β π΄ β§ π£ β π΄)) β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β (π’ππ£) = ((πΉβπ’)π(πΉβπ£))) |
26 | 25 | an32s 651 |
. . . . . . . 8
β’ (((π΄ β π β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β§ (π’ β π΄ β§ π£ β π΄)) β (π’ππ£) = ((πΉβπ’)π(πΉβπ£))) |
27 | 26 | adantlrl 719 |
. . . . . . 7
β’ (((π΄ β π β§ (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)))) β§ (π’ β π΄ β§ π£ β π΄)) β (π’ππ£) = ((πΉβπ’)π(πΉβπ£))) |
28 | 27 | adantlll 717 |
. . . . . 6
β’
(((((π β
(βMetβπ) β§
π β
(βMetβπ)) β§
π΄ β π) β§ (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)))) β§ (π’ β π΄ β§ π£ β π΄)) β (π’ππ£) = ((πΉβπ’)π(πΉβπ£))) |
29 | | ismtyres.3 |
. . . . . . . . 9
β’ π = (π βΎ (π΄ Γ π΄)) |
30 | 29 | oveqi 7375 |
. . . . . . . 8
β’ (π’ππ£) = (π’(π βΎ (π΄ Γ π΄))π£) |
31 | | ovres 7525 |
. . . . . . . 8
β’ ((π’ β π΄ β§ π£ β π΄) β (π’(π βΎ (π΄ Γ π΄))π£) = (π’ππ£)) |
32 | 30, 31 | eqtrid 2789 |
. . . . . . 7
β’ ((π’ β π΄ β§ π£ β π΄) β (π’ππ£) = (π’ππ£)) |
33 | 32 | adantl 483 |
. . . . . 6
β’
(((((π β
(βMetβπ) β§
π β
(βMetβπ)) β§
π΄ β π) β§ (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)))) β§ (π’ β π΄ β§ π£ β π΄)) β (π’ππ£) = (π’ππ£)) |
34 | | fvres 6866 |
. . . . . . . . . . 11
β’ (π’ β π΄ β ((πΉ βΎ π΄)βπ’) = (πΉβπ’)) |
35 | 34 | ad2antrl 727 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π΄ β§ π£ β π΄)) β ((πΉ βΎ π΄)βπ’) = (πΉβπ’)) |
36 | | fvres 6866 |
. . . . . . . . . . 11
β’ (π£ β π΄ β ((πΉ βΎ π΄)βπ£) = (πΉβπ£)) |
37 | 36 | ad2antll 728 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π΄ β§ π£ β π΄)) β ((πΉ βΎ π΄)βπ£) = (πΉβπ£)) |
38 | 35, 37 | oveq12d 7380 |
. . . . . . . . 9
β’ (((π΄ β π β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π΄ β§ π£ β π΄)) β (((πΉ βΎ π΄)βπ’)π((πΉ βΎ π΄)βπ£)) = ((πΉβπ’)π(πΉβπ£))) |
39 | | ismtyres.4 |
. . . . . . . . . . 11
β’ π = (π βΎ (π΅ Γ π΅)) |
40 | 39 | oveqi 7375 |
. . . . . . . . . 10
β’ ((πΉβπ’)π(πΉβπ£)) = ((πΉβπ’)(π βΎ (π΅ Γ π΅))(πΉβπ£)) |
41 | | f1ofun 6791 |
. . . . . . . . . . . . . . . 16
β’ (πΉ:πβ1-1-ontoβπ β Fun πΉ) |
42 | 41 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β π β§ πΉ:πβ1-1-ontoβπ) β Fun πΉ) |
43 | | f1odm 6793 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ:πβ1-1-ontoβπ β dom πΉ = π) |
44 | 43 | sseq2d 3981 |
. . . . . . . . . . . . . . . 16
β’ (πΉ:πβ1-1-ontoβπ β (π΄ β dom πΉ β π΄ β π)) |
45 | 44 | biimparc 481 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β π β§ πΉ:πβ1-1-ontoβπ) β π΄ β dom πΉ) |
46 | | funfvima2 7186 |
. . . . . . . . . . . . . . 15
β’ ((Fun
πΉ β§ π΄ β dom πΉ) β (π’ β π΄ β (πΉβπ’) β (πΉ β π΄))) |
47 | 42, 45, 46 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π΄ β π β§ πΉ:πβ1-1-ontoβπ) β (π’ β π΄ β (πΉβπ’) β (πΉ β π΄))) |
48 | 47 | imp 408 |
. . . . . . . . . . . . 13
β’ (((π΄ β π β§ πΉ:πβ1-1-ontoβπ) β§ π’ β π΄) β (πΉβπ’) β (πΉ β π΄)) |
49 | | ismtyres.2 |
. . . . . . . . . . . . 13
β’ π΅ = (πΉ β π΄) |
50 | 48, 49 | eleqtrrdi 2849 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ πΉ:πβ1-1-ontoβπ) β§ π’ β π΄) β (πΉβπ’) β π΅) |
51 | 50 | adantrr 716 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π΄ β§ π£ β π΄)) β (πΉβπ’) β π΅) |
52 | | funfvima2 7186 |
. . . . . . . . . . . . . . 15
β’ ((Fun
πΉ β§ π΄ β dom πΉ) β (π£ β π΄ β (πΉβπ£) β (πΉ β π΄))) |
53 | 42, 45, 52 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π΄ β π β§ πΉ:πβ1-1-ontoβπ) β (π£ β π΄ β (πΉβπ£) β (πΉ β π΄))) |
54 | 53 | imp 408 |
. . . . . . . . . . . . 13
β’ (((π΄ β π β§ πΉ:πβ1-1-ontoβπ) β§ π£ β π΄) β (πΉβπ£) β (πΉ β π΄)) |
55 | 54, 49 | eleqtrrdi 2849 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ πΉ:πβ1-1-ontoβπ) β§ π£ β π΄) β (πΉβπ£) β π΅) |
56 | 55 | adantrl 715 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π΄ β§ π£ β π΄)) β (πΉβπ£) β π΅) |
57 | 51, 56 | ovresd 7526 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π΄ β§ π£ β π΄)) β ((πΉβπ’)(π βΎ (π΅ Γ π΅))(πΉβπ£)) = ((πΉβπ’)π(πΉβπ£))) |
58 | 40, 57 | eqtrid 2789 |
. . . . . . . . 9
β’ (((π΄ β π β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π΄ β§ π£ β π΄)) β ((πΉβπ’)π(πΉβπ£)) = ((πΉβπ’)π(πΉβπ£))) |
59 | 38, 58 | eqtrd 2777 |
. . . . . . . 8
β’ (((π΄ β π β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π΄ β§ π£ β π΄)) β (((πΉ βΎ π΄)βπ’)π((πΉ βΎ π΄)βπ£)) = ((πΉβπ’)π(πΉβπ£))) |
60 | 59 | adantlrr 720 |
. . . . . . 7
β’ (((π΄ β π β§ (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)))) β§ (π’ β π΄ β§ π£ β π΄)) β (((πΉ βΎ π΄)βπ’)π((πΉ βΎ π΄)βπ£)) = ((πΉβπ’)π(πΉβπ£))) |
61 | 60 | adantlll 717 |
. . . . . 6
β’
(((((π β
(βMetβπ) β§
π β
(βMetβπ)) β§
π΄ β π) β§ (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)))) β§ (π’ β π΄ β§ π£ β π΄)) β (((πΉ βΎ π΄)βπ’)π((πΉ βΎ π΄)βπ£)) = ((πΉβπ’)π(πΉβπ£))) |
62 | 28, 33, 61 | 3eqtr4d 2787 |
. . . . 5
β’
(((((π β
(βMetβπ) β§
π β
(βMetβπ)) β§
π΄ β π) β§ (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)))) β§ (π’ β π΄ β§ π£ β π΄)) β (π’ππ£) = (((πΉ βΎ π΄)βπ’)π((πΉ βΎ π΄)βπ£))) |
63 | 62 | ralrimivva 3198 |
. . . 4
β’ ((((π β (βMetβπ) β§ π β (βMetβπ)) β§ π΄ β π) β§ (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)))) β βπ’ β π΄ βπ£ β π΄ (π’ππ£) = (((πΉ βΎ π΄)βπ’)π((πΉ βΎ π΄)βπ£))) |
64 | 63 | adantlrl 719 |
. . 3
β’ ((((π β (βMetβπ) β§ π β (βMetβπ)) β§ (πΉ β (π Ismty π) β§ π΄ β π)) β§ (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)))) β βπ’ β π΄ βπ£ β π΄ (π’ππ£) = (((πΉ βΎ π΄)βπ’)π((πΉ βΎ π΄)βπ£))) |
65 | 10, 64 | mpdan 686 |
. 2
β’ (((π β (βMetβπ) β§ π β (βMetβπ)) β§ (πΉ β (π Ismty π) β§ π΄ β π)) β βπ’ β π΄ βπ£ β π΄ (π’ππ£) = (((πΉ βΎ π΄)βπ’)π((πΉ βΎ π΄)βπ£))) |
66 | | xmetres2 23730 |
. . . . 5
β’ ((π β (βMetβπ) β§ π΄ β π) β (π βΎ (π΄ Γ π΄)) β (βMetβπ΄)) |
67 | 29, 66 | eqeltrid 2842 |
. . . 4
β’ ((π β (βMetβπ) β§ π΄ β π) β π β (βMetβπ΄)) |
68 | 67 | ad2ant2rl 748 |
. . 3
β’ (((π β (βMetβπ) β§ π β (βMetβπ)) β§ (πΉ β (π Ismty π) β§ π΄ β π)) β π β (βMetβπ΄)) |
69 | | simplr 768 |
. . . . . 6
β’ (((π β (βMetβπ) β§ π β (βMetβπ)) β§ (πΉ β (π Ismty π) β§ π΄ β π)) β π β (βMetβπ)) |
70 | | imassrn 6029 |
. . . . . . . 8
β’ (πΉ β π΄) β ran πΉ |
71 | 49, 70 | eqsstri 3983 |
. . . . . . 7
β’ π΅ β ran πΉ |
72 | | f1ofo 6796 |
. . . . . . . 8
β’ (πΉ:πβ1-1-ontoβπ β πΉ:πβontoβπ) |
73 | | forn 6764 |
. . . . . . . 8
β’ (πΉ:πβontoβπ β ran πΉ = π) |
74 | 3, 72, 73 | 3syl 18 |
. . . . . . 7
β’ (((π β (βMetβπ) β§ π β (βMetβπ)) β§ (πΉ β (π Ismty π) β§ π΄ β π)) β ran πΉ = π) |
75 | 71, 74 | sseqtrid 4001 |
. . . . . 6
β’ (((π β (βMetβπ) β§ π β (βMetβπ)) β§ (πΉ β (π Ismty π) β§ π΄ β π)) β π΅ β π) |
76 | | xmetres2 23730 |
. . . . . 6
β’ ((π β (βMetβπ) β§ π΅ β π) β (π βΎ (π΅ Γ π΅)) β (βMetβπ΅)) |
77 | 69, 75, 76 | syl2anc 585 |
. . . . 5
β’ (((π β (βMetβπ) β§ π β (βMetβπ)) β§ (πΉ β (π Ismty π) β§ π΄ β π)) β (π βΎ (π΅ Γ π΅)) β (βMetβπ΅)) |
78 | 39, 77 | eqeltrid 2842 |
. . . 4
β’ (((π β (βMetβπ) β§ π β (βMetβπ)) β§ (πΉ β (π Ismty π) β§ π΄ β π)) β π β (βMetβπ΅)) |
79 | 49 | fveq2i 6850 |
. . . 4
β’
(βMetβπ΅)
= (βMetβ(πΉ
β π΄)) |
80 | 78, 79 | eleqtrdi 2848 |
. . 3
β’ (((π β (βMetβπ) β§ π β (βMetβπ)) β§ (πΉ β (π Ismty π) β§ π΄ β π)) β π β (βMetβ(πΉ β π΄))) |
81 | | isismty 36289 |
. . 3
β’ ((π β (βMetβπ΄) β§ π β (βMetβ(πΉ β π΄))) β ((πΉ βΎ π΄) β (π Ismty π) β ((πΉ βΎ π΄):π΄β1-1-ontoβ(πΉ β π΄) β§ βπ’ β π΄ βπ£ β π΄ (π’ππ£) = (((πΉ βΎ π΄)βπ’)π((πΉ βΎ π΄)βπ£))))) |
82 | 68, 80, 81 | syl2anc 585 |
. 2
β’ (((π β (βMetβπ) β§ π β (βMetβπ)) β§ (πΉ β (π Ismty π) β§ π΄ β π)) β ((πΉ βΎ π΄) β (π Ismty π) β ((πΉ βΎ π΄):π΄β1-1-ontoβ(πΉ β π΄) β§ βπ’ β π΄ βπ£ β π΄ (π’ππ£) = (((πΉ βΎ π΄)βπ’)π((πΉ βΎ π΄)βπ£))))) |
83 | 8, 65, 82 | mpbir2and 712 |
1
β’ (((π β (βMetβπ) β§ π β (βMetβπ)) β§ (πΉ β (π Ismty π) β§ π΄ β π)) β (πΉ βΎ π΄) β (π Ismty π)) |