Proof of Theorem cnneiima
| Step | Hyp | Ref
| Expression |
| 1 | | cnneiima.3 |
. . . 4
⊢ (𝜑 → 𝑆 ⊆ (◡𝐹 “ 𝑇)) |
| 2 | | cnneiima.1 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
| 3 | | eqid 2737 |
. . . . . . . 8
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 4 | | eqid 2737 |
. . . . . . . 8
⊢ ∪ 𝐾 =
∪ 𝐾 |
| 5 | 3, 4 | cnf 23254 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
| 6 | 2, 5 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:∪ 𝐽⟶∪ 𝐾) |
| 7 | 6 | ffund 6740 |
. . . . 5
⊢ (𝜑 → Fun 𝐹) |
| 8 | | cnneiima.2 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ((nei‘𝐾)‘𝑇)) |
| 9 | | cntop2 23249 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
| 10 | 2, 9 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Top) |
| 11 | 4 | neiss2 23109 |
. . . . . . . 8
⊢ ((𝐾 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐾)‘𝑇)) → 𝑇 ⊆ ∪ 𝐾) |
| 12 | 10, 8, 11 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ⊆ ∪ 𝐾) |
| 13 | 4 | neii1 23114 |
. . . . . . . 8
⊢ ((𝐾 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐾)‘𝑇)) → 𝑁 ⊆ ∪ 𝐾) |
| 14 | 10, 8, 13 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ⊆ ∪ 𝐾) |
| 15 | 4 | neiint 23112 |
. . . . . . 7
⊢ ((𝐾 ∈ Top ∧ 𝑇 ⊆ ∪ 𝐾
∧ 𝑁 ⊆ ∪ 𝐾)
→ (𝑁 ∈
((nei‘𝐾)‘𝑇) ↔ 𝑇 ⊆ ((int‘𝐾)‘𝑁))) |
| 16 | 10, 12, 14, 15 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (𝑁 ∈ ((nei‘𝐾)‘𝑇) ↔ 𝑇 ⊆ ((int‘𝐾)‘𝑁))) |
| 17 | 8, 16 | mpbid 232 |
. . . . 5
⊢ (𝜑 → 𝑇 ⊆ ((int‘𝐾)‘𝑁)) |
| 18 | | sspreima 7088 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝑇 ⊆ ((int‘𝐾)‘𝑁)) → (◡𝐹 “ 𝑇) ⊆ (◡𝐹 “ ((int‘𝐾)‘𝑁))) |
| 19 | 7, 17, 18 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (◡𝐹 “ 𝑇) ⊆ (◡𝐹 “ ((int‘𝐾)‘𝑁))) |
| 20 | 1, 19 | sstrd 3994 |
. . 3
⊢ (𝜑 → 𝑆 ⊆ (◡𝐹 “ ((int‘𝐾)‘𝑁))) |
| 21 | 4 | cnntri 23279 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑁 ⊆ ∪ 𝐾) → (◡𝐹 “ ((int‘𝐾)‘𝑁)) ⊆ ((int‘𝐽)‘(◡𝐹 “ 𝑁))) |
| 22 | 2, 14, 21 | syl2anc 584 |
. . 3
⊢ (𝜑 → (◡𝐹 “ ((int‘𝐾)‘𝑁)) ⊆ ((int‘𝐽)‘(◡𝐹 “ 𝑁))) |
| 23 | 20, 22 | sstrd 3994 |
. 2
⊢ (𝜑 → 𝑆 ⊆ ((int‘𝐽)‘(◡𝐹 “ 𝑁))) |
| 24 | | cntop1 23248 |
. . . 4
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) |
| 25 | 2, 24 | syl 17 |
. . 3
⊢ (𝜑 → 𝐽 ∈ Top) |
| 26 | | sspreima 7088 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝑇 ⊆ ∪ 𝐾) → (◡𝐹 “ 𝑇) ⊆ (◡𝐹 “ ∪ 𝐾)) |
| 27 | 7, 12, 26 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ 𝑇) ⊆ (◡𝐹 “ ∪ 𝐾)) |
| 28 | | fimacnv 6758 |
. . . . . 6
⊢ (𝐹:∪
𝐽⟶∪ 𝐾
→ (◡𝐹 “ ∪ 𝐾) = ∪
𝐽) |
| 29 | 6, 28 | syl 17 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ ∪ 𝐾) = ∪
𝐽) |
| 30 | 27, 29 | sseqtrd 4020 |
. . . 4
⊢ (𝜑 → (◡𝐹 “ 𝑇) ⊆ ∪ 𝐽) |
| 31 | 1, 30 | sstrd 3994 |
. . 3
⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽) |
| 32 | | sspreima 7088 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝑁 ⊆ ∪ 𝐾) → (◡𝐹 “ 𝑁) ⊆ (◡𝐹 “ ∪ 𝐾)) |
| 33 | 7, 14, 32 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (◡𝐹 “ 𝑁) ⊆ (◡𝐹 “ ∪ 𝐾)) |
| 34 | 33, 29 | sseqtrd 4020 |
. . 3
⊢ (𝜑 → (◡𝐹 “ 𝑁) ⊆ ∪ 𝐽) |
| 35 | 3 | neiint 23112 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽
∧ (◡𝐹 “ 𝑁) ⊆ ∪ 𝐽) → ((◡𝐹 “ 𝑁) ∈ ((nei‘𝐽)‘𝑆) ↔ 𝑆 ⊆ ((int‘𝐽)‘(◡𝐹 “ 𝑁)))) |
| 36 | 25, 31, 34, 35 | syl3anc 1373 |
. 2
⊢ (𝜑 → ((◡𝐹 “ 𝑁) ∈ ((nei‘𝐽)‘𝑆) ↔ 𝑆 ⊆ ((int‘𝐽)‘(◡𝐹 “ 𝑁)))) |
| 37 | 23, 36 | mpbird 257 |
1
⊢ (𝜑 → (◡𝐹 “ 𝑁) ∈ ((nei‘𝐽)‘𝑆)) |