Proof of Theorem cncfiooicc
Step | Hyp | Ref
| Expression |
1 | | nfv 1920 |
. . 3
⊢
Ⅎ𝑥(𝜑 ∧ 𝐴 < 𝐵) |
2 | | cncfiooicc.g |
. . 3
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) |
3 | | cncfiooicc.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℝ) |
4 | 3 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℝ) |
5 | | cncfiooicc.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) |
6 | 5 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ) |
7 | | simpr 488 |
. . 3
⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝐴 < 𝐵) |
8 | | cncfiooicc.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
9 | 8 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
10 | | cncfiooicc.l |
. . . 4
⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵)) |
11 | 10 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝐿 ∈ (𝐹 limℂ 𝐵)) |
12 | | cncfiooicc.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ (𝐹 limℂ 𝐴)) |
13 | 12 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝑅 ∈ (𝐹 limℂ 𝐴)) |
14 | 1, 2, 4, 6, 7, 9, 11, 13 | cncfiooicclem1 42960 |
. 2
⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
15 | | limccl 24619 |
. . . . . . . . . 10
⊢ (𝐹 limℂ 𝐴) ⊆
ℂ |
16 | 15, 12 | sseldi 3873 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ ℂ) |
17 | 16 | snssd 4694 |
. . . . . . . 8
⊢ (𝜑 → {𝑅} ⊆ ℂ) |
18 | | ssid 3897 |
. . . . . . . . 9
⊢ ℂ
⊆ ℂ |
19 | 18 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℂ ⊆
ℂ) |
20 | | cncfss 23644 |
. . . . . . . 8
⊢ (({𝑅} ⊆ ℂ ∧ ℂ
⊆ ℂ) → ({𝐴}–cn→{𝑅}) ⊆ ({𝐴}–cn→ℂ)) |
21 | 17, 19, 20 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → ({𝐴}–cn→{𝑅}) ⊆ ({𝐴}–cn→ℂ)) |
22 | 21 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → ({𝐴}–cn→{𝑅}) ⊆ ({𝐴}–cn→ℂ)) |
23 | 3 | rexrd 10762 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
24 | | iccid 12859 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ*
→ (𝐴[,]𝐴) = {𝐴}) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴[,]𝐴) = {𝐴}) |
26 | | oveq2 7172 |
. . . . . . . . . . 11
⊢ (𝐴 = 𝐵 → (𝐴[,]𝐴) = (𝐴[,]𝐵)) |
27 | 25, 26 | sylan9req 2794 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → {𝐴} = (𝐴[,]𝐵)) |
28 | 27 | eqcomd 2744 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝐴[,]𝐵) = {𝐴}) |
29 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ (𝐴[,]𝐵)) |
30 | 28 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴[,]𝐵) = {𝐴}) |
31 | 29, 30 | eleqtrd 2835 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ {𝐴}) |
32 | | elsni 4530 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝐴} → 𝑥 = 𝐴) |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 = 𝐴) |
34 | 33 | iftrued 4419 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = 𝑅) |
35 | 28, 34 | mpteq12dva 5111 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) = (𝑥 ∈ {𝐴} ↦ 𝑅)) |
36 | 2, 35 | syl5eq 2785 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐺 = (𝑥 ∈ {𝐴} ↦ 𝑅)) |
37 | 3 | recnd 10740 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) |
38 | 37 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴 ∈ ℂ) |
39 | 16 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝑅 ∈ ℂ) |
40 | | cncfdmsn 42957 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ) → (𝑥 ∈ {𝐴} ↦ 𝑅) ∈ ({𝐴}–cn→{𝑅})) |
41 | 38, 39, 40 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝑥 ∈ {𝐴} ↦ 𝑅) ∈ ({𝐴}–cn→{𝑅})) |
42 | 36, 41 | eqeltrd 2833 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐺 ∈ ({𝐴}–cn→{𝑅})) |
43 | 22, 42 | sseldd 3876 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐺 ∈ ({𝐴}–cn→ℂ)) |
44 | 27 | oveq1d 7179 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → ({𝐴}–cn→ℂ) = ((𝐴[,]𝐵)–cn→ℂ)) |
45 | 43, 44 | eleqtrd 2835 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
46 | 45 | adantlr 715 |
. . 3
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ 𝐴 = 𝐵) → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
47 | | simpll 767 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → 𝜑) |
48 | | eqcom 2745 |
. . . . . . . . 9
⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) |
49 | 48 | biimpi 219 |
. . . . . . . 8
⊢ (𝐵 = 𝐴 → 𝐴 = 𝐵) |
50 | 49 | con3i 157 |
. . . . . . 7
⊢ (¬
𝐴 = 𝐵 → ¬ 𝐵 = 𝐴) |
51 | 50 | adantl 485 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → ¬ 𝐵 = 𝐴) |
52 | | simplr 769 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → ¬ 𝐴 < 𝐵) |
53 | | pm4.56 988 |
. . . . . . 7
⊢ ((¬
𝐵 = 𝐴 ∧ ¬ 𝐴 < 𝐵) ↔ ¬ (𝐵 = 𝐴 ∨ 𝐴 < 𝐵)) |
54 | 53 | biimpi 219 |
. . . . . 6
⊢ ((¬
𝐵 = 𝐴 ∧ ¬ 𝐴 < 𝐵) → ¬ (𝐵 = 𝐴 ∨ 𝐴 < 𝐵)) |
55 | 51, 52, 54 | syl2anc 587 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → ¬ (𝐵 = 𝐴 ∨ 𝐴 < 𝐵)) |
56 | 47, 5 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → 𝐵 ∈ ℝ) |
57 | 47, 3 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → 𝐴 ∈ ℝ) |
58 | 56, 57 | lttrid 10849 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → (𝐵 < 𝐴 ↔ ¬ (𝐵 = 𝐴 ∨ 𝐴 < 𝐵))) |
59 | 55, 58 | mpbird 260 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → 𝐵 < 𝐴) |
60 | | 0ss 4282 |
. . . . . . . 8
⊢ ∅
⊆ ℂ |
61 | | eqid 2738 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
62 | 61 | cnfldtop 23529 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) ∈ Top |
63 | | rest0 21913 |
. . . . . . . . . . 11
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ∅) =
{∅}) |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t ∅) =
{∅} |
65 | 64 | eqcomi 2747 |
. . . . . . . . 9
⊢ {∅}
= ((TopOpen‘ℂfld) ↾t
∅) |
66 | 61, 65, 65 | cncfcn 23655 |
. . . . . . . 8
⊢ ((∅
⊆ ℂ ∧ ∅ ⊆ ℂ) → (∅–cn→∅) = ({∅} Cn
{∅})) |
67 | 60, 60, 66 | mp2an 692 |
. . . . . . 7
⊢
(∅–cn→∅) =
({∅} Cn {∅}) |
68 | | cncfss 23644 |
. . . . . . . 8
⊢ ((∅
⊆ ℂ ∧ ℂ ⊆ ℂ) → (∅–cn→∅) ⊆ (∅–cn→ℂ)) |
69 | 60, 18, 68 | mp2an 692 |
. . . . . . 7
⊢
(∅–cn→∅)
⊆ (∅–cn→ℂ) |
70 | 67, 69 | eqsstrri 3910 |
. . . . . 6
⊢
({∅} Cn {∅}) ⊆ (∅–cn→ℂ) |
71 | 2 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))) |
72 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐵 < 𝐴) |
73 | 23 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐴 ∈
ℝ*) |
74 | 5 | rexrd 10762 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
75 | 74 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐵 ∈
ℝ*) |
76 | | icc0 12862 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴)) |
77 | 73, 75, 76 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴)) |
78 | 72, 77 | mpbird 260 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → (𝐴[,]𝐵) = ∅) |
79 | 78 | mpteq1d 5116 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) = (𝑥 ∈ ∅ ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))) |
80 | | mpt0 6473 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∅ ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) = ∅ |
81 | 80 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → (𝑥 ∈ ∅ ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) = ∅) |
82 | 71, 79, 81 | 3eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐺 = ∅) |
83 | | 0cnf 42944 |
. . . . . . 7
⊢ ∅
∈ ({∅} Cn {∅}) |
84 | 82, 83 | eqeltrdi 2841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐺 ∈ ({∅} Cn
{∅})) |
85 | 70, 84 | sseldi 3873 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐺 ∈ (∅–cn→ℂ)) |
86 | 78 | eqcomd 2744 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → ∅ = (𝐴[,]𝐵)) |
87 | 86 | oveq1d 7179 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → (∅–cn→ℂ) = ((𝐴[,]𝐵)–cn→ℂ)) |
88 | 85, 87 | eleqtrd 2835 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
89 | 47, 59, 88 | syl2anc 587 |
. . 3
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
90 | 46, 89 | pm2.61dan 813 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐴 < 𝐵) → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
91 | 14, 90 | pm2.61dan 813 |
1
⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |