Step | Hyp | Ref
| Expression |
1 | | 0ex 5284 |
. . . . . . 7
β’ β
β V |
2 | 1 | snid 4642 |
. . . . . 6
β’ β
β {β
} |
3 | 2 | a1i 11 |
. . . . 5
β’ ((π β§ π = β
) β β
β
{β
}) |
4 | | hoiqssbl.y |
. . . . . . . . 9
β’ (π β π β (β βm π)) |
5 | 4 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π = β
) β π β (β βm π)) |
6 | | oveq2 7385 |
. . . . . . . . . 10
β’ (π = β
β (β
βm π) =
(β βm β
)) |
7 | | reex 11166 |
. . . . . . . . . . . 12
β’ β
β V |
8 | | mapdm0 8802 |
. . . . . . . . . . . 12
β’ (β
β V β (β βm β
) =
{β
}) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . . 11
β’ (β
βm β
) = {β
} |
10 | 9 | a1i 11 |
. . . . . . . . . 10
β’ (π = β
β (β
βm β
) = {β
}) |
11 | 6, 10 | eqtrd 2771 |
. . . . . . . . 9
β’ (π = β
β (β
βm π) =
{β
}) |
12 | 11 | adantl 482 |
. . . . . . . 8
β’ ((π β§ π = β
) β (β
βm π) =
{β
}) |
13 | 5, 12 | eleqtrd 2834 |
. . . . . . 7
β’ ((π β§ π = β
) β π β {β
}) |
14 | | 0fin 9137 |
. . . . . . . . . . . . 13
β’ β
β Fin |
15 | | eqid 2731 |
. . . . . . . . . . . . . 14
β’
(distβ(β^ββ
)) =
(distβ(β^ββ
)) |
16 | 15 | rrxmetfi 24828 |
. . . . . . . . . . . . 13
β’ (β
β Fin β (distβ(β^ββ
)) β
(Metβ(β βm β
))) |
17 | 14, 16 | ax-mp 5 |
. . . . . . . . . . . 12
β’
(distβ(β^ββ
)) β (Metβ(β
βm β
)) |
18 | | metxmet 23739 |
. . . . . . . . . . . 12
β’
((distβ(β^ββ
)) β (Metβ(β
βm β
)) β (distβ(β^ββ
))
β (βMetβ(β βm
β
))) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . 11
β’
(distβ(β^ββ
)) β (βMetβ(β
βm β
)) |
20 | 19 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π = β
) β
(distβ(β^ββ
)) β (βMetβ(β
βm β
))) |
21 | 3, 9 | eleqtrrdi 2843 |
. . . . . . . . . 10
β’ ((π β§ π = β
) β β
β (β
βm β
)) |
22 | | hoiqssbl.e |
. . . . . . . . . . 11
β’ (π β πΈ β
β+) |
23 | 22 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π = β
) β πΈ β
β+) |
24 | | blcntr 23818 |
. . . . . . . . . 10
β’
(((distβ(β^ββ
)) β
(βMetβ(β βm β
)) β§ β
β
(β βm β
) β§ πΈ β β+) β β
β (β
(ballβ(distβ(β^ββ
)))πΈ)) |
25 | 20, 21, 23, 24 | syl3anc 1371 |
. . . . . . . . 9
β’ ((π β§ π = β
) β β
β
(β
(ballβ(distβ(β^ββ
)))πΈ)) |
26 | | elsni 4623 |
. . . . . . . . . . . 12
β’ (π β {β
} β π = β
) |
27 | 13, 26 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π = β
) β π = β
) |
28 | 27 | eqcomd 2737 |
. . . . . . . . . 10
β’ ((π β§ π = β
) β β
= π) |
29 | 28 | oveq1d 7392 |
. . . . . . . . 9
β’ ((π β§ π = β
) β
(β
(ballβ(distβ(β^ββ
)))πΈ) = (π(ballβ(distβ(β^ββ
)))πΈ)) |
30 | 25, 29 | eleqtrd 2834 |
. . . . . . . 8
β’ ((π β§ π = β
) β β
β (π(ballβ(distβ(β^ββ
)))πΈ)) |
31 | 30 | snssd 4789 |
. . . . . . 7
β’ ((π β§ π = β
) β {β
} β (π(ballβ(distβ(β^ββ
)))πΈ)) |
32 | 13, 31 | jca 512 |
. . . . . 6
β’ ((π β§ π = β
) β (π β {β
} β§ {β
} β
(π(ballβ(distβ(β^ββ
)))πΈ))) |
33 | | biidd 261 |
. . . . . . 7
β’ (π = β
β ((π β {β
} β§
{β
} β (π(ballβ(distβ(β^ββ
)))πΈ)) β (π β {β
} β§ {β
} β (π(ballβ(distβ(β^ββ
)))πΈ)))) |
34 | 33 | rspcev 3595 |
. . . . . 6
β’ ((β
β {β
} β§ (π
β {β
} β§ {β
} β (π(ballβ(distβ(β^ββ
)))πΈ))) β βπ β {β
} (π β {β
} β§ {β
} β (π(ballβ(distβ(β^ββ
)))πΈ))) |
35 | 3, 32, 34 | syl2anc 584 |
. . . . 5
β’ ((π β§ π = β
) β βπ β {β
} (π β {β
} β§ {β
} β
(π(ballβ(distβ(β^ββ
)))πΈ))) |
36 | | biidd 261 |
. . . . . 6
β’ (π = β
β (βπ β {β
} (π β {β
} β§
{β
} β (π(ballβ(distβ(β^ββ
)))πΈ)) β βπ β {β
} (π β {β
} β§ {β
} β (π(ballβ(distβ(β^ββ
)))πΈ)))) |
37 | 36 | rspcev 3595 |
. . . . 5
β’ ((β
β {β
} β§ βπ β {β
} (π β {β
} β§ {β
} β
(π(ballβ(distβ(β^ββ
)))πΈ))) β βπ β {β
}βπ β {β
} (π β {β
} β§ {β
} β (π(ballβ(distβ(β^ββ
)))πΈ))) |
38 | 3, 35, 37 | syl2anc 584 |
. . . 4
β’ ((π β§ π = β
) β βπ β {β
}βπ β {β
} (π β {β
} β§ {β
} β
(π(ballβ(distβ(β^ββ
)))πΈ))) |
39 | | oveq2 7385 |
. . . . . . . . . 10
β’ (π = β
β (β
βm π) =
(β βm β
)) |
40 | | qex 12910 |
. . . . . . . . . . . 12
β’ β
β V |
41 | | mapdm0 8802 |
. . . . . . . . . . . 12
β’ (β
β V β (β βm β
) =
{β
}) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . . . . 11
β’ (β
βm β
) = {β
} |
43 | 42 | a1i 11 |
. . . . . . . . . 10
β’ (π = β
β (β
βm β
) = {β
}) |
44 | 39, 43 | eqtr2d 2772 |
. . . . . . . . 9
β’ (π = β
β {β
} =
(β βm π)) |
45 | 44 | eqcomd 2737 |
. . . . . . . 8
β’ (π = β
β (β
βm π) =
{β
}) |
46 | 45 | eleq2d 2818 |
. . . . . . 7
β’ (π = β
β (π β (β
βm π)
β π β
{β
})) |
47 | 45 | eleq2d 2818 |
. . . . . . . . 9
β’ (π = β
β (π β (β
βm π)
β π β
{β
})) |
48 | 47 | anbi1d 630 |
. . . . . . . 8
β’ (π = β
β ((π β (β
βm π) β§
(π β {β
} β§
{β
} β (π(ballβ(distβ(β^ββ
)))πΈ))) β (π β {β
} β§ (π β {β
} β§ {β
} β (π(ballβ(distβ(β^ββ
)))πΈ))))) |
49 | 48 | rexbidv2 3173 |
. . . . . . 7
β’ (π = β
β (βπ β (β
βm π)(π β {β
} β§
{β
} β (π(ballβ(distβ(β^ββ
)))πΈ)) β βπ β {β
} (π β {β
} β§ {β
} β (π(ballβ(distβ(β^ββ
)))πΈ)))) |
50 | 46, 49 | anbi12d 631 |
. . . . . 6
β’ (π = β
β ((π β (β
βm π) β§
βπ β (β
βm π)(π β {β
} β§
{β
} β (π(ballβ(distβ(β^ββ
)))πΈ))) β (π β {β
} β§ βπ β {β
} (π β {β
} β§ {β
} β (π(ballβ(distβ(β^ββ
)))πΈ))))) |
51 | 50 | rexbidv2 3173 |
. . . . 5
β’ (π = β
β (βπ β (β
βm π)βπ β (β βm π)(π β {β
} β§ {β
} β
(π(ballβ(distβ(β^ββ
)))πΈ)) β βπ β {β
}βπ β {β
} (π β {β
} β§ {β
} β (π(ballβ(distβ(β^ββ
)))πΈ)))) |
52 | 51 | adantl 482 |
. . . 4
β’ ((π β§ π = β
) β (βπ β (β
βm π)βπ β (β βm π)(π β {β
} β§ {β
} β
(π(ballβ(distβ(β^ββ
)))πΈ)) β βπ β {β
}βπ β {β
} (π β {β
} β§ {β
} β (π(ballβ(distβ(β^ββ
)))πΈ)))) |
53 | 38, 52 | mpbird 256 |
. . 3
β’ ((π β§ π = β
) β βπ β (β βm π)βπ β (β βm π)(π β {β
} β§ {β
} β
(π(ballβ(distβ(β^ββ
)))πΈ))) |
54 | | ixpeq1 8868 |
. . . . . . . . 9
β’ (π = β
β Xπ β
π ((πβπ)[,)(πβπ)) = Xπ β β
((πβπ)[,)(πβπ))) |
55 | | ixp0x 8886 |
. . . . . . . . . 10
β’ Xπ β
β
((πβπ)[,)(πβπ)) = {β
} |
56 | 55 | a1i 11 |
. . . . . . . . 9
β’ (π = β
β Xπ β
β
((πβπ)[,)(πβπ)) = {β
}) |
57 | 54, 56 | eqtrd 2771 |
. . . . . . . 8
β’ (π = β
β Xπ β
π ((πβπ)[,)(πβπ)) = {β
}) |
58 | 57 | eleq2d 2818 |
. . . . . . 7
β’ (π = β
β (π β Xπ β
π ((πβπ)[,)(πβπ)) β π β {β
})) |
59 | | 2fveq3 6867 |
. . . . . . . . . 10
β’ (π = β
β
(distβ(β^βπ)) =
(distβ(β^ββ
))) |
60 | 59 | fveq2d 6866 |
. . . . . . . . 9
β’ (π = β
β
(ballβ(distβ(β^βπ))) =
(ballβ(distβ(β^ββ
)))) |
61 | 60 | oveqd 7394 |
. . . . . . . 8
β’ (π = β
β (π(ballβ(distβ(β^βπ)))πΈ) = (π(ballβ(distβ(β^ββ
)))πΈ)) |
62 | 57, 61 | sseq12d 3995 |
. . . . . . 7
β’ (π = β
β (Xπ β
π ((πβπ)[,)(πβπ)) β (π(ballβ(distβ(β^βπ)))πΈ) β {β
} β (π(ballβ(distβ(β^ββ
)))πΈ))) |
63 | 58, 62 | anbi12d 631 |
. . . . . 6
β’ (π = β
β ((π β Xπ β
π ((πβπ)[,)(πβπ)) β§ Xπ β π ((πβπ)[,)(πβπ)) β (π(ballβ(distβ(β^βπ)))πΈ)) β (π β {β
} β§ {β
} β
(π(ballβ(distβ(β^ββ
)))πΈ)))) |
64 | 63 | rexbidv 3177 |
. . . . 5
β’ (π = β
β (βπ β (β
βm π)(π β Xπ β
π ((πβπ)[,)(πβπ)) β§ Xπ β π ((πβπ)[,)(πβπ)) β (π(ballβ(distβ(β^βπ)))πΈ)) β βπ β (β βm π)(π β {β
} β§ {β
} β
(π(ballβ(distβ(β^ββ
)))πΈ)))) |
65 | 64 | rexbidv 3177 |
. . . 4
β’ (π = β
β (βπ β (β
βm π)βπ β (β βm π)(π β Xπ β π ((πβπ)[,)(πβπ)) β§ Xπ β π ((πβπ)[,)(πβπ)) β (π(ballβ(distβ(β^βπ)))πΈ)) β βπ β (β βm π)βπ β (β βm π)(π β {β
} β§ {β
} β
(π(ballβ(distβ(β^ββ
)))πΈ)))) |
66 | 65 | adantl 482 |
. . 3
β’ ((π β§ π = β
) β (βπ β (β
βm π)βπ β (β βm π)(π β Xπ β π ((πβπ)[,)(πβπ)) β§ Xπ β π ((πβπ)[,)(πβπ)) β (π(ballβ(distβ(β^βπ)))πΈ)) β βπ β (β βm π)βπ β (β βm π)(π β {β
} β§ {β
} β
(π(ballβ(distβ(β^ββ
)))πΈ)))) |
67 | 53, 66 | mpbird 256 |
. 2
β’ ((π β§ π = β
) β βπ β (β βm π)βπ β (β βm π)(π β Xπ β π ((πβπ)[,)(πβπ)) β§ Xπ β π ((πβπ)[,)(πβπ)) β (π(ballβ(distβ(β^βπ)))πΈ))) |
68 | | hoiqssbl.x |
. . . 4
β’ (π β π β Fin) |
69 | 68 | adantr 481 |
. . 3
β’ ((π β§ Β¬ π = β
) β π β Fin) |
70 | | neqne 2947 |
. . . 4
β’ (Β¬
π = β
β π β β
) |
71 | 70 | adantl 482 |
. . 3
β’ ((π β§ Β¬ π = β
) β π β β
) |
72 | 4 | adantr 481 |
. . 3
β’ ((π β§ Β¬ π = β
) β π β (β βm π)) |
73 | 22 | adantr 481 |
. . 3
β’ ((π β§ Β¬ π = β
) β πΈ β
β+) |
74 | 69, 71, 72, 73 | hoiqssbllem3 45018 |
. 2
β’ ((π β§ Β¬ π = β
) β βπ β (β βm π)βπ β (β βm π)(π β Xπ β π ((πβπ)[,)(πβπ)) β§ Xπ β π ((πβπ)[,)(πβπ)) β (π(ballβ(distβ(β^βπ)))πΈ))) |
75 | 67, 74 | pm2.61dan 811 |
1
β’ (π β βπ β (β βm π)βπ β (β βm π)(π β Xπ β π ((πβπ)[,)(πβπ)) β§ Xπ β π ((πβπ)[,)(πβπ)) β (π(ballβ(distβ(β^βπ)))πΈ))) |