cnpnei - Metamath Proof Explorer

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

Theorem cnpnei 23543

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 6072	. . . . . . . 8 ⊢ (^◡𝐹 “ 𝑦) ⊆ dom 𝐹
2		fdm 6707	. . . . . . . 8 ⊢ (𝐹:𝑋⟶𝑌 → dom 𝐹 = 𝑋)
3	1, 2	sseqtrid 3972	. . . . . . 7 ⊢ (𝐹:𝑋⟶𝑌 → (^◡𝐹 “ 𝑦) ⊆ 𝑋)
4	3	3ad2ant3 1153	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → (^◡𝐹 “ 𝑦) ⊆ 𝑋)
5	4	ad2antrr 739	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → (^◡𝐹 “ 𝑦) ⊆ 𝑋)
6		neii2 23387	. . . . . . . 8 ⊢ ((𝐾 ∈ Top ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) → ∃𝑔 ∈ 𝐾 ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))
7	6	3ad2antl2 1205	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) → ∃𝑔 ∈ 𝐾 ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))
8	7	ad2ant2rl 762	. . . . . 6 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → ∃𝑔 ∈ 𝐾 ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))
9		simpll 779	. . . . . . . . . 10 ⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
10		simprl 783	. . . . . . . . . 10 ⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → 𝑔 ∈ 𝐾)
11		fvex 6886	. . . . . . . . . . . . 13 ⊢ (𝐹‘𝐴) ∈ V
12	11	snss 4744	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝐴) ∈ 𝑔 ↔ {(𝐹‘𝐴)} ⊆ 𝑔)
13	12	biranri 511	. . . . . . . . . . 11 ⊢ (({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦) → (𝐹‘𝐴) ∈ 𝑔)
14	13	ad2antll 742	. . . . . . . . . 10 ⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (𝐹‘𝐴) ∈ 𝑔)
15	9, 10, 14	3jca 1146	. . . . . . . . 9 ⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑔))
16	15	adantll 727	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑔))
17		cnpimaex 23535	. . . . . . . 8 ⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑔) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔))
18	16, 17	syl 18	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔))
19		sstr2 3937	. . . . . . . . . . . . 13 ⊢ ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝑔 ⊆ 𝑦 → (𝐹 “ 𝑜) ⊆ 𝑦))
20	19	com12 33	. . . . . . . . . . . 12 ⊢ (𝑔 ⊆ 𝑦 → ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝐹 “ 𝑜) ⊆ 𝑦))
21	20	ad2antll 742	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)) → ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝐹 “ 𝑜) ⊆ 𝑦))
22	21	ad2antlr 740	. . . . . . . . . 10 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝐹 “ 𝑜) ⊆ 𝑦))
23		ffun 6700	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝑋⟶𝑌 → Fun 𝐹)
24	23	3ad2ant3 1153	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → Fun 𝐹)
25	24	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → Fun 𝐹)
26	25	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → Fun 𝐹)
27		cnpnei.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝑋 = ∪ 𝐽
28	27	eltopss 23186	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ 𝑋)
29	28	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ 𝑋)
30	2	sseq2d 3962	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑋⟶𝑌 → (𝑜 ⊆ dom 𝐹 ↔ 𝑜 ⊆ 𝑋))
31	30	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → (𝑜 ⊆ dom 𝐹 ↔ 𝑜 ⊆ 𝑋))
32	29, 31	mpbird 260	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
33	32	3adantl2 1186	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
34	33	adantlr 728	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
35	34	ad4ant14 765	. . . . . . . . . . 11 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
36		funimass3 7041	. . . . . . . . . . 11 ⊢ ((Fun 𝐹 ∧ 𝑜 ⊆ dom 𝐹) → ((𝐹 “ 𝑜) ⊆ 𝑦 ↔ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
37	26, 35, 36	syl2anc 596	. . . . . . . . . 10 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐹 “ 𝑜) ⊆ 𝑦 ↔ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
38	22, 37	sylibd 242	. . . . . . . . 9 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐹 “ 𝑜) ⊆ 𝑔 → 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
39	38	anim2d 624	. . . . . . . 8 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔) → (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦))))
40	39	reximdva 3175	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦))))
41	18, 40	mpd 16	. . . . . 6 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
42	8, 41	rexlimddv 3169	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
43	27	isneip 23384	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋) → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((^◡𝐹 “ 𝑦) ⊆ 𝑋 ∧ ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))))
44	43	3ad2antl1 1204	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((^◡𝐹 “ 𝑦) ⊆ 𝑋 ∧ ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))))
45	44	adantr 486	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((^◡𝐹 “ 𝑦) ⊆ 𝑋 ∧ ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))))
46	5, 42, 45	mpbir2and 726	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → (^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}))
47	46	exp32 426	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → (𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}) → (^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}))))
48	47	ralrimdv 3160	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})))
49		simpll3 1233	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → 𝐹:𝑋⟶𝑌)
50		opnneip 23398	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Top ∧ 𝑜 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑜) → 𝑜 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))
51		imaeq2 6046	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑜 → (^◡𝐹 “ 𝑦) = (^◡𝐹 “ 𝑜))
52	51	eleq1d 2845	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑜 → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
53	52	rspcv 3572	. . . . . . . . . . . . . 14 ⊢ (𝑜 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
54	50, 53	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑜 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑜) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
55	54	3com23 1144	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Top ∧ (𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
56	55	3expb 1138	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Top ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
57	56	3ad2antl2 1205	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
58	57	adantlr 728	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
59		neii2 23387	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜)))
60	59	ex 418	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → ((^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
61	60	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → ((^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
62	61	ad2antrr 739	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → ((^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
63		snssg 4743	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ 𝑔 ↔ {𝐴} ⊆ 𝑔))
64	63	ad3antlr 744	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → (𝐴 ∈ 𝑔 ↔ {𝐴} ⊆ 𝑔))
65	24	ad3antrrr 743	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → Fun 𝐹)
66	27	eltopss 23186	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ 𝑋)
67	66	3ad2antl1 1204	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ 𝑋)
68	2	sseq2d 3962	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋⟶𝑌 → (𝑔 ⊆ dom 𝐹 ↔ 𝑔 ⊆ 𝑋))
69	68	3ad2ant3 1153	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → (𝑔 ⊆ dom 𝐹 ↔ 𝑔 ⊆ 𝑋))
70	69	biimpar 483	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ⊆ 𝑋) → 𝑔 ⊆ dom 𝐹)
71	67, 70	syldan 603	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ dom 𝐹)
72	71	ad4ant14 765	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ dom 𝐹)
73		funimass3 7041	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐹 ∧ 𝑔 ⊆ dom 𝐹) → ((𝐹 “ 𝑔) ⊆ 𝑜 ↔ 𝑔 ⊆ (^◡𝐹 “ 𝑜)))
74	65, 72, 73	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → ((𝐹 “ 𝑔) ⊆ 𝑜 ↔ 𝑔 ⊆ (^◡𝐹 “ 𝑜)))
75	64, 74	anbi12d 644	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → ((𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜) ↔ ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
76	75	biimprd 251	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → (({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜)) → (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
77	76	reximdva 3175	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜)) → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
78	58, 62, 77	3syld 61	. . . . . . . 8 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
79	78	exp32 426	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝐴) ∈ 𝑜 → (𝑜 ∈ 𝐾 → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
80	79	com24 96	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝑜 ∈ 𝐾 → ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
81	80	imp 412	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → (𝑜 ∈ 𝐾 → ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜))))
82	81	ralrimiv 3153	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
83		cnpnei.2	. . . . . . . . 9 ⊢ 𝑌 = ∪ 𝐾
84	27, 83	iscnp2 23518	. . . . . . . 8 ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
85	84	baib 545	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
86	85	3expa 1136	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
87	86	3adantl3 1187	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
88	87	adantr 486	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
89	49, 82, 88	mpbir2and 726	. . 3 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
90	89	ex 418	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)))
91	48, 90	impbid 215	1 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∀wral 3076 ∃wrex 3086 ⊆ wss 3898 {csn 4583 ∪ cuni 4866 ^◡ccnv 5646 dom cdm 5647 “ cima 5650 Fun wfun 6521 ⟶wf 6523 ‘cfv 6527 (class class class)co 7408 Topctop 23172 neicnei 23376 CnP ccnp 23504

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7734

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5542 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-iota 6483 df-fun 6529 df-fn 6530 df-f 6531 df-f1 6532 df-fo 6533 df-f1o 6534 df-fv 6535 df-ov 7411 df-oprab 7412 df-mpo 7413 df-1st 7984 df-2nd 7985 df-map 8827 df-top 23173 df-topon 23190 df-nei 23377 df-cnp 23507

This theorem is used by: (None)

W3C validator