Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . 3
β’
β²π₯(π β§ π΄ < π΅) |
2 | | cncfiooicc.g |
. . 3
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) |
3 | | cncfiooicc.a |
. . . 4
β’ (π β π΄ β β) |
4 | 3 | adantr 482 |
. . 3
β’ ((π β§ π΄ < π΅) β π΄ β β) |
5 | | cncfiooicc.b |
. . . 4
β’ (π β π΅ β β) |
6 | 5 | adantr 482 |
. . 3
β’ ((π β§ π΄ < π΅) β π΅ β β) |
7 | | simpr 486 |
. . 3
β’ ((π β§ π΄ < π΅) β π΄ < π΅) |
8 | | cncfiooicc.f |
. . . 4
β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) |
9 | 8 | adantr 482 |
. . 3
β’ ((π β§ π΄ < π΅) β πΉ β ((π΄(,)π΅)βcnββ)) |
10 | | cncfiooicc.l |
. . . 4
β’ (π β πΏ β (πΉ limβ π΅)) |
11 | 10 | adantr 482 |
. . 3
β’ ((π β§ π΄ < π΅) β πΏ β (πΉ limβ π΅)) |
12 | | cncfiooicc.r |
. . . 4
β’ (π β π
β (πΉ limβ π΄)) |
13 | 12 | adantr 482 |
. . 3
β’ ((π β§ π΄ < π΅) β π
β (πΉ limβ π΄)) |
14 | 1, 2, 4, 6, 7, 9, 11, 13 | cncfiooicclem1 44224 |
. 2
β’ ((π β§ π΄ < π΅) β πΊ β ((π΄[,]π΅)βcnββ)) |
15 | | limccl 25262 |
. . . . . . . . . 10
β’ (πΉ limβ π΄) β
β |
16 | 15, 12 | sselid 3946 |
. . . . . . . . 9
β’ (π β π
β β) |
17 | 16 | snssd 4773 |
. . . . . . . 8
β’ (π β {π
} β β) |
18 | | ssid 3970 |
. . . . . . . . 9
β’ β
β β |
19 | 18 | a1i 11 |
. . . . . . . 8
β’ (π β β β
β) |
20 | | cncfss 24285 |
. . . . . . . 8
β’ (({π
} β β β§ β
β β) β ({π΄}βcnβ{π
}) β ({π΄}βcnββ)) |
21 | 17, 19, 20 | syl2anc 585 |
. . . . . . 7
β’ (π β ({π΄}βcnβ{π
}) β ({π΄}βcnββ)) |
22 | 21 | adantr 482 |
. . . . . 6
β’ ((π β§ π΄ = π΅) β ({π΄}βcnβ{π
}) β ({π΄}βcnββ)) |
23 | 3 | rexrd 11213 |
. . . . . . . . . . . 12
β’ (π β π΄ β
β*) |
24 | | iccid 13318 |
. . . . . . . . . . . 12
β’ (π΄ β β*
β (π΄[,]π΄) = {π΄}) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π΄[,]π΄) = {π΄}) |
26 | | oveq2 7369 |
. . . . . . . . . . 11
β’ (π΄ = π΅ β (π΄[,]π΄) = (π΄[,]π΅)) |
27 | 25, 26 | sylan9req 2794 |
. . . . . . . . . 10
β’ ((π β§ π΄ = π΅) β {π΄} = (π΄[,]π΅)) |
28 | 27 | eqcomd 2739 |
. . . . . . . . 9
β’ ((π β§ π΄ = π΅) β (π΄[,]π΅) = {π΄}) |
29 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ π΄ = π΅) β§ π₯ β (π΄[,]π΅)) β π₯ β (π΄[,]π΅)) |
30 | 28 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π΄ = π΅) β§ π₯ β (π΄[,]π΅)) β (π΄[,]π΅) = {π΄}) |
31 | 29, 30 | eleqtrd 2836 |
. . . . . . . . . . 11
β’ (((π β§ π΄ = π΅) β§ π₯ β (π΄[,]π΅)) β π₯ β {π΄}) |
32 | | elsni 4607 |
. . . . . . . . . . 11
β’ (π₯ β {π΄} β π₯ = π΄) |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π΄ = π΅) β§ π₯ β (π΄[,]π΅)) β π₯ = π΄) |
34 | 33 | iftrued 4498 |
. . . . . . . . 9
β’ (((π β§ π΄ = π΅) β§ π₯ β (π΄[,]π΅)) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = π
) |
35 | 28, 34 | mpteq12dva 5198 |
. . . . . . . 8
β’ ((π β§ π΄ = π΅) β (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) = (π₯ β {π΄} β¦ π
)) |
36 | 2, 35 | eqtrid 2785 |
. . . . . . 7
β’ ((π β§ π΄ = π΅) β πΊ = (π₯ β {π΄} β¦ π
)) |
37 | 3 | recnd 11191 |
. . . . . . . . 9
β’ (π β π΄ β β) |
38 | 37 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π΄ = π΅) β π΄ β β) |
39 | 16 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π΄ = π΅) β π
β β) |
40 | | cncfdmsn 44221 |
. . . . . . . 8
β’ ((π΄ β β β§ π
β β) β (π₯ β {π΄} β¦ π
) β ({π΄}βcnβ{π
})) |
41 | 38, 39, 40 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π΄ = π΅) β (π₯ β {π΄} β¦ π
) β ({π΄}βcnβ{π
})) |
42 | 36, 41 | eqeltrd 2834 |
. . . . . 6
β’ ((π β§ π΄ = π΅) β πΊ β ({π΄}βcnβ{π
})) |
43 | 22, 42 | sseldd 3949 |
. . . . 5
β’ ((π β§ π΄ = π΅) β πΊ β ({π΄}βcnββ)) |
44 | 27 | oveq1d 7376 |
. . . . 5
β’ ((π β§ π΄ = π΅) β ({π΄}βcnββ) = ((π΄[,]π΅)βcnββ)) |
45 | 43, 44 | eleqtrd 2836 |
. . . 4
β’ ((π β§ π΄ = π΅) β πΊ β ((π΄[,]π΅)βcnββ)) |
46 | 45 | adantlr 714 |
. . 3
β’ (((π β§ Β¬ π΄ < π΅) β§ π΄ = π΅) β πΊ β ((π΄[,]π΅)βcnββ)) |
47 | | simpll 766 |
. . . 4
β’ (((π β§ Β¬ π΄ < π΅) β§ Β¬ π΄ = π΅) β π) |
48 | | eqcom 2740 |
. . . . . . . . 9
β’ (π΅ = π΄ β π΄ = π΅) |
49 | 48 | biimpi 215 |
. . . . . . . 8
β’ (π΅ = π΄ β π΄ = π΅) |
50 | 49 | con3i 154 |
. . . . . . 7
β’ (Β¬
π΄ = π΅ β Β¬ π΅ = π΄) |
51 | 50 | adantl 483 |
. . . . . 6
β’ (((π β§ Β¬ π΄ < π΅) β§ Β¬ π΄ = π΅) β Β¬ π΅ = π΄) |
52 | | simplr 768 |
. . . . . 6
β’ (((π β§ Β¬ π΄ < π΅) β§ Β¬ π΄ = π΅) β Β¬ π΄ < π΅) |
53 | | pm4.56 988 |
. . . . . . 7
β’ ((Β¬
π΅ = π΄ β§ Β¬ π΄ < π΅) β Β¬ (π΅ = π΄ β¨ π΄ < π΅)) |
54 | 53 | biimpi 215 |
. . . . . 6
β’ ((Β¬
π΅ = π΄ β§ Β¬ π΄ < π΅) β Β¬ (π΅ = π΄ β¨ π΄ < π΅)) |
55 | 51, 52, 54 | syl2anc 585 |
. . . . 5
β’ (((π β§ Β¬ π΄ < π΅) β§ Β¬ π΄ = π΅) β Β¬ (π΅ = π΄ β¨ π΄ < π΅)) |
56 | 47, 5 | syl 17 |
. . . . . 6
β’ (((π β§ Β¬ π΄ < π΅) β§ Β¬ π΄ = π΅) β π΅ β β) |
57 | 47, 3 | syl 17 |
. . . . . 6
β’ (((π β§ Β¬ π΄ < π΅) β§ Β¬ π΄ = π΅) β π΄ β β) |
58 | 56, 57 | lttrid 11301 |
. . . . 5
β’ (((π β§ Β¬ π΄ < π΅) β§ Β¬ π΄ = π΅) β (π΅ < π΄ β Β¬ (π΅ = π΄ β¨ π΄ < π΅))) |
59 | 55, 58 | mpbird 257 |
. . . 4
β’ (((π β§ Β¬ π΄ < π΅) β§ Β¬ π΄ = π΅) β π΅ < π΄) |
60 | | 0ss 4360 |
. . . . . . . 8
β’ β
β β |
61 | | eqid 2733 |
. . . . . . . . 9
β’
(TopOpenββfld) =
(TopOpenββfld) |
62 | 61 | cnfldtop 24170 |
. . . . . . . . . . 11
β’
(TopOpenββfld) β Top |
63 | | rest0 22543 |
. . . . . . . . . . 11
β’
((TopOpenββfld) β Top β
((TopOpenββfld) βΎt β
) =
{β
}) |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . 10
β’
((TopOpenββfld) βΎt β
) =
{β
} |
65 | 64 | eqcomi 2742 |
. . . . . . . . 9
β’ {β
}
= ((TopOpenββfld) βΎt
β
) |
66 | 61, 65, 65 | cncfcn 24296 |
. . . . . . . 8
β’ ((β
β β β§ β
β β) β (β
βcnββ
) = ({β
} Cn
{β
})) |
67 | 60, 60, 66 | mp2an 691 |
. . . . . . 7
β’
(β
βcnββ
) =
({β
} Cn {β
}) |
68 | | cncfss 24285 |
. . . . . . . 8
β’ ((β
β β β§ β β β) β (β
βcnββ
) β (β
βcnββ)) |
69 | 60, 18, 68 | mp2an 691 |
. . . . . . 7
β’
(β
βcnββ
)
β (β
βcnββ) |
70 | 67, 69 | eqsstrri 3983 |
. . . . . 6
β’
({β
} Cn {β
}) β (β
βcnββ) |
71 | 2 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π΅ < π΄) β πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))))) |
72 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π΅ < π΄) β π΅ < π΄) |
73 | 23 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π΅ < π΄) β π΄ β
β*) |
74 | 5 | rexrd 11213 |
. . . . . . . . . . . 12
β’ (π β π΅ β
β*) |
75 | 74 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π΅ < π΄) β π΅ β
β*) |
76 | | icc0 13321 |
. . . . . . . . . . 11
β’ ((π΄ β β*
β§ π΅ β
β*) β ((π΄[,]π΅) = β
β π΅ < π΄)) |
77 | 73, 75, 76 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π΅ < π΄) β ((π΄[,]π΅) = β
β π΅ < π΄)) |
78 | 72, 77 | mpbird 257 |
. . . . . . . . 9
β’ ((π β§ π΅ < π΄) β (π΄[,]π΅) = β
) |
79 | 78 | mpteq1d 5204 |
. . . . . . . 8
β’ ((π β§ π΅ < π΄) β (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) = (π₯ β β
β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))))) |
80 | | mpt0 6647 |
. . . . . . . . 9
β’ (π₯ β β
β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) = β
|
81 | 80 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π΅ < π΄) β (π₯ β β
β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) = β
) |
82 | 71, 79, 81 | 3eqtrd 2777 |
. . . . . . 7
β’ ((π β§ π΅ < π΄) β πΊ = β
) |
83 | | 0cnf 44208 |
. . . . . . 7
β’ β
β ({β
} Cn {β
}) |
84 | 82, 83 | eqeltrdi 2842 |
. . . . . 6
β’ ((π β§ π΅ < π΄) β πΊ β ({β
} Cn
{β
})) |
85 | 70, 84 | sselid 3946 |
. . . . 5
β’ ((π β§ π΅ < π΄) β πΊ β (β
βcnββ)) |
86 | 78 | eqcomd 2739 |
. . . . . 6
β’ ((π β§ π΅ < π΄) β β
= (π΄[,]π΅)) |
87 | 86 | oveq1d 7376 |
. . . . 5
β’ ((π β§ π΅ < π΄) β (β
βcnββ) = ((π΄[,]π΅)βcnββ)) |
88 | 85, 87 | eleqtrd 2836 |
. . . 4
β’ ((π β§ π΅ < π΄) β πΊ β ((π΄[,]π΅)βcnββ)) |
89 | 47, 59, 88 | syl2anc 585 |
. . 3
β’ (((π β§ Β¬ π΄ < π΅) β§ Β¬ π΄ = π΅) β πΊ β ((π΄[,]π΅)βcnββ)) |
90 | 46, 89 | pm2.61dan 812 |
. 2
β’ ((π β§ Β¬ π΄ < π΅) β πΊ β ((π΄[,]π΅)βcnββ)) |
91 | 14, 90 | pm2.61dan 812 |
1
β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) |