Step | Hyp | Ref
| Expression |
1 | | f1of 6834 |
. . . . . . 7
β’ (πΉ:πβ1-1-ontoβπ β πΉ:πβΆπ) |
2 | | ffvelcdm 7084 |
. . . . . . . . 9
β’ ((πΉ:πβΆπ β§ π₯ β π) β (πΉβπ₯) β π) |
3 | 2 | ex 414 |
. . . . . . . 8
β’ (πΉ:πβΆπ β (π₯ β π β (πΉβπ₯) β π)) |
4 | | ffvelcdm 7084 |
. . . . . . . . 9
β’ ((πΉ:πβΆπ β§ π¦ β π) β (πΉβπ¦) β π) |
5 | 4 | ex 414 |
. . . . . . . 8
β’ (πΉ:πβΆπ β (π¦ β π β (πΉβπ¦) β π)) |
6 | 3, 5 | anim12d 610 |
. . . . . . 7
β’ (πΉ:πβΆπ β ((π₯ β π β§ π¦ β π) β ((πΉβπ₯) β π β§ (πΉβπ¦) β π))) |
7 | 1, 6 | syl 17 |
. . . . . 6
β’ (πΉ:πβ1-1-ontoβπ β ((π₯ β π β§ π¦ β π) β ((πΉβπ₯) β π β§ (πΉβπ¦) β π))) |
8 | | metcl 23838 |
. . . . . . 7
β’ ((π β (Metβπ) β§ (πΉβπ₯) β π β§ (πΉβπ¦) β π) β ((πΉβπ₯)π(πΉβπ¦)) β β) |
9 | 8 | 3expib 1123 |
. . . . . 6
β’ (π β (Metβπ) β (((πΉβπ₯) β π β§ (πΉβπ¦) β π) β ((πΉβπ₯)π(πΉβπ¦)) β β)) |
10 | 7, 9 | sylan9r 510 |
. . . . 5
β’ ((π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β ((π₯ β π β§ π¦ β π) β ((πΉβπ₯)π(πΉβπ¦)) β β)) |
11 | 10 | 3adant1 1131 |
. . . 4
β’ ((π β π΄ β§ π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β ((π₯ β π β§ π¦ β π) β ((πΉβπ₯)π(πΉβπ¦)) β β)) |
12 | 11 | ralrimivv 3199 |
. . 3
β’ ((π β π΄ β§ π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β βπ₯ β π βπ¦ β π ((πΉβπ₯)π(πΉβπ¦)) β β) |
13 | | metf1o.2 |
. . . 4
β’ π = (π₯ β π, π¦ β π β¦ ((πΉβπ₯)π(πΉβπ¦))) |
14 | 13 | fmpo 8054 |
. . 3
β’
(βπ₯ β
π βπ¦ β π ((πΉβπ₯)π(πΉβπ¦)) β β β π:(π Γ π)βΆβ) |
15 | 12, 14 | sylib 217 |
. 2
β’ ((π β π΄ β§ π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β π:(π Γ π)βΆβ) |
16 | | fveq2 6892 |
. . . . . . . . . . 11
β’ (π₯ = π’ β (πΉβπ₯) = (πΉβπ’)) |
17 | 16 | oveq1d 7424 |
. . . . . . . . . 10
β’ (π₯ = π’ β ((πΉβπ₯)π(πΉβπ¦)) = ((πΉβπ’)π(πΉβπ¦))) |
18 | | fveq2 6892 |
. . . . . . . . . . 11
β’ (π¦ = π£ β (πΉβπ¦) = (πΉβπ£)) |
19 | 18 | oveq2d 7425 |
. . . . . . . . . 10
β’ (π¦ = π£ β ((πΉβπ’)π(πΉβπ¦)) = ((πΉβπ’)π(πΉβπ£))) |
20 | | ovex 7442 |
. . . . . . . . . 10
β’ ((πΉβπ’)π(πΉβπ£)) β V |
21 | 17, 19, 13, 20 | ovmpo 7568 |
. . . . . . . . 9
β’ ((π’ β π β§ π£ β π) β (π’ππ£) = ((πΉβπ’)π(πΉβπ£))) |
22 | 21 | eqeq1d 2735 |
. . . . . . . 8
β’ ((π’ β π β§ π£ β π) β ((π’ππ£) = 0 β ((πΉβπ’)π(πΉβπ£)) = 0)) |
23 | 22 | adantl 483 |
. . . . . . 7
β’ (((π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π β§ π£ β π)) β ((π’ππ£) = 0 β ((πΉβπ’)π(πΉβπ£)) = 0)) |
24 | | ffvelcdm 7084 |
. . . . . . . . . . . . 13
β’ ((πΉ:πβΆπ β§ π’ β π) β (πΉβπ’) β π) |
25 | 24 | ex 414 |
. . . . . . . . . . . 12
β’ (πΉ:πβΆπ β (π’ β π β (πΉβπ’) β π)) |
26 | | ffvelcdm 7084 |
. . . . . . . . . . . . 13
β’ ((πΉ:πβΆπ β§ π£ β π) β (πΉβπ£) β π) |
27 | 26 | ex 414 |
. . . . . . . . . . . 12
β’ (πΉ:πβΆπ β (π£ β π β (πΉβπ£) β π)) |
28 | 25, 27 | anim12d 610 |
. . . . . . . . . . 11
β’ (πΉ:πβΆπ β ((π’ β π β§ π£ β π) β ((πΉβπ’) β π β§ (πΉβπ£) β π))) |
29 | 1, 28 | syl 17 |
. . . . . . . . . 10
β’ (πΉ:πβ1-1-ontoβπ β ((π’ β π β§ π£ β π) β ((πΉβπ’) β π β§ (πΉβπ£) β π))) |
30 | 29 | imp 408 |
. . . . . . . . 9
β’ ((πΉ:πβ1-1-ontoβπ β§ (π’ β π β§ π£ β π)) β ((πΉβπ’) β π β§ (πΉβπ£) β π)) |
31 | 30 | adantll 713 |
. . . . . . . 8
β’ (((π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π β§ π£ β π)) β ((πΉβπ’) β π β§ (πΉβπ£) β π)) |
32 | | meteq0 23845 |
. . . . . . . . . 10
β’ ((π β (Metβπ) β§ (πΉβπ’) β π β§ (πΉβπ£) β π) β (((πΉβπ’)π(πΉβπ£)) = 0 β (πΉβπ’) = (πΉβπ£))) |
33 | 32 | 3expb 1121 |
. . . . . . . . 9
β’ ((π β (Metβπ) β§ ((πΉβπ’) β π β§ (πΉβπ£) β π)) β (((πΉβπ’)π(πΉβπ£)) = 0 β (πΉβπ’) = (πΉβπ£))) |
34 | 33 | adantlr 714 |
. . . . . . . 8
β’ (((π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β§ ((πΉβπ’) β π β§ (πΉβπ£) β π)) β (((πΉβπ’)π(πΉβπ£)) = 0 β (πΉβπ’) = (πΉβπ£))) |
35 | 31, 34 | syldan 592 |
. . . . . . 7
β’ (((π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π β§ π£ β π)) β (((πΉβπ’)π(πΉβπ£)) = 0 β (πΉβπ’) = (πΉβπ£))) |
36 | | f1of1 6833 |
. . . . . . . . 9
β’ (πΉ:πβ1-1-ontoβπ β πΉ:πβ1-1βπ) |
37 | | f1fveq 7261 |
. . . . . . . . 9
β’ ((πΉ:πβ1-1βπ β§ (π’ β π β§ π£ β π)) β ((πΉβπ’) = (πΉβπ£) β π’ = π£)) |
38 | 36, 37 | sylan 581 |
. . . . . . . 8
β’ ((πΉ:πβ1-1-ontoβπ β§ (π’ β π β§ π£ β π)) β ((πΉβπ’) = (πΉβπ£) β π’ = π£)) |
39 | 38 | adantll 713 |
. . . . . . 7
β’ (((π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π β§ π£ β π)) β ((πΉβπ’) = (πΉβπ£) β π’ = π£)) |
40 | 23, 35, 39 | 3bitrd 305 |
. . . . . 6
β’ (((π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π β§ π£ β π)) β ((π’ππ£) = 0 β π’ = π£)) |
41 | | ffvelcdm 7084 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:πβΆπ β§ π€ β π) β (πΉβπ€) β π) |
42 | 41 | ex 414 |
. . . . . . . . . . . . . 14
β’ (πΉ:πβΆπ β (π€ β π β (πΉβπ€) β π)) |
43 | 28, 42 | anim12d 610 |
. . . . . . . . . . . . 13
β’ (πΉ:πβΆπ β (((π’ β π β§ π£ β π) β§ π€ β π) β (((πΉβπ’) β π β§ (πΉβπ£) β π) β§ (πΉβπ€) β π))) |
44 | 1, 43 | syl 17 |
. . . . . . . . . . . 12
β’ (πΉ:πβ1-1-ontoβπ β (((π’ β π β§ π£ β π) β§ π€ β π) β (((πΉβπ’) β π β§ (πΉβπ£) β π) β§ (πΉβπ€) β π))) |
45 | 44 | imp 408 |
. . . . . . . . . . 11
β’ ((πΉ:πβ1-1-ontoβπ β§ ((π’ β π β§ π£ β π) β§ π€ β π)) β (((πΉβπ’) β π β§ (πΉβπ£) β π) β§ (πΉβπ€) β π)) |
46 | 45 | adantll 713 |
. . . . . . . . . 10
β’ (((π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β§ ((π’ β π β§ π£ β π) β§ π€ β π)) β (((πΉβπ’) β π β§ (πΉβπ£) β π) β§ (πΉβπ€) β π)) |
47 | | mettri2 23847 |
. . . . . . . . . . . . . . 15
β’ ((π β (Metβπ) β§ ((πΉβπ€) β π β§ (πΉβπ’) β π β§ (πΉβπ£) β π)) β ((πΉβπ’)π(πΉβπ£)) β€ (((πΉβπ€)π(πΉβπ’)) + ((πΉβπ€)π(πΉβπ£)))) |
48 | 47 | expcom 415 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ€) β π β§ (πΉβπ’) β π β§ (πΉβπ£) β π) β (π β (Metβπ) β ((πΉβπ’)π(πΉβπ£)) β€ (((πΉβπ€)π(πΉβπ’)) + ((πΉβπ€)π(πΉβπ£))))) |
49 | 48 | 3expb 1121 |
. . . . . . . . . . . . 13
β’ (((πΉβπ€) β π β§ ((πΉβπ’) β π β§ (πΉβπ£) β π)) β (π β (Metβπ) β ((πΉβπ’)π(πΉβπ£)) β€ (((πΉβπ€)π(πΉβπ’)) + ((πΉβπ€)π(πΉβπ£))))) |
50 | 49 | ancoms 460 |
. . . . . . . . . . . 12
β’ ((((πΉβπ’) β π β§ (πΉβπ£) β π) β§ (πΉβπ€) β π) β (π β (Metβπ) β ((πΉβπ’)π(πΉβπ£)) β€ (((πΉβπ€)π(πΉβπ’)) + ((πΉβπ€)π(πΉβπ£))))) |
51 | 50 | impcom 409 |
. . . . . . . . . . 11
β’ ((π β (Metβπ) β§ (((πΉβπ’) β π β§ (πΉβπ£) β π) β§ (πΉβπ€) β π)) β ((πΉβπ’)π(πΉβπ£)) β€ (((πΉβπ€)π(πΉβπ’)) + ((πΉβπ€)π(πΉβπ£)))) |
52 | 51 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β§ (((πΉβπ’) β π β§ (πΉβπ£) β π) β§ (πΉβπ€) β π)) β ((πΉβπ’)π(πΉβπ£)) β€ (((πΉβπ€)π(πΉβπ’)) + ((πΉβπ€)π(πΉβπ£)))) |
53 | 46, 52 | syldan 592 |
. . . . . . . . 9
β’ (((π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β§ ((π’ β π β§ π£ β π) β§ π€ β π)) β ((πΉβπ’)π(πΉβπ£)) β€ (((πΉβπ€)π(πΉβπ’)) + ((πΉβπ€)π(πΉβπ£)))) |
54 | 53 | anassrs 469 |
. . . . . . . 8
β’ ((((π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π β§ π£ β π)) β§ π€ β π) β ((πΉβπ’)π(πΉβπ£)) β€ (((πΉβπ€)π(πΉβπ’)) + ((πΉβπ€)π(πΉβπ£)))) |
55 | 21 | adantr 482 |
. . . . . . . . . 10
β’ (((π’ β π β§ π£ β π) β§ π€ β π) β (π’ππ£) = ((πΉβπ’)π(πΉβπ£))) |
56 | | fveq2 6892 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π€ β (πΉβπ₯) = (πΉβπ€)) |
57 | 56 | oveq1d 7424 |
. . . . . . . . . . . . . 14
β’ (π₯ = π€ β ((πΉβπ₯)π(πΉβπ¦)) = ((πΉβπ€)π(πΉβπ¦))) |
58 | | fveq2 6892 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π’ β (πΉβπ¦) = (πΉβπ’)) |
59 | 58 | oveq2d 7425 |
. . . . . . . . . . . . . 14
β’ (π¦ = π’ β ((πΉβπ€)π(πΉβπ¦)) = ((πΉβπ€)π(πΉβπ’))) |
60 | | ovex 7442 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ€)π(πΉβπ’)) β V |
61 | 57, 59, 13, 60 | ovmpo 7568 |
. . . . . . . . . . . . 13
β’ ((π€ β π β§ π’ β π) β (π€ππ’) = ((πΉβπ€)π(πΉβπ’))) |
62 | 61 | ancoms 460 |
. . . . . . . . . . . 12
β’ ((π’ β π β§ π€ β π) β (π€ππ’) = ((πΉβπ€)π(πΉβπ’))) |
63 | 62 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π’ β π β§ π£ β π) β§ π€ β π) β (π€ππ’) = ((πΉβπ€)π(πΉβπ’))) |
64 | 18 | oveq2d 7425 |
. . . . . . . . . . . . . 14
β’ (π¦ = π£ β ((πΉβπ€)π(πΉβπ¦)) = ((πΉβπ€)π(πΉβπ£))) |
65 | | ovex 7442 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ€)π(πΉβπ£)) β V |
66 | 57, 64, 13, 65 | ovmpo 7568 |
. . . . . . . . . . . . 13
β’ ((π€ β π β§ π£ β π) β (π€ππ£) = ((πΉβπ€)π(πΉβπ£))) |
67 | 66 | ancoms 460 |
. . . . . . . . . . . 12
β’ ((π£ β π β§ π€ β π) β (π€ππ£) = ((πΉβπ€)π(πΉβπ£))) |
68 | 67 | adantll 713 |
. . . . . . . . . . 11
β’ (((π’ β π β§ π£ β π) β§ π€ β π) β (π€ππ£) = ((πΉβπ€)π(πΉβπ£))) |
69 | 63, 68 | oveq12d 7427 |
. . . . . . . . . 10
β’ (((π’ β π β§ π£ β π) β§ π€ β π) β ((π€ππ’) + (π€ππ£)) = (((πΉβπ€)π(πΉβπ’)) + ((πΉβπ€)π(πΉβπ£)))) |
70 | 55, 69 | breq12d 5162 |
. . . . . . . . 9
β’ (((π’ β π β§ π£ β π) β§ π€ β π) β ((π’ππ£) β€ ((π€ππ’) + (π€ππ£)) β ((πΉβπ’)π(πΉβπ£)) β€ (((πΉβπ€)π(πΉβπ’)) + ((πΉβπ€)π(πΉβπ£))))) |
71 | 70 | adantll 713 |
. . . . . . . 8
β’ ((((π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π β§ π£ β π)) β§ π€ β π) β ((π’ππ£) β€ ((π€ππ’) + (π€ππ£)) β ((πΉβπ’)π(πΉβπ£)) β€ (((πΉβπ€)π(πΉβπ’)) + ((πΉβπ€)π(πΉβπ£))))) |
72 | 54, 71 | mpbird 257 |
. . . . . . 7
β’ ((((π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π β§ π£ β π)) β§ π€ β π) β (π’ππ£) β€ ((π€ππ’) + (π€ππ£))) |
73 | 72 | ralrimiva 3147 |
. . . . . 6
β’ (((π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π β§ π£ β π)) β βπ€ β π (π’ππ£) β€ ((π€ππ’) + (π€ππ£))) |
74 | 40, 73 | jca 513 |
. . . . 5
β’ (((π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π β§ π£ β π)) β (((π’ππ£) = 0 β π’ = π£) β§ βπ€ β π (π’ππ£) β€ ((π€ππ’) + (π€ππ£)))) |
75 | 74 | 3adantl1 1167 |
. . . 4
β’ (((π β π΄ β§ π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β§ (π’ β π β§ π£ β π)) β (((π’ππ£) = 0 β π’ = π£) β§ βπ€ β π (π’ππ£) β€ ((π€ππ’) + (π€ππ£)))) |
76 | 75 | ex 414 |
. . 3
β’ ((π β π΄ β§ π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β ((π’ β π β§ π£ β π) β (((π’ππ£) = 0 β π’ = π£) β§ βπ€ β π (π’ππ£) β€ ((π€ππ’) + (π€ππ£))))) |
77 | 76 | ralrimivv 3199 |
. 2
β’ ((π β π΄ β§ π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β βπ’ β π βπ£ β π (((π’ππ£) = 0 β π’ = π£) β§ βπ€ β π (π’ππ£) β€ ((π€ππ’) + (π€ππ£)))) |
78 | | ismet 23829 |
. . 3
β’ (π β π΄ β (π β (Metβπ) β (π:(π Γ π)βΆβ β§ βπ’ β π βπ£ β π (((π’ππ£) = 0 β π’ = π£) β§ βπ€ β π (π’ππ£) β€ ((π€ππ’) + (π€ππ£)))))) |
79 | 78 | 3ad2ant1 1134 |
. 2
β’ ((π β π΄ β§ π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β (π β (Metβπ) β (π:(π Γ π)βΆβ β§ βπ’ β π βπ£ β π (((π’ππ£) = 0 β π’ = π£) β§ βπ€ β π (π’ππ£) β€ ((π€ππ’) + (π€ππ£)))))) |
80 | 15, 77, 79 | mpbir2and 712 |
1
β’ ((π β π΄ β§ π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β π β (Metβπ)) |