Proof of Theorem cncfiooicc
| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. . 3
⊢
Ⅎ𝑥(𝜑 ∧ 𝐴 < 𝐵) |
| 2 | | cncfiooicc.g |
. . 3
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) |
| 3 | | cncfiooicc.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 4 | 3 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℝ) |
| 5 | | cncfiooicc.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 6 | 5 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ) |
| 7 | | simpr 484 |
. . 3
⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝐴 < 𝐵) |
| 8 | | cncfiooicc.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 9 | 8 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 10 | | cncfiooicc.l |
. . . 4
⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵)) |
| 11 | 10 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝐿 ∈ (𝐹 limℂ 𝐵)) |
| 12 | | cncfiooicc.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ (𝐹 limℂ 𝐴)) |
| 13 | 12 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝑅 ∈ (𝐹 limℂ 𝐴)) |
| 14 | 1, 2, 4, 6, 7, 9, 11, 13 | cncfiooicclem1 45908 |
. 2
⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 15 | | limccl 25910 |
. . . . . . . . . 10
⊢ (𝐹 limℂ 𝐴) ⊆
ℂ |
| 16 | 15, 12 | sselid 3981 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ ℂ) |
| 17 | 16 | snssd 4809 |
. . . . . . . 8
⊢ (𝜑 → {𝑅} ⊆ ℂ) |
| 18 | | ssid 4006 |
. . . . . . . . 9
⊢ ℂ
⊆ ℂ |
| 19 | 18 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℂ ⊆
ℂ) |
| 20 | | cncfss 24925 |
. . . . . . . 8
⊢ (({𝑅} ⊆ ℂ ∧ ℂ
⊆ ℂ) → ({𝐴}–cn→{𝑅}) ⊆ ({𝐴}–cn→ℂ)) |
| 21 | 17, 19, 20 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ({𝐴}–cn→{𝑅}) ⊆ ({𝐴}–cn→ℂ)) |
| 22 | 21 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → ({𝐴}–cn→{𝑅}) ⊆ ({𝐴}–cn→ℂ)) |
| 23 | 3 | rexrd 11311 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 24 | | iccid 13432 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ*
→ (𝐴[,]𝐴) = {𝐴}) |
| 25 | 23, 24 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴[,]𝐴) = {𝐴}) |
| 26 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝐴 = 𝐵 → (𝐴[,]𝐴) = (𝐴[,]𝐵)) |
| 27 | 25, 26 | sylan9req 2798 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → {𝐴} = (𝐴[,]𝐵)) |
| 28 | 27 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝐴[,]𝐵) = {𝐴}) |
| 29 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ (𝐴[,]𝐵)) |
| 30 | 28 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴[,]𝐵) = {𝐴}) |
| 31 | 29, 30 | eleqtrd 2843 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ {𝐴}) |
| 32 | | elsni 4643 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝐴} → 𝑥 = 𝐴) |
| 33 | 31, 32 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 = 𝐴) |
| 34 | 33 | iftrued 4533 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 = 𝐵) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = 𝑅) |
| 35 | 28, 34 | mpteq12dva 5231 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) = (𝑥 ∈ {𝐴} ↦ 𝑅)) |
| 36 | 2, 35 | eqtrid 2789 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐺 = (𝑥 ∈ {𝐴} ↦ 𝑅)) |
| 37 | 3 | recnd 11289 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 38 | 37 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴 ∈ ℂ) |
| 39 | 16 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝑅 ∈ ℂ) |
| 40 | | cncfdmsn 45905 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ) → (𝑥 ∈ {𝐴} ↦ 𝑅) ∈ ({𝐴}–cn→{𝑅})) |
| 41 | 38, 39, 40 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝑥 ∈ {𝐴} ↦ 𝑅) ∈ ({𝐴}–cn→{𝑅})) |
| 42 | 36, 41 | eqeltrd 2841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐺 ∈ ({𝐴}–cn→{𝑅})) |
| 43 | 22, 42 | sseldd 3984 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐺 ∈ ({𝐴}–cn→ℂ)) |
| 44 | 27 | oveq1d 7446 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → ({𝐴}–cn→ℂ) = ((𝐴[,]𝐵)–cn→ℂ)) |
| 45 | 43, 44 | eleqtrd 2843 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 46 | 45 | adantlr 715 |
. . 3
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ 𝐴 = 𝐵) → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 47 | | simpll 767 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → 𝜑) |
| 48 | | eqcom 2744 |
. . . . . . . . 9
⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) |
| 49 | 48 | biimpi 216 |
. . . . . . . 8
⊢ (𝐵 = 𝐴 → 𝐴 = 𝐵) |
| 50 | 49 | con3i 154 |
. . . . . . 7
⊢ (¬
𝐴 = 𝐵 → ¬ 𝐵 = 𝐴) |
| 51 | 50 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → ¬ 𝐵 = 𝐴) |
| 52 | | simplr 769 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → ¬ 𝐴 < 𝐵) |
| 53 | | pm4.56 991 |
. . . . . . 7
⊢ ((¬
𝐵 = 𝐴 ∧ ¬ 𝐴 < 𝐵) ↔ ¬ (𝐵 = 𝐴 ∨ 𝐴 < 𝐵)) |
| 54 | 53 | biimpi 216 |
. . . . . 6
⊢ ((¬
𝐵 = 𝐴 ∧ ¬ 𝐴 < 𝐵) → ¬ (𝐵 = 𝐴 ∨ 𝐴 < 𝐵)) |
| 55 | 51, 52, 54 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → ¬ (𝐵 = 𝐴 ∨ 𝐴 < 𝐵)) |
| 56 | 47, 5 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → 𝐵 ∈ ℝ) |
| 57 | 47, 3 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → 𝐴 ∈ ℝ) |
| 58 | 56, 57 | lttrid 11399 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → (𝐵 < 𝐴 ↔ ¬ (𝐵 = 𝐴 ∨ 𝐴 < 𝐵))) |
| 59 | 55, 58 | mpbird 257 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → 𝐵 < 𝐴) |
| 60 | | 0ss 4400 |
. . . . . . . 8
⊢ ∅
⊆ ℂ |
| 61 | | eqid 2737 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 62 | 61 | cnfldtop 24804 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) ∈ Top |
| 63 | | rest0 23177 |
. . . . . . . . . . 11
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ∅) =
{∅}) |
| 64 | 62, 63 | ax-mp 5 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t ∅) =
{∅} |
| 65 | 64 | eqcomi 2746 |
. . . . . . . . 9
⊢ {∅}
= ((TopOpen‘ℂfld) ↾t
∅) |
| 66 | 61, 65, 65 | cncfcn 24936 |
. . . . . . . 8
⊢ ((∅
⊆ ℂ ∧ ∅ ⊆ ℂ) → (∅–cn→∅) = ({∅} Cn
{∅})) |
| 67 | 60, 60, 66 | mp2an 692 |
. . . . . . 7
⊢
(∅–cn→∅) =
({∅} Cn {∅}) |
| 68 | | cncfss 24925 |
. . . . . . . 8
⊢ ((∅
⊆ ℂ ∧ ℂ ⊆ ℂ) → (∅–cn→∅) ⊆ (∅–cn→ℂ)) |
| 69 | 60, 18, 68 | mp2an 692 |
. . . . . . 7
⊢
(∅–cn→∅)
⊆ (∅–cn→ℂ) |
| 70 | 67, 69 | eqsstrri 4031 |
. . . . . 6
⊢
({∅} Cn {∅}) ⊆ (∅–cn→ℂ) |
| 71 | 2 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))) |
| 72 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐵 < 𝐴) |
| 73 | 23 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐴 ∈
ℝ*) |
| 74 | 5 | rexrd 11311 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 75 | 74 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐵 ∈
ℝ*) |
| 76 | | icc0 13435 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴)) |
| 77 | 73, 75, 76 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴)) |
| 78 | 72, 77 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → (𝐴[,]𝐵) = ∅) |
| 79 | 78 | mpteq1d 5237 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) = (𝑥 ∈ ∅ ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))) |
| 80 | | mpt0 6710 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∅ ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) = ∅ |
| 81 | 80 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → (𝑥 ∈ ∅ ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) = ∅) |
| 82 | 71, 79, 81 | 3eqtrd 2781 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐺 = ∅) |
| 83 | | 0cnf 45892 |
. . . . . . 7
⊢ ∅
∈ ({∅} Cn {∅}) |
| 84 | 82, 83 | eqeltrdi 2849 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐺 ∈ ({∅} Cn
{∅})) |
| 85 | 70, 84 | sselid 3981 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐺 ∈ (∅–cn→ℂ)) |
| 86 | 78 | eqcomd 2743 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → ∅ = (𝐴[,]𝐵)) |
| 87 | 86 | oveq1d 7446 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → (∅–cn→ℂ) = ((𝐴[,]𝐵)–cn→ℂ)) |
| 88 | 85, 87 | eleqtrd 2843 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 < 𝐴) → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 89 | 47, 59, 88 | syl2anc 584 |
. . 3
⊢ (((𝜑 ∧ ¬ 𝐴 < 𝐵) ∧ ¬ 𝐴 = 𝐵) → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 90 | 46, 89 | pm2.61dan 813 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐴 < 𝐵) → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 91 | 14, 90 | pm2.61dan 813 |
1
⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |