Step | Hyp | Ref
| Expression |
1 | | iftrue 4496 |
. . . . . . 7
β’ (π₯ = π΄ β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = π
) |
2 | 1 | adantl 483 |
. . . . . 6
β’ ((π β§ π₯ = π΄) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = π
) |
3 | | cncfiooiccre.f |
. . . . . . . . 9
β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) |
4 | | cncff 24279 |
. . . . . . . . 9
β’ (πΉ β ((π΄(,)π΅)βcnββ) β πΉ:(π΄(,)π΅)βΆβ) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
β’ (π β πΉ:(π΄(,)π΅)βΆβ) |
6 | | ioosscn 13335 |
. . . . . . . . 9
β’ (π΄(,)π΅) β β |
7 | 6 | a1i 11 |
. . . . . . . 8
β’ (π β (π΄(,)π΅) β β) |
8 | | eqid 2733 |
. . . . . . . . 9
β’
(TopOpenββfld) =
(TopOpenββfld) |
9 | | cncfiooiccre.b |
. . . . . . . . . 10
β’ (π β π΅ β β) |
10 | 9 | rexrd 11213 |
. . . . . . . . 9
β’ (π β π΅ β
β*) |
11 | | cncfiooiccre.a |
. . . . . . . . 9
β’ (π β π΄ β β) |
12 | | cncfiooiccre.altb |
. . . . . . . . 9
β’ (π β π΄ < π΅) |
13 | 8, 10, 11, 12 | lptioo1cn 43977 |
. . . . . . . 8
β’ (π β π΄ β
((limPtβ(TopOpenββfld))β(π΄(,)π΅))) |
14 | | cncfiooiccre.r |
. . . . . . . 8
β’ (π β π
β (πΉ limβ π΄)) |
15 | 5, 7, 13, 14 | limcrecl 43960 |
. . . . . . 7
β’ (π β π
β β) |
16 | 15 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ = π΄) β π
β β) |
17 | 2, 16 | eqeltrd 2834 |
. . . . 5
β’ ((π β§ π₯ = π΄) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
18 | 17 | adantlr 714 |
. . . 4
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ π₯ = π΄) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
19 | | iffalse 4499 |
. . . . . . . . 9
β’ (Β¬
π₯ = π΄ β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = if(π₯ = π΅, πΏ, (πΉβπ₯))) |
20 | | iftrue 4496 |
. . . . . . . . 9
β’ (π₯ = π΅ β if(π₯ = π΅, πΏ, (πΉβπ₯)) = πΏ) |
21 | 19, 20 | sylan9eq 2793 |
. . . . . . . 8
β’ ((Β¬
π₯ = π΄ β§ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = πΏ) |
22 | 21 | adantll 713 |
. . . . . . 7
β’ (((π β§ Β¬ π₯ = π΄) β§ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = πΏ) |
23 | 11 | rexrd 11213 |
. . . . . . . . . 10
β’ (π β π΄ β
β*) |
24 | 8, 23, 9, 12 | lptioo2cn 43976 |
. . . . . . . . 9
β’ (π β π΅ β
((limPtβ(TopOpenββfld))β(π΄(,)π΅))) |
25 | | cncfiooiccre.l |
. . . . . . . . 9
β’ (π β πΏ β (πΉ limβ π΅)) |
26 | 5, 7, 24, 25 | limcrecl 43960 |
. . . . . . . 8
β’ (π β πΏ β β) |
27 | 26 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ Β¬ π₯ = π΄) β§ π₯ = π΅) β πΏ β β) |
28 | 22, 27 | eqeltrd 2834 |
. . . . . 6
β’ (((π β§ Β¬ π₯ = π΄) β§ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
29 | 28 | adantllr 718 |
. . . . 5
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
30 | | iffalse 4499 |
. . . . . . . 8
β’ (Β¬
π₯ = π΅ β if(π₯ = π΅, πΏ, (πΉβπ₯)) = (πΉβπ₯)) |
31 | 19, 30 | sylan9eq 2793 |
. . . . . . 7
β’ ((Β¬
π₯ = π΄ β§ Β¬ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = (πΉβπ₯)) |
32 | 31 | adantll 713 |
. . . . . 6
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) = (πΉβπ₯)) |
33 | 5 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β πΉ:(π΄(,)π΅)βΆβ) |
34 | 23 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π΄ β
β*) |
35 | 10 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π΅ β
β*) |
36 | 11 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΄ β β) |
37 | 9 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄[,]π΅)) β π΅ β β) |
38 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β (π΄[,]π΅)) |
39 | | eliccre 43833 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΅ β β β§ π₯ β (π΄[,]π΅)) β π₯ β β) |
40 | 36, 37, 38, 39 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β β) |
41 | 40 | ad2antrr 725 |
. . . . . . . 8
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π₯ β β) |
42 | 11 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π΄ β β) |
43 | 40 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π₯ β β) |
44 | 23 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π΄ β
β*) |
45 | 10 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π΅ β
β*) |
46 | 38 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π₯ β (π΄[,]π΅)) |
47 | | iccgelb 13329 |
. . . . . . . . . . 11
β’ ((π΄ β β*
β§ π΅ β
β* β§ π₯
β (π΄[,]π΅)) β π΄ β€ π₯) |
48 | 44, 45, 46, 47 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π΄ β€ π₯) |
49 | | neqne 2948 |
. . . . . . . . . . 11
β’ (Β¬
π₯ = π΄ β π₯ β π΄) |
50 | 49 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π₯ β π΄) |
51 | 42, 43, 48, 50 | leneltd 11317 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β π΄ < π₯) |
52 | 51 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π΄ < π₯) |
53 | 40 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΅) β π₯ β β) |
54 | 9 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΅) β π΅ β β) |
55 | 23 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΅) β π΄ β
β*) |
56 | 10 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΅) β π΅ β
β*) |
57 | 38 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΅) β π₯ β (π΄[,]π΅)) |
58 | | iccleub 13328 |
. . . . . . . . . . 11
β’ ((π΄ β β*
β§ π΅ β
β* β§ π₯
β (π΄[,]π΅)) β π₯ β€ π΅) |
59 | 55, 56, 57, 58 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΅) β π₯ β€ π΅) |
60 | | neqne 2948 |
. . . . . . . . . . . 12
β’ (Β¬
π₯ = π΅ β π₯ β π΅) |
61 | 60 | necomd 2996 |
. . . . . . . . . . 11
β’ (Β¬
π₯ = π΅ β π΅ β π₯) |
62 | 61 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΅) β π΅ β π₯) |
63 | 53, 54, 59, 62 | leneltd 11317 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΅) β π₯ < π΅) |
64 | 63 | adantlr 714 |
. . . . . . . 8
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π₯ < π΅) |
65 | 34, 35, 41, 52, 64 | eliood 43826 |
. . . . . . 7
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β π₯ β (π΄(,)π΅)) |
66 | 33, 65 | ffvelcdmd 7040 |
. . . . . 6
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β (πΉβπ₯) β β) |
67 | 32, 66 | eqeltrd 2834 |
. . . . 5
β’ ((((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β§ Β¬ π₯ = π΅) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
68 | 29, 67 | pm2.61dan 812 |
. . . 4
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ Β¬ π₯ = π΄) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
69 | 18, 68 | pm2.61dan 812 |
. . 3
β’ ((π β§ π₯ β (π΄[,]π΅)) β if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯))) β β) |
70 | | cncfiooiccre.g |
. . 3
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π
, if(π₯ = π΅, πΏ, (πΉβπ₯)))) |
71 | 69, 70 | fmptd 7066 |
. 2
β’ (π β πΊ:(π΄[,]π΅)βΆβ) |
72 | | ax-resscn 11116 |
. . 3
β’ β
β β |
73 | | cncfiooiccre.x |
. . . 4
β’
β²π₯π |
74 | | ssid 3970 |
. . . . . 6
β’ β
β β |
75 | | cncfss 24285 |
. . . . . 6
β’ ((β
β β β§ β β β) β ((π΄(,)π΅)βcnββ) β ((π΄(,)π΅)βcnββ)) |
76 | 72, 74, 75 | mp2an 691 |
. . . . 5
β’ ((π΄(,)π΅)βcnββ) β ((π΄(,)π΅)βcnββ) |
77 | 76, 3 | sselid 3946 |
. . . 4
β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) |
78 | 73, 70, 11, 9, 77, 25, 14 | cncfiooicc 44225 |
. . 3
β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) |
79 | | cncfcdm 24284 |
. . 3
β’ ((β
β β β§ πΊ
β ((π΄[,]π΅)βcnββ)) β (πΊ β ((π΄[,]π΅)βcnββ) β πΊ:(π΄[,]π΅)βΆβ)) |
80 | 72, 78, 79 | sylancr 588 |
. 2
β’ (π β (πΊ β ((π΄[,]π΅)βcnββ) β πΊ:(π΄[,]π΅)βΆβ)) |
81 | 71, 80 | mpbird 257 |
1
β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) |