cnpnei - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > cnpnei		GIF version

Theorem cnpnei 12169

Description: A condition for continuity at a point in terms of neighborhoods. (Contributed by Jeff Hankins, 7-Sep-2009.)

**Hypotheses**
Ref	Expression
cnpnei.1	⊢ 𝑋 = ∪ 𝐽
cnpnei.2	⊢ 𝑌 = ∪ 𝐾

**Assertion**
Ref	Expression
cnpnei	⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})))

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

Proof of Theorem cnpnei Dummy variables 𝑔 𝑜 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnvimass 4838	. . . . . . . 8 ⊢ (^◡𝐹 “ 𝑦) ⊆ dom 𝐹
2		fdm 5214	. . . . . . . 8 ⊢ (𝐹:𝑋⟶𝑌 → dom 𝐹 = 𝑋)
3	1, 2	syl5sseq 3097	. . . . . . 7 ⊢ (𝐹:𝑋⟶𝑌 → (^◡𝐹 “ 𝑦) ⊆ 𝑋)
4	3	3ad2ant3 972	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → (^◡𝐹 “ 𝑦) ⊆ 𝑋)
5	4	ad2antrr 475	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → (^◡𝐹 “ 𝑦) ⊆ 𝑋)
6		neii2 12100	. . . . . . . 8 ⊢ ((𝐾 ∈ Top ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) → ∃𝑔 ∈ 𝐾 ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))
7	6	3ad2antl2 1112	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) → ∃𝑔 ∈ 𝐾 ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))
8	7	ad2ant2rl 498	. . . . . 6 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → ∃𝑔 ∈ 𝐾 ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))
9		cnpnei.1	. . . . . . . . . . . 12 ⊢ 𝑋 = ∪ 𝐽
10	9	toptopon 11967	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
11	10	biimpi 119	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → 𝐽 ∈ (TopOn‘𝑋))
12	11	3ad2ant1 970	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → 𝐽 ∈ (TopOn‘𝑋))
13	12	ad3antrrr 479	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → 𝐽 ∈ (TopOn‘𝑋))
14		cnpnei.2	. . . . . . . . . . . 12 ⊢ 𝑌 = ∪ 𝐾
15	14	toptopon 11967	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌))
16	15	biimpi 119	. . . . . . . . . 10 ⊢ (𝐾 ∈ Top → 𝐾 ∈ (TopOn‘𝑌))
17	16	3ad2ant2 971	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → 𝐾 ∈ (TopOn‘𝑌))
18	17	ad3antrrr 479	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → 𝐾 ∈ (TopOn‘𝑌))
19		simpllr 504	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → 𝐴 ∈ 𝑋)
20		simplrl 505	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
21		simprl 501	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → 𝑔 ∈ 𝐾)
22		simprrl 509	. . . . . . . . 9 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → {(𝐹‘𝐴)} ⊆ 𝑔)
23		fvexg 5372	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ∈ V)
24	20, 19, 23	syl2anc 406	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (𝐹‘𝐴) ∈ V)
25		snssg 3603	. . . . . . . . . 10 ⊢ ((𝐹‘𝐴) ∈ V → ((𝐹‘𝐴) ∈ 𝑔 ↔ {(𝐹‘𝐴)} ⊆ 𝑔))
26	24, 25	syl 14	. . . . . . . . 9 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → ((𝐹‘𝐴) ∈ 𝑔 ↔ {(𝐹‘𝐴)} ⊆ 𝑔))
27	22, 26	mpbird 166	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (𝐹‘𝐴) ∈ 𝑔)
28		icnpimaex 12161	. . . . . . . 8 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑔)) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔))
29	13, 18, 19, 20, 21, 27, 28	syl33anc 1199	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔))
30		sstr2 3054	. . . . . . . . . . . . 13 ⊢ ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝑔 ⊆ 𝑦 → (𝐹 “ 𝑜) ⊆ 𝑦))
31	30	com12 30	. . . . . . . . . . . 12 ⊢ (𝑔 ⊆ 𝑦 → ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝐹 “ 𝑜) ⊆ 𝑦))
32	31	ad2antll 478	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)) → ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝐹 “ 𝑜) ⊆ 𝑦))
33	32	ad2antlr 476	. . . . . . . . . 10 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝐹 “ 𝑜) ⊆ 𝑦))
34		ffun 5211	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝑋⟶𝑌 → Fun 𝐹)
35	34	3ad2ant3 972	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → Fun 𝐹)
36	35	ad2antrr 475	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → Fun 𝐹)
37	36	ad2antrr 475	. . . . . . . . . . 11 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → Fun 𝐹)
38	9	eltopss 11958	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ 𝑋)
39	38	adantlr 464	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ 𝑋)
40	2	sseq2d 3077	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋⟶𝑌 → (𝑜 ⊆ dom 𝐹 ↔ 𝑜 ⊆ 𝑋))
41	40	ad2antlr 476	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → (𝑜 ⊆ dom 𝐹 ↔ 𝑜 ⊆ 𝑋))
42	39, 41	mpbird 166	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
43	42	3adantl2 1106	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
44	43	adantlr 464	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
45	44	adantlr 464	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
46	45	adantlr 464	. . . . . . . . . . 11 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
47		funimass3 5468	. . . . . . . . . . 11 ⊢ ((Fun 𝐹 ∧ 𝑜 ⊆ dom 𝐹) → ((𝐹 “ 𝑜) ⊆ 𝑦 ↔ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
48	37, 46, 47	syl2anc 406	. . . . . . . . . 10 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐹 “ 𝑜) ⊆ 𝑦 ↔ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
49	33, 48	sylibd 148	. . . . . . . . 9 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐹 “ 𝑜) ⊆ 𝑔 → 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
50	49	anim2d 333	. . . . . . . 8 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔) → (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦))))
51	50	reximdva 2493	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦))))
52	29, 51	mpd 13	. . . . . 6 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
53	8, 52	rexlimddv 2513	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
54	9	isneip 12097	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋) → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((^◡𝐹 “ 𝑦) ⊆ 𝑋 ∧ ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))))
55	54	3ad2antl1 1111	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((^◡𝐹 “ 𝑦) ⊆ 𝑋 ∧ ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))))
56	55	adantr 272	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((^◡𝐹 “ 𝑦) ⊆ 𝑋 ∧ ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))))
57	5, 53, 56	mpbir2and 896	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → (^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}))
58	57	exp32 360	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → (𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}) → (^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}))))
59	58	ralrimdv 2470	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})))
60		simpll3 990	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → 𝐹:𝑋⟶𝑌)
61		opnneip 12110	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Top ∧ 𝑜 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑜) → 𝑜 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))
62		imaeq2 4813	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑜 → (^◡𝐹 “ 𝑦) = (^◡𝐹 “ 𝑜))
63	62	eleq1d 2168	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑜 → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
64	63	rspcv 2740	. . . . . . . . . . . . . 14 ⊢ (𝑜 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
65	61, 64	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑜 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑜) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
66	65	3com23 1155	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Top ∧ (𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
67	66	3expb 1150	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Top ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
68	67	3ad2antl2 1112	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
69	68	adantlr 464	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
70		neii2 12100	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜)))
71	70	ex 114	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → ((^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
72	71	3ad2ant1 970	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → ((^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
73	72	ad2antrr 475	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → ((^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
74		snssg 3603	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ 𝑔 ↔ {𝐴} ⊆ 𝑔))
75	74	ad3antlr 480	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → (𝐴 ∈ 𝑔 ↔ {𝐴} ⊆ 𝑔))
76	35	ad3antrrr 479	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → Fun 𝐹)
77	9	eltopss 11958	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ 𝑋)
78	77	3ad2antl1 1111	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ 𝑋)
79	2	sseq2d 3077	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:𝑋⟶𝑌 → (𝑔 ⊆ dom 𝐹 ↔ 𝑔 ⊆ 𝑋))
80	79	3ad2ant3 972	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → (𝑔 ⊆ dom 𝐹 ↔ 𝑔 ⊆ 𝑋))
81	80	biimpar 293	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ⊆ 𝑋) → 𝑔 ⊆ dom 𝐹)
82	78, 81	syldan 278	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ dom 𝐹)
83	82	adantlr 464	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ dom 𝐹)
84	83	adantlr 464	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ dom 𝐹)
85		funimass3 5468	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐹 ∧ 𝑔 ⊆ dom 𝐹) → ((𝐹 “ 𝑔) ⊆ 𝑜 ↔ 𝑔 ⊆ (^◡𝐹 “ 𝑜)))
86	76, 84, 85	syl2anc 406	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → ((𝐹 “ 𝑔) ⊆ 𝑜 ↔ 𝑔 ⊆ (^◡𝐹 “ 𝑜)))
87	75, 86	anbi12d 460	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → ((𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜) ↔ ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
88	87	biimprd 157	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → (({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜)) → (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
89	88	reximdva 2493	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜)) → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
90	69, 73, 89	3syld 57	. . . . . . . 8 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
91	90	exp32 360	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝐴) ∈ 𝑜 → (𝑜 ∈ 𝐾 → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
92	91	com24 87	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝑜 ∈ 𝐾 → ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
93	92	imp 123	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → (𝑜 ∈ 𝐾 → ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜))))
94	93	ralrimiv 2463	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
95	11	3ad2ant1 970	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑋))
96	16	3ad2ant2 971	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋) → 𝐾 ∈ (TopOn‘𝑌))
97		simp3 951	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑋)
98		iscnp 12149	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
99	95, 96, 97, 98	syl3anc 1184	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
100	99	3expa 1149	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
101	100	3adantl3 1107	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
102	101	adantr 272	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
103	60, 94, 102	mpbir2and 896	. . 3 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
104	103	ex 114	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)))
105	59, 104	impbid 128	1 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∧ w3a 930 = wceq 1299 ∈ wcel 1448 ∀wral 2375 ∃wrex 2376 Vcvv 2641 ⊆ wss 3021 {csn 3474 ∪ cuni 3683 ^◡ccnv 4476 dom cdm 4477 “ cima 4480 Fun wfun 5053 ⟶wf 5055 ‘cfv 5059 (class class class)co 5706 Topctop 11946 TopOnctopon 11959 neicnei 12089 CnP ccnp 12137

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 584 ax-in2 585 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-13 1459 ax-14 1460 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 ax-coll 3983 ax-sep 3986 ax-pow 4038 ax-pr 4069 ax-un 4293 ax-setind 4390

This theorem depends on definitions: df-bi 116 df-3an 932 df-tru 1302 df-fal 1305 df-nf 1405 df-sb 1704 df-eu 1963 df-mo 1964 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-ne 2268 df-ral 2380 df-rex 2381 df-reu 2382 df-rab 2384 df-v 2643 df-sbc 2863 df-csb 2956 df-dif 3023 df-un 3025 df-in 3027 df-ss 3034 df-pw 3459 df-sn 3480 df-pr 3481 df-op 3483 df-uni 3684 df-iun 3762 df-br 3876 df-opab 3930 df-mpt 3931 df-id 4153 df-xp 4483 df-rel 4484 df-cnv 4485 df-co 4486 df-dm 4487 df-rn 4488 df-res 4489 df-ima 4490 df-iota 5024 df-fun 5061 df-fn 5062 df-f 5063 df-f1 5064 df-fo 5065 df-f1o 5066 df-fv 5067 df-ov 5709 df-oprab 5710 df-mpo 5711 df-1st 5969 df-2nd 5970 df-map 6474 df-top 11947 df-topon 11960 df-nei 12090 df-cnp 12140

This theorem is referenced by: (None)

W3C validator