cnpnei - Intuitionistic Logic Explorer

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

Theorem cnpnei 13013

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 4974	. . . . . . . 8 ⊢ (^◡𝐹 “ 𝑦) ⊆ dom 𝐹
2		fdm 5353	. . . . . . . 8 ⊢ (𝐹:𝑋⟶𝑌 → dom 𝐹 = 𝑋)
3	1, 2	sseqtrid 3197	. . . . . . 7 ⊢ (𝐹:𝑋⟶𝑌 → (^◡𝐹 “ 𝑦) ⊆ 𝑋)
4	3	3ad2ant3 1015	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → (^◡𝐹 “ 𝑦) ⊆ 𝑋)
5	4	ad2antrr 485	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → (^◡𝐹 “ 𝑦) ⊆ 𝑋)
6		neii2 12943	. . . . . . . 8 ⊢ ((𝐾 ∈ Top ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) → ∃𝑔 ∈ 𝐾 ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))
7	6	3ad2antl2 1155	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) → ∃𝑔 ∈ 𝐾 ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))
8	7	ad2ant2rl 508	. . . . . 6 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → ∃𝑔 ∈ 𝐾 ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))
9		cnpnei.1	. . . . . . . . . . . 12 ⊢ 𝑋 = ∪ 𝐽
10	9	toptopon 12810	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
11	10	biimpi 119	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → 𝐽 ∈ (TopOn‘𝑋))
12	11	3ad2ant1 1013	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → 𝐽 ∈ (TopOn‘𝑋))
13	12	ad3antrrr 489	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → 𝐽 ∈ (TopOn‘𝑋))
14		cnpnei.2	. . . . . . . . . . . 12 ⊢ 𝑌 = ∪ 𝐾
15	14	toptopon 12810	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌))
16	15	biimpi 119	. . . . . . . . . 10 ⊢ (𝐾 ∈ Top → 𝐾 ∈ (TopOn‘𝑌))
17	16	3ad2ant2 1014	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → 𝐾 ∈ (TopOn‘𝑌))
18	17	ad3antrrr 489	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → 𝐾 ∈ (TopOn‘𝑌))
19		simpllr 529	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → 𝐴 ∈ 𝑋)
20		simplrl 530	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
21		simprl 526	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → 𝑔 ∈ 𝐾)
22		simprrl 534	. . . . . . . . 9 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → {(𝐹‘𝐴)} ⊆ 𝑔)
23		fvexg 5515	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ∈ V)
24	20, 19, 23	syl2anc 409	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (𝐹‘𝐴) ∈ V)
25		snssg 3716	. . . . . . . . . 10 ⊢ ((𝐹‘𝐴) ∈ V → ((𝐹‘𝐴) ∈ 𝑔 ↔ {(𝐹‘𝐴)} ⊆ 𝑔))
26	24, 25	syl 14	. . . . . . . . 9 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → ((𝐹‘𝐴) ∈ 𝑔 ↔ {(𝐹‘𝐴)} ⊆ 𝑔))
27	22, 26	mpbird 166	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (𝐹‘𝐴) ∈ 𝑔)
28		icnpimaex 13005	. . . . . . . 8 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑔)) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔))
29	13, 18, 19, 20, 21, 27, 28	syl33anc 1248	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔))
30		sstr2 3154	. . . . . . . . . . . . 13 ⊢ ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝑔 ⊆ 𝑦 → (𝐹 “ 𝑜) ⊆ 𝑦))
31	30	com12 30	. . . . . . . . . . . 12 ⊢ (𝑔 ⊆ 𝑦 → ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝐹 “ 𝑜) ⊆ 𝑦))
32	31	ad2antll 488	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)) → ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝐹 “ 𝑜) ⊆ 𝑦))
33	32	ad2antlr 486	. . . . . . . . . 10 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝐹 “ 𝑜) ⊆ 𝑦))
34		ffun 5350	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝑋⟶𝑌 → Fun 𝐹)
35	34	3ad2ant3 1015	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → Fun 𝐹)
36	35	ad2antrr 485	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → Fun 𝐹)
37	36	ad2antrr 485	. . . . . . . . . . 11 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → Fun 𝐹)
38	9	eltopss 12801	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ 𝑋)
39	38	adantlr 474	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ 𝑋)
40	2	sseq2d 3177	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋⟶𝑌 → (𝑜 ⊆ dom 𝐹 ↔ 𝑜 ⊆ 𝑋))
41	40	ad2antlr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → (𝑜 ⊆ dom 𝐹 ↔ 𝑜 ⊆ 𝑋))
42	39, 41	mpbird 166	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
43	42	3adantl2 1149	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
44	43	adantlr 474	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
45	44	adantlr 474	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
46	45	adantlr 474	. . . . . . . . . . 11 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
47		funimass3 5612	. . . . . . . . . . 11 ⊢ ((Fun 𝐹 ∧ 𝑜 ⊆ dom 𝐹) → ((𝐹 “ 𝑜) ⊆ 𝑦 ↔ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
48	37, 46, 47	syl2anc 409	. . . . . . . . . 10 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐹 “ 𝑜) ⊆ 𝑦 ↔ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
49	33, 48	sylibd 148	. . . . . . . . 9 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐹 “ 𝑜) ⊆ 𝑔 → 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
50	49	anim2d 335	. . . . . . . 8 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔) → (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦))))
51	50	reximdva 2572	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦))))
52	29, 51	mpd 13	. . . . . 6 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
53	8, 52	rexlimddv 2592	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
54	9	isneip 12940	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋) → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((^◡𝐹 “ 𝑦) ⊆ 𝑋 ∧ ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))))
55	54	3ad2antl1 1154	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((^◡𝐹 “ 𝑦) ⊆ 𝑋 ∧ ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))))
56	55	adantr 274	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((^◡𝐹 “ 𝑦) ⊆ 𝑋 ∧ ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))))
57	5, 53, 56	mpbir2and 939	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → (^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}))
58	57	exp32 363	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → (𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}) → (^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}))))
59	58	ralrimdv 2549	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})))
60		simpll3 1033	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → 𝐹:𝑋⟶𝑌)
61		opnneip 12953	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Top ∧ 𝑜 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑜) → 𝑜 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))
62		imaeq2 4949	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑜 → (^◡𝐹 “ 𝑦) = (^◡𝐹 “ 𝑜))
63	62	eleq1d 2239	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑜 → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
64	63	rspcv 2830	. . . . . . . . . . . . . 14 ⊢ (𝑜 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
65	61, 64	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑜 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑜) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
66	65	3com23 1204	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Top ∧ (𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
67	66	3expb 1199	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Top ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
68	67	3ad2antl2 1155	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
69	68	adantlr 474	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
70		neii2 12943	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜)))
71	70	ex 114	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → ((^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
72	71	3ad2ant1 1013	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → ((^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
73	72	ad2antrr 485	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → ((^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
74		snssg 3716	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ 𝑔 ↔ {𝐴} ⊆ 𝑔))
75	74	ad3antlr 490	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → (𝐴 ∈ 𝑔 ↔ {𝐴} ⊆ 𝑔))
76	35	ad3antrrr 489	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → Fun 𝐹)
77	9	eltopss 12801	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ 𝑋)
78	77	3ad2antl1 1154	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ 𝑋)
79	2	sseq2d 3177	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:𝑋⟶𝑌 → (𝑔 ⊆ dom 𝐹 ↔ 𝑔 ⊆ 𝑋))
80	79	3ad2ant3 1015	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → (𝑔 ⊆ dom 𝐹 ↔ 𝑔 ⊆ 𝑋))
81	80	biimpar 295	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ⊆ 𝑋) → 𝑔 ⊆ dom 𝐹)
82	78, 81	syldan 280	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ dom 𝐹)
83	82	adantlr 474	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ dom 𝐹)
84	83	adantlr 474	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ dom 𝐹)
85		funimass3 5612	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐹 ∧ 𝑔 ⊆ dom 𝐹) → ((𝐹 “ 𝑔) ⊆ 𝑜 ↔ 𝑔 ⊆ (^◡𝐹 “ 𝑜)))
86	76, 84, 85	syl2anc 409	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → ((𝐹 “ 𝑔) ⊆ 𝑜 ↔ 𝑔 ⊆ (^◡𝐹 “ 𝑜)))
87	75, 86	anbi12d 470	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → ((𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜) ↔ ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
88	87	biimprd 157	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → (({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜)) → (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
89	88	reximdva 2572	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜)) → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
90	69, 73, 89	3syld 57	. . . . . . . 8 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
91	90	exp32 363	. . . . . . 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 2542	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
95	11	3ad2ant1 1013	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑋))
96	16	3ad2ant2 1014	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋) → 𝐾 ∈ (TopOn‘𝑌))
97		simp3 994	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑋)
98		iscnp 12993	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
99	95, 96, 97, 98	syl3anc 1233	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
100	99	3expa 1198	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
101	100	3adantl3 1150	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
102	101	adantr 274	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
103	60, 94, 102	mpbir2and 939	. . 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 973 = wceq 1348 ∈ wcel 2141 ∀wral 2448 ∃wrex 2449 Vcvv 2730 ⊆ wss 3121 {csn 3583 ∪ cuni 3796 ^◡ccnv 4610 dom cdm 4611 “ cima 4614 Fun wfun 5192 ⟶wf 5194 ‘cfv 5198 (class class class)co 5853 Topctop 12789 TopOnctopon 12802 neicnei 12932 CnP ccnp 12980

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4104 ax-sep 4107 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-setind 4521

This theorem depends on definitions: df-bi 116 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-ral 2453 df-rex 2454 df-reu 2455 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-iun 3875 df-br 3990 df-opab 4051 df-mpt 4052 df-id 4278 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-f1 5203 df-fo 5204 df-f1o 5205 df-fv 5206 df-ov 5856 df-oprab 5857 df-mpo 5858 df-1st 6119 df-2nd 6120 df-map 6628 df-top 12790 df-topon 12803 df-nei 12933 df-cnp 12983

This theorem is referenced by: (None)

W3C validator