Proof of Theorem cnfcf
Step | Hyp | Ref
| Expression |
1 | | cncnp 21084 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥)))) |
2 | | cnpfcf 21845 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑥 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝑥 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹))))) |
3 | 2 | 3expa 1265 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑥 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝑥 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹))))) |
4 | 3 | adantlr 751 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑥 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝑥 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹))))) |
5 | | simplr 792 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑥 ∈ 𝑋) → 𝐹:𝑋⟶𝑌) |
6 | 5 | biantrurd 529 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑥 ∈ 𝑋) → (∀𝑓 ∈ (Fil‘𝑋)(𝑥 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝑥 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹))))) |
7 | 4, 6 | bitr4d 271 |
. . . . 5
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑥 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ ∀𝑓 ∈ (Fil‘𝑋)(𝑥 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))) |
8 | 7 | ralbidva 2985 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) → (∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ ∀𝑥 ∈ 𝑋 ∀𝑓 ∈ (Fil‘𝑋)(𝑥 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))) |
9 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ ∪ 𝐽 =
∪ 𝐽 |
10 | 9 | fclselbas 21820 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐽 fClus 𝑓) → 𝑥 ∈ ∪ 𝐽) |
11 | | toponuni 20719 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
12 | 11 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) → 𝑋 = ∪ 𝐽) |
13 | 12 | eleq2d 2687 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝐽)) |
14 | 10, 13 | syl5ibr 236 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) → (𝑥 ∈ (𝐽 fClus 𝑓) → 𝑥 ∈ 𝑋)) |
15 | 14 | pm4.71rd 667 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) → (𝑥 ∈ (𝐽 fClus 𝑓) ↔ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ (𝐽 fClus 𝑓)))) |
16 | 15 | imbi1d 331 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) → ((𝑥 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ (𝐽 fClus 𝑓)) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))) |
17 | | impexp 462 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ (𝐽 fClus 𝑓)) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ↔ (𝑥 ∈ 𝑋 → (𝑥 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))) |
18 | 16, 17 | syl6bb 276 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) → ((𝑥 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ↔ (𝑥 ∈ 𝑋 → (𝑥 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹))))) |
19 | 18 | ralbidv2 2984 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) → (∀𝑥 ∈ (𝐽 fClus 𝑓)(𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹) ↔ ∀𝑥 ∈ 𝑋 (𝑥 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))) |
20 | 19 | ralbidv 2986 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) → (∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ (𝐽 fClus 𝑓)(𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹) ↔ ∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ 𝑋 (𝑥 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))) |
21 | | ralcom 3098 |
. . . . 5
⊢
(∀𝑥 ∈
𝑋 ∀𝑓 ∈ (Fil‘𝑋)(𝑥 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ↔ ∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ 𝑋 (𝑥 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹))) |
22 | 20, 21 | syl6rbbr 279 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) → (∀𝑥 ∈ 𝑋 ∀𝑓 ∈ (Fil‘𝑋)(𝑥 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ↔ ∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ (𝐽 fClus 𝑓)(𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹))) |
23 | 8, 22 | bitrd 268 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋⟶𝑌) → (∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ ∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ (𝐽 fClus 𝑓)(𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹))) |
24 | 23 | pm5.32da 673 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → ((𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥)) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ (𝐽 fClus 𝑓)(𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))) |
25 | 1, 24 | bitrd 268 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ (𝐽 fClus 𝑓)(𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))) |