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 21874

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 5951	. . . . . . . 8 ⊢ (^◡𝐹 “ 𝑦) ⊆ dom 𝐹
2		fdm 6524	. . . . . . . 8 ⊢ (𝐹:𝑋⟶𝑌 → dom 𝐹 = 𝑋)
3	1, 2	sseqtrid 4021	. . . . . . 7 ⊢ (𝐹:𝑋⟶𝑌 → (^◡𝐹 “ 𝑦) ⊆ 𝑋)
4	3	3ad2ant3 1131	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → (^◡𝐹 “ 𝑦) ⊆ 𝑋)
5	4	ad2antrr 724	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → (^◡𝐹 “ 𝑦) ⊆ 𝑋)
6		neii2 21718	. . . . . . . 8 ⊢ ((𝐾 ∈ Top ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) → ∃𝑔 ∈ 𝐾 ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))
7	6	3ad2antl2 1182	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) → ∃𝑔 ∈ 𝐾 ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))
8	7	ad2ant2rl 747	. . . . . 6 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → ∃𝑔 ∈ 𝐾 ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))
9		simpll 765	. . . . . . . . . 10 ⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
10		simprl 769	. . . . . . . . . 10 ⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → 𝑔 ∈ 𝐾)
11		fvex 6685	. . . . . . . . . . . . . 14 ⊢ (𝐹‘𝐴) ∈ V
12	11	snss 4720	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝐴) ∈ 𝑔 ↔ {(𝐹‘𝐴)} ⊆ 𝑔)
13	12	biimpri 230	. . . . . . . . . . . 12 ⊢ ({(𝐹‘𝐴)} ⊆ 𝑔 → (𝐹‘𝐴) ∈ 𝑔)
14	13	adantr 483	. . . . . . . . . . 11 ⊢ (({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦) → (𝐹‘𝐴) ∈ 𝑔)
15	14	ad2antll 727	. . . . . . . . . 10 ⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (𝐹‘𝐴) ∈ 𝑔)
16	9, 10, 15	3jca 1124	. . . . . . . . 9 ⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑔))
17	16	adantll 712	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑔))
18		cnpimaex 21866	. . . . . . . 8 ⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑔) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔))
19	17, 18	syl 17	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔))
20		sstr2 3976	. . . . . . . . . . . . 13 ⊢ ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝑔 ⊆ 𝑦 → (𝐹 “ 𝑜) ⊆ 𝑦))
21	20	com12 32	. . . . . . . . . . . 12 ⊢ (𝑔 ⊆ 𝑦 → ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝐹 “ 𝑜) ⊆ 𝑦))
22	21	ad2antll 727	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)) → ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝐹 “ 𝑜) ⊆ 𝑦))
23	22	ad2antlr 725	. . . . . . . . . 10 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝐹 “ 𝑜) ⊆ 𝑦))
24		ffun 6519	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝑋⟶𝑌 → Fun 𝐹)
25	24	3ad2ant3 1131	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → Fun 𝐹)
26	25	ad2antrr 724	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → Fun 𝐹)
27	26	ad2antrr 724	. . . . . . . . . . 11 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → Fun 𝐹)
28		cnpnei.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝑋 = ∪ 𝐽
29	28	eltopss 21517	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ 𝑋)
30	29	adantlr 713	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ 𝑋)
31	2	sseq2d 4001	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑋⟶𝑌 → (𝑜 ⊆ dom 𝐹 ↔ 𝑜 ⊆ 𝑋))
32	31	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → (𝑜 ⊆ dom 𝐹 ↔ 𝑜 ⊆ 𝑋))
33	30, 32	mpbird 259	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
34	33	3adantl2 1163	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
35	34	adantlr 713	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
36	35	ad4ant14 750	. . . . . . . . . . 11 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
37		funimass3 6826	. . . . . . . . . . 11 ⊢ ((Fun 𝐹 ∧ 𝑜 ⊆ dom 𝐹) → ((𝐹 “ 𝑜) ⊆ 𝑦 ↔ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
38	27, 36, 37	syl2anc 586	. . . . . . . . . 10 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐹 “ 𝑜) ⊆ 𝑦 ↔ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
39	23, 38	sylibd 241	. . . . . . . . 9 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐹 “ 𝑜) ⊆ 𝑔 → 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
40	39	anim2d 613	. . . . . . . 8 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔) → (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦))))
41	40	reximdva 3276	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦))))
42	19, 41	mpd 15	. . . . . 6 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
43	8, 42	rexlimddv 3293	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
44	28	isneip 21715	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋) → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((^◡𝐹 “ 𝑦) ⊆ 𝑋 ∧ ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))))
45	44	3ad2antl1 1181	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((^◡𝐹 “ 𝑦) ⊆ 𝑋 ∧ ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))))
46	45	adantr 483	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((^◡𝐹 “ 𝑦) ⊆ 𝑋 ∧ ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))))
47	5, 43, 46	mpbir2and 711	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → (^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}))
48	47	exp32 423	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → (𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}) → (^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}))))
49	48	ralrimdv 3190	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})))
50		simpll3 1210	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → 𝐹:𝑋⟶𝑌)
51		opnneip 21729	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Top ∧ 𝑜 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑜) → 𝑜 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))
52		imaeq2 5927	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑜 → (^◡𝐹 “ 𝑦) = (^◡𝐹 “ 𝑜))
53	52	eleq1d 2899	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑜 → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
54	53	rspcv 3620	. . . . . . . . . . . . . 14 ⊢ (𝑜 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
55	51, 54	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑜 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑜) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
56	55	3com23 1122	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Top ∧ (𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
57	56	3expb 1116	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Top ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
58	57	3ad2antl2 1182	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
59	58	adantlr 713	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
60		neii2 21718	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜)))
61	60	ex 415	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → ((^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
62	61	3ad2ant1 1129	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → ((^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
63	62	ad2antrr 724	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → ((^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
64		snssg 4719	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ 𝑔 ↔ {𝐴} ⊆ 𝑔))
65	64	ad3antlr 729	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → (𝐴 ∈ 𝑔 ↔ {𝐴} ⊆ 𝑔))
66	25	ad3antrrr 728	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → Fun 𝐹)
67	28	eltopss 21517	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ 𝑋)
68	67	3ad2antl1 1181	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ 𝑋)
69	2	sseq2d 4001	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋⟶𝑌 → (𝑔 ⊆ dom 𝐹 ↔ 𝑔 ⊆ 𝑋))
70	69	3ad2ant3 1131	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → (𝑔 ⊆ dom 𝐹 ↔ 𝑔 ⊆ 𝑋))
71	70	biimpar 480	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ⊆ 𝑋) → 𝑔 ⊆ dom 𝐹)
72	68, 71	syldan 593	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ dom 𝐹)
73	72	ad4ant14 750	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ dom 𝐹)
74		funimass3 6826	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐹 ∧ 𝑔 ⊆ dom 𝐹) → ((𝐹 “ 𝑔) ⊆ 𝑜 ↔ 𝑔 ⊆ (^◡𝐹 “ 𝑜)))
75	66, 73, 74	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → ((𝐹 “ 𝑔) ⊆ 𝑜 ↔ 𝑔 ⊆ (^◡𝐹 “ 𝑜)))
76	65, 75	anbi12d 632	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → ((𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜) ↔ ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
77	76	biimprd 250	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → (({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜)) → (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
78	77	reximdva 3276	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜)) → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
79	59, 63, 78	3syld 60	. . . . . . . 8 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
80	79	exp32 423	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝐴) ∈ 𝑜 → (𝑜 ∈ 𝐾 → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
81	80	com24 95	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝑜 ∈ 𝐾 → ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
82	81	imp 409	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → (𝑜 ∈ 𝐾 → ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜))))
83	82	ralrimiv 3183	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
84		cnpnei.2	. . . . . . . . 9 ⊢ 𝑌 = ∪ 𝐾
85	28, 84	iscnp2 21849	. . . . . . . 8 ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
86	85	baib 538	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
87	86	3expa 1114	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
88	87	3adantl3 1164	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
89	88	adantr 483	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
90	50, 83, 89	mpbir2and 711	. . 3 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
91	90	ex 415	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)))
92	49, 91	impbid 214	1 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 ∀wral 3140 ∃wrex 3141 ⊆ wss 3938 {csn 4569 ∪ cuni 4840 ^◡ccnv 5556 dom cdm 5557 “ cima 5560 Fun wfun 6351 ⟶wf 6353 ‘cfv 6357 (class class class)co 7158 Topctop 21503 neicnei 21707 CnP ccnp 21835

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-ral 3145 df-rex 3146 df-reu 3147 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-op 4576 df-uni 4841 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-id 5462 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-ov 7161 df-oprab 7162 df-mpo 7163 df-1st 7691 df-2nd 7692 df-map 8410 df-top 21504 df-topon 21521 df-nei 21708 df-cnp 21838

This theorem is referenced by: (None)

W3C validator