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 22615

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 6033	. . . . . . . 8 ⊢ (^◡𝐹 “ 𝑦) ⊆ dom 𝐹
2		fdm 6677	. . . . . . . 8 ⊢ (𝐹:𝑋⟶𝑌 → dom 𝐹 = 𝑋)
3	1, 2	sseqtrid 3996	. . . . . . 7 ⊢ (𝐹:𝑋⟶𝑌 → (^◡𝐹 “ 𝑦) ⊆ 𝑋)
4	3	3ad2ant3 1135	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → (^◡𝐹 “ 𝑦) ⊆ 𝑋)
5	4	ad2antrr 724	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → (^◡𝐹 “ 𝑦) ⊆ 𝑋)
6		neii2 22459	. . . . . . . 8 ⊢ ((𝐾 ∈ Top ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) → ∃𝑔 ∈ 𝐾 ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))
7	6	3ad2antl2 1186	. . . . . . 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 6855	. . . . . . . . . . . . . 14 ⊢ (𝐹‘𝐴) ∈ V
12	11	snss 4746	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝐴) ∈ 𝑔 ↔ {(𝐹‘𝐴)} ⊆ 𝑔)
13	12	biimpri 227	. . . . . . . . . . . 12 ⊢ ({(𝐹‘𝐴)} ⊆ 𝑔 → (𝐹‘𝐴) ∈ 𝑔)
14	13	adantr 481	. . . . . . . . . . 11 ⊢ (({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦) → (𝐹‘𝐴) ∈ 𝑔)
15	14	ad2antll 727	. . . . . . . . . 10 ⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (𝐹‘𝐴) ∈ 𝑔)
16	9, 10, 15	3jca 1128	. . . . . . . . 9 ⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑔))
17	16	adantll 712	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑔))
18		cnpimaex 22607	. . . . . . . 8 ⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑔) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔))
19	17, 18	syl 17	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔))
20		sstr2 3951	. . . . . . . . . . . . 13 ⊢ ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝑔 ⊆ 𝑦 → (𝐹 “ 𝑜) ⊆ 𝑦))
21	20	com12 32	. . . . . . . . . . . 12 ⊢ (𝑔 ⊆ 𝑦 → ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝐹 “ 𝑜) ⊆ 𝑦))
22	21	ad2antll 727	. . . . . . . . . . 11 ⊢ ((𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)) → ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝐹 “ 𝑜) ⊆ 𝑦))
23	22	ad2antlr 725	. . . . . . . . . 10 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐹 “ 𝑜) ⊆ 𝑔 → (𝐹 “ 𝑜) ⊆ 𝑦))
24		ffun 6671	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝑋⟶𝑌 → Fun 𝐹)
25	24	3ad2ant3 1135	. . . . . . . . . . . . 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 22256	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ 𝑋)
30	29	adantlr 713	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ 𝑋)
31	2	sseq2d 3976	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑋⟶𝑌 → (𝑜 ⊆ dom 𝐹 ↔ 𝑜 ⊆ 𝑋))
32	31	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → (𝑜 ⊆ dom 𝐹 ↔ 𝑜 ⊆ 𝑋))
33	30, 32	mpbird 256	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
34	33	3adantl2 1167	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
35	34	adantlr 713	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
36	35	ad4ant14 750	. . . . . . . . . . 11 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ dom 𝐹)
37		funimass3 7004	. . . . . . . . . . 11 ⊢ ((Fun 𝐹 ∧ 𝑜 ⊆ dom 𝐹) → ((𝐹 “ 𝑜) ⊆ 𝑦 ↔ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
38	27, 36, 37	syl2anc 584	. . . . . . . . . 10 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐹 “ 𝑜) ⊆ 𝑦 ↔ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
39	23, 38	sylibd 238	. . . . . . . . 9 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐹 “ 𝑜) ⊆ 𝑔 → 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
40	39	anim2d 612	. . . . . . . 8 ⊢ ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) ∧ 𝑜 ∈ 𝐽) → ((𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔) → (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦))))
41	40	reximdva 3165	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → (∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ (𝐹 “ 𝑜) ⊆ 𝑔) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦))))
42	19, 41	mpd 15	. . . . . 6 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(𝐹‘𝐴)} ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦))) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
43	8, 42	rexlimddv 3158	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))
44	28	isneip 22456	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋) → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((^◡𝐹 “ 𝑦) ⊆ 𝑋 ∧ ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))))
45	44	3ad2antl1 1185	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((^◡𝐹 “ 𝑦) ⊆ 𝑋 ∧ ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))))
46	45	adantr 481	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((^◡𝐹 “ 𝑦) ⊆ 𝑋 ∧ ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ (^◡𝐹 “ 𝑦)))))
47	5, 43, 46	mpbir2and 711	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))) → (^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}))
48	47	exp32 421	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → (𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}) → (^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}))))
49	48	ralrimdv 3149	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})))
50		simpll3 1214	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → 𝐹:𝑋⟶𝑌)
51		opnneip 22470	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Top ∧ 𝑜 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑜) → 𝑜 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}))
52		imaeq2 6009	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑜 → (^◡𝐹 “ 𝑦) = (^◡𝐹 “ 𝑜))
53	52	eleq1d 2822	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑜 → ((^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
54	53	rspcv 3577	. . . . . . . . . . . . . 14 ⊢ (𝑜 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)}) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
55	51, 54	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝑜 ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ 𝑜) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
56	55	3com23 1126	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Top ∧ (𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
57	56	3expb 1120	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Top ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
58	57	3ad2antl2 1186	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
59	58	adantlr 713	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
60		neii2 22459	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ (^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴})) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜)))
61	60	ex 413	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → ((^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
62	61	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → ((^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
63	62	ad2antrr 724	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → ((^◡𝐹 “ 𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
64		snssg 4744	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ 𝑔 ↔ {𝐴} ⊆ 𝑔))
65	64	ad3antlr 729	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → (𝐴 ∈ 𝑔 ↔ {𝐴} ⊆ 𝑔))
66	25	ad3antrrr 728	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → Fun 𝐹)
67	28	eltopss 22256	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ 𝑋)
68	67	3ad2antl1 1185	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ 𝑋)
69	2	sseq2d 3976	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋⟶𝑌 → (𝑔 ⊆ dom 𝐹 ↔ 𝑔 ⊆ 𝑋))
70	69	3ad2ant3 1135	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → (𝑔 ⊆ dom 𝐹 ↔ 𝑔 ⊆ 𝑋))
71	70	biimpar 478	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ⊆ 𝑋) → 𝑔 ⊆ dom 𝐹)
72	68, 71	syldan 591	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ dom 𝐹)
73	72	ad4ant14 750	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → 𝑔 ⊆ dom 𝐹)
74		funimass3 7004	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐹 ∧ 𝑔 ⊆ dom 𝐹) → ((𝐹 “ 𝑔) ⊆ 𝑜 ↔ 𝑔 ⊆ (^◡𝐹 “ 𝑜)))
75	66, 73, 74	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → ((𝐹 “ 𝑔) ⊆ 𝑜 ↔ 𝑔 ⊆ (^◡𝐹 “ 𝑜)))
76	65, 75	anbi12d 631	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → ((𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜) ↔ ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜))))
77	76	biimprd 247	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) → (({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜)) → (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
78	77	reximdva 3165	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∃𝑔 ∈ 𝐽 ({𝐴} ⊆ 𝑔 ∧ 𝑔 ⊆ (^◡𝐹 “ 𝑜)) → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
79	59, 63, 78	3syld 60	. . . . . . . 8 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ((𝐹‘𝐴) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
80	79	exp32 421	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝐴) ∈ 𝑜 → (𝑜 ∈ 𝐾 → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
81	80	com24 95	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝑜 ∈ 𝐾 → ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
82	81	imp 407	. . . . 5 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → (𝑜 ∈ 𝐾 → ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜))))
83	82	ralrimiv 3142	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))
84		cnpnei.2	. . . . . . . . 9 ⊢ 𝑌 = ∪ 𝐾
85	28, 84	iscnp2 22590	. . . . . . . 8 ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
86	85	baib 536	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
87	86	3expa 1118	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
88	87	3adantl3 1168	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
89	88	adantr 481	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑜 ∈ 𝐾 ((𝐹‘𝐴) ∈ 𝑜 → ∃𝑔 ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 “ 𝑔) ⊆ 𝑜)))))
90	50, 83, 89	mpbir2and 711	. . 3 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
91	90	ex 413	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)))
92	49, 91	impbid 211	1 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(^◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∀wral 3064 ∃wrex 3073 ⊆ wss 3910 {csn 4586 ∪ cuni 4865 ^◡ccnv 5632 dom cdm 5633 “ cima 5636 Fun wfun 6490 ⟶wf 6492 ‘cfv 6496 (class class class)co 7357 Topctop 22242 neicnei 22448 CnP ccnp 22576

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-ov 7360 df-oprab 7361 df-mpo 7362 df-1st 7921 df-2nd 7922 df-map 8767 df-top 22243 df-topon 22260 df-nei 22449 df-cnp 22579

This theorem is referenced by: (None)

W3C validator