cnpfcf - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cnpfcf		Structured version Visualization version GIF version

Theorem cnpfcf 23984

Description: A function 𝐹 is continuous at point 𝐴 iff 𝐹 respects cluster points there. (Contributed by Jeff Hankins, 14-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)

**Assertion**
Ref	Expression
cnpfcf	⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))))

Distinct variable groups: 𝐴,𝑓 𝑓,𝐹 𝑓,𝐽 𝑓,𝐾 𝑓,𝑋 𝑓,𝑌

Proof of Theorem cnpfcf Dummy variables 𝑔 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnpf2 23193	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋⟶𝑌)
2	1	3expa 1118	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋⟶𝑌)
3	2	3adantl3 1169	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋⟶𝑌)
4		topontop 22856	. . . . . . 7 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
5		cnpfcfi 23983	. . . . . . . . 9 ⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝑓) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))
6	5	3com23 1126	. . . . . . . 8 ⊢ ((𝐾 ∈ Top ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝐴 ∈ (𝐽 fClus 𝑓)) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))
7	6	3expia 1121	. . . . . . 7 ⊢ ((𝐾 ∈ Top ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))
8	4, 7	sylan 580	. . . . . 6 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))
9	8	ralrimivw 3137	. . . . 5 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))
10	9	3ad2antl2 1187	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))
11	3, 10	jca 511	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))))
12	11	ex 412	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))))
13		simplrl 776	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → 𝑔 ∈ (Fil‘𝑋))
14		filfbas 23791	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ (Fil‘𝑋) → 𝑔 ∈ (fBas‘𝑋))
15	13, 14	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → 𝑔 ∈ (fBas‘𝑋))
16		simprl 770	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → ℎ ∈ (Fil‘𝑌))
17		simpllr 775	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → 𝐹:𝑋⟶𝑌)
18		simprr 772	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)
19	15, 16, 17, 18	fmfnfm 23901	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → ∃𝑓 ∈ (Fil‘𝑋)(𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))
20		r19.29 3102	. . . . . . . . . . . . 13 ⊢ ((∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ ∃𝑓 ∈ (Fil‘𝑋)(𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓))) → ∃𝑓 ∈ (Fil‘𝑋)((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓))))
21		flimfcls 23969	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 fLim 𝑓) ⊆ (𝐽 fClus 𝑓)
22		simpll1 1213	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝐽 ∈ (TopOn‘𝑋))
23	22	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐽 ∈ (TopOn‘𝑋))
24		simprl 770	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝑓 ∈ (Fil‘𝑋))
25		simprrl 780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝑔 ⊆ 𝑓)
26		flimss2 23915	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝑔 ⊆ 𝑓) → (𝐽 fLim 𝑔) ⊆ (𝐽 fLim 𝑓))
27	23, 24, 25, 26	syl3anc 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → (𝐽 fLim 𝑔) ⊆ (𝐽 fLim 𝑓))
28		simprr 772	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝐴 ∈ (𝐽 fLim 𝑔))
29	28	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐴 ∈ (𝐽 fLim 𝑔))
30	27, 29	sseldd 3964	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐴 ∈ (𝐽 fLim 𝑓))
31	21, 30	sselid 3961	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐴 ∈ (𝐽 fClus 𝑓))
32		simpll2 1214	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝐾 ∈ (TopOn‘𝑌))
33	32	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐾 ∈ (TopOn‘𝑌))
34		simplr 768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝐹:𝑋⟶𝑌)
35	34	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐹:𝑋⟶𝑌)
36		fcfval 23976	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝐹:𝑋⟶𝑌) → ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ((𝑌 FilMap 𝐹)‘𝑓)))
37	33, 24, 35, 36	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ((𝑌 FilMap 𝐹)‘𝑓)))
38		simprrr 781	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ℎ = ((𝑌 FilMap 𝐹)‘𝑓))
39	38	oveq2d 7426	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → (𝐾 fClus ℎ) = (𝐾 fClus ((𝑌 FilMap 𝐹)‘𝑓)))
40	37, 39	eqtr4d 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ℎ))
41	40	eleq2d 2821	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹) ↔ (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
42	41	biimpd 229	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
43	31, 42	embantd 59	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
44	43	expr 456	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ 𝑓 ∈ (Fil‘𝑋)) → ((𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓)) → ((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
45	44	impcomd 411	. . . . . . . . . . . . . 14 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) ∧ 𝑓 ∈ (Fil‘𝑋)) → (((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓))) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
46	45	rexlimdva 3142	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → (∃𝑓 ∈ (Fil‘𝑋)((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ (𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓))) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
47	20, 46	syl5 34	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → ((∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ ∃𝑓 ∈ (Fil‘𝑋)(𝑔 ⊆ 𝑓 ∧ ℎ = ((𝑌 FilMap 𝐹)‘𝑓))) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
48	19, 47	mpan2d 694	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ (ℎ ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ)) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)))
49	48	expr 456	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ℎ ∈ (Fil‘𝑌)) → (((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
50	49	com23 86	. . . . . . . . 9 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ℎ ∈ (Fil‘𝑌)) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
51	50	ralrimdva 3141	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → ∀ℎ ∈ (Fil‘𝑌)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
52		toponmax 22869	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝐾)
53	32, 52	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝑌 ∈ 𝐾)
54		simprl 770	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝑔 ∈ (Fil‘𝑋))
55	54, 14	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝑔 ∈ (fBas‘𝑋))
56		fmfil 23887	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ 𝐾 ∧ 𝑔 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌) → ((𝑌 FilMap 𝐹)‘𝑔) ∈ (Fil‘𝑌))
57	53, 55, 34, 56	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝑌 FilMap 𝐹)‘𝑔) ∈ (Fil‘𝑌))
58		toponuni 22857	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾)
59	32, 58	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝑌 = ∪ 𝐾)
60	59	fveq2d 6885	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → (Fil‘𝑌) = (Fil‘∪ 𝐾))
61	57, 60	eleqtrd 2837	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝑌 FilMap 𝐹)‘𝑔) ∈ (Fil‘∪ 𝐾))
62		eqid 2736	. . . . . . . . . . 11 ⊢ ∪ 𝐾 = ∪ 𝐾
63	62	flimfnfcls 23971	. . . . . . . . . 10 ⊢ (((𝑌 FilMap 𝐹)‘𝑔) ∈ (Fil‘∪ 𝐾) → ((𝐹‘𝐴) ∈ (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔)) ↔ ∀ℎ ∈ (Fil‘∪ 𝐾)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
64	61, 63	syl 17	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝐹‘𝐴) ∈ (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔)) ↔ ∀ℎ ∈ (Fil‘∪ 𝐾)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
65		flfval 23933	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑔 ∈ (Fil‘𝑋) ∧ 𝐹:𝑋⟶𝑌) → ((𝐾 fLimf 𝑔)‘𝐹) = (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔)))
66	32, 54, 34, 65	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝐾 fLimf 𝑔)‘𝐹) = (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔)))
67	66	eleq2d 2821	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹) ↔ (𝐹‘𝐴) ∈ (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔))))
68	60	raleqdv 3309	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → (∀ℎ ∈ (Fil‘𝑌)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ)) ↔ ∀ℎ ∈ (Fil‘∪ 𝐾)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
69	64, 67, 68	3bitr4d 311	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹) ↔ ∀ℎ ∈ (Fil‘𝑌)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ ℎ → (𝐹‘𝐴) ∈ (𝐾 fClus ℎ))))
70	51, 69	sylibrd 259	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹)))
71	70	expr 456	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝑔) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹))))
72	71	com23 86	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ∈ (Fil‘𝑋)) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐴 ∈ (𝐽 fLim 𝑔) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹))))
73	72	ralrimdva 3141	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → ∀𝑔 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fLim 𝑔) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹))))
74	73	imdistanda 571	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → ((𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑔 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fLim 𝑔) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹)))))
75		cnpflf 23944	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑔 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fLim 𝑔) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹)))))
76	74, 75	sylibrd 259	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → ((𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)))
77	12, 76	impbid 212	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3052 ∃wrex 3061 ⊆ wss 3931 ∪ cuni 4888 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 fBascfbas 21308 Topctop 22836 TopOnctopon 22853 CnP ccnp 23168 Filcfil 23788 FilMap cfm 23876 fLim cflim 23877 fLimf cflf 23878 fClus cfcls 23879 fClusf cfcf 23880

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-iin 4975 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-1st 7993 df-2nd 7994 df-1o 8485 df-2o 8486 df-map 8847 df-en 8965 df-fin 8968 df-fi 9428 df-fbas 21317 df-fg 21318 df-top 22837 df-topon 22854 df-cld 22962 df-ntr 22963 df-cls 22964 df-nei 23041 df-cnp 23171 df-fil 23789 df-fm 23881 df-flim 23882 df-flf 23883 df-fcls 23884 df-fcf 23885

This theorem is referenced by: cnfcf 23985

W3C validator