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.
StepHypRef Expression
1 cnvimass 4838 . . . . . . . 8 (𝐹𝑦) ⊆ dom 𝐹
2 fdm 5214 . . . . . . . 8 (𝐹:𝑋𝑌 → dom 𝐹 = 𝑋)
31, 2syl5sseq 3097 . . . . . . 7 (𝐹:𝑋𝑌 → (𝐹𝑦) ⊆ 𝑋)
433ad2ant3 972 . . . . . 6 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → (𝐹𝑦) ⊆ 𝑋)
54ad2antrr 475 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → (𝐹𝑦) ⊆ 𝑋)
6 neii2 12100 . . . . . . . 8 ((𝐾 ∈ Top ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) → ∃𝑔𝐾 ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))
763ad2antl2 1112 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) → ∃𝑔𝐾 ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))
87ad2ant2rl 498 . . . . . 6 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → ∃𝑔𝐾 ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))
9 cnpnei.1 . . . . . . . . . . . 12 𝑋 = 𝐽
109toptopon 11967 . . . . . . . . . . 11 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
1110biimpi 119 . . . . . . . . . 10 (𝐽 ∈ Top → 𝐽 ∈ (TopOn‘𝑋))
12113ad2ant1 970 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → 𝐽 ∈ (TopOn‘𝑋))
1312ad3antrrr 479 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → 𝐽 ∈ (TopOn‘𝑋))
14 cnpnei.2 . . . . . . . . . . . 12 𝑌 = 𝐾
1514toptopon 11967 . . . . . . . . . . 11 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌))
1615biimpi 119 . . . . . . . . . 10 (𝐾 ∈ Top → 𝐾 ∈ (TopOn‘𝑌))
17163ad2ant2 971 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → 𝐾 ∈ (TopOn‘𝑌))
1817ad3antrrr 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)
2420, 19, 23syl2anc 406 . . . . . . . . . 10 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → (𝐹𝐴) ∈ V)
25 snssg 3603 . . . . . . . . . 10 ((𝐹𝐴) ∈ V → ((𝐹𝐴) ∈ 𝑔 ↔ {(𝐹𝐴)} ⊆ 𝑔))
2624, 25syl 14 . . . . . . . . 9 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → ((𝐹𝐴) ∈ 𝑔 ↔ {(𝐹𝐴)} ⊆ 𝑔))
2722, 26mpbird 166 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → (𝐹𝐴) ∈ 𝑔)
28 icnpimaex 12161 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔𝐾 ∧ (𝐹𝐴) ∈ 𝑔)) → ∃𝑜𝐽 (𝐴𝑜 ∧ (𝐹𝑜) ⊆ 𝑔))
2913, 18, 19, 20, 21, 27, 28syl33anc 1199 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → ∃𝑜𝐽 (𝐴𝑜 ∧ (𝐹𝑜) ⊆ 𝑔))
30 sstr2 3054 . . . . . . . . . . . . 13 ((𝐹𝑜) ⊆ 𝑔 → (𝑔𝑦 → (𝐹𝑜) ⊆ 𝑦))
3130com12 30 . . . . . . . . . . . 12 (𝑔𝑦 → ((𝐹𝑜) ⊆ 𝑔 → (𝐹𝑜) ⊆ 𝑦))
3231ad2antll 478 . . . . . . . . . . 11 ((𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦)) → ((𝐹𝑜) ⊆ 𝑔 → (𝐹𝑜) ⊆ 𝑦))
3332ad2antlr 476 . . . . . . . . . 10 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → ((𝐹𝑜) ⊆ 𝑔 → (𝐹𝑜) ⊆ 𝑦))
34 ffun 5211 . . . . . . . . . . . . . 14 (𝐹:𝑋𝑌 → Fun 𝐹)
35343ad2ant3 972 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → Fun 𝐹)
3635ad2antrr 475 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → Fun 𝐹)
3736ad2antrr 475 . . . . . . . . . . 11 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → Fun 𝐹)
389eltopss 11958 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑜𝐽) → 𝑜𝑋)
3938adantlr 464 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑜𝐽) → 𝑜𝑋)
402sseq2d 3077 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋𝑌 → (𝑜 ⊆ dom 𝐹𝑜𝑋))
4140ad2antlr 476 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑜𝐽) → (𝑜 ⊆ dom 𝐹𝑜𝑋))
4239, 41mpbird 166 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
43423adantl2 1106 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
4443adantlr 464 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
4544adantlr 464 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
4645adantlr 464 . . . . . . . . . . 11 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
47 funimass3 5468 . . . . . . . . . . 11 ((Fun 𝐹𝑜 ⊆ dom 𝐹) → ((𝐹𝑜) ⊆ 𝑦𝑜 ⊆ (𝐹𝑦)))
4837, 46, 47syl2anc 406 . . . . . . . . . 10 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → ((𝐹𝑜) ⊆ 𝑦𝑜 ⊆ (𝐹𝑦)))
4933, 48sylibd 148 . . . . . . . . 9 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → ((𝐹𝑜) ⊆ 𝑔𝑜 ⊆ (𝐹𝑦)))
5049anim2d 333 . . . . . . . 8 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → ((𝐴𝑜 ∧ (𝐹𝑜) ⊆ 𝑔) → (𝐴𝑜𝑜 ⊆ (𝐹𝑦))))
5150reximdva 2493 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → (∃𝑜𝐽 (𝐴𝑜 ∧ (𝐹𝑜) ⊆ 𝑔) → ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦))))
5229, 51mpd 13 . . . . . 6 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))
538, 52rexlimddv 2513 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))
549isneip 12097 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐴𝑋) → ((𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((𝐹𝑦) ⊆ 𝑋 ∧ ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))))
55543ad2antl1 1111 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → ((𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((𝐹𝑦) ⊆ 𝑋 ∧ ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))))
5655adantr 272 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → ((𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((𝐹𝑦) ⊆ 𝑋 ∧ ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))))
575, 53, 56mpbir2and 896 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → (𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}))
5857exp32 360 . . 3 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → (𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}) → (𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}))))
5958ralrimdv 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 (𝑦 = 𝑜 → (𝐹𝑦) = (𝐹𝑜))
6362eleq1d 2168 . . . . . . . . . . . . . . 15 (𝑦 = 𝑜 → ((𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
6463rspcv 2740 . . . . . . . . . . . . . 14 (𝑜 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
6561, 64syl 14 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑜𝐾 ∧ (𝐹𝐴) ∈ 𝑜) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
66653com23 1155 . . . . . . . . . . . 12 ((𝐾 ∈ Top ∧ (𝐹𝐴) ∈ 𝑜𝑜𝐾) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
67663expb 1150 . . . . . . . . . . 11 ((𝐾 ∈ Top ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
68673ad2antl2 1112 . . . . . . . . . 10 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
6968adantlr 464 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
70 neii2 12100 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})) → ∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜)))
7170ex 114 . . . . . . . . . . 11 (𝐽 ∈ Top → ((𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜))))
72713ad2ant1 970 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → ((𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜))))
7372ad2antrr 475 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → ((𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜))))
74 snssg 3603 . . . . . . . . . . . . 13 (𝐴𝑋 → (𝐴𝑔 ↔ {𝐴} ⊆ 𝑔))
7574ad3antlr 480 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → (𝐴𝑔 ↔ {𝐴} ⊆ 𝑔))
7635ad3antrrr 479 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → Fun 𝐹)
779eltopss 11958 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑔𝐽) → 𝑔𝑋)
78773ad2antl1 1111 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑔𝐽) → 𝑔𝑋)
792sseq2d 3077 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑋𝑌 → (𝑔 ⊆ dom 𝐹𝑔𝑋))
80793ad2ant3 972 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → (𝑔 ⊆ dom 𝐹𝑔𝑋))
8180biimpar 293 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑔𝑋) → 𝑔 ⊆ dom 𝐹)
8278, 81syldan 278 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑔𝐽) → 𝑔 ⊆ dom 𝐹)
8382adantlr 464 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ 𝑔𝐽) → 𝑔 ⊆ dom 𝐹)
8483adantlr 464 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → 𝑔 ⊆ dom 𝐹)
85 funimass3 5468 . . . . . . . . . . . . 13 ((Fun 𝐹𝑔 ⊆ dom 𝐹) → ((𝐹𝑔) ⊆ 𝑜𝑔 ⊆ (𝐹𝑜)))
8676, 84, 85syl2anc 406 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → ((𝐹𝑔) ⊆ 𝑜𝑔 ⊆ (𝐹𝑜)))
8775, 86anbi12d 460 . . . . . . . . . . 11 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → ((𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜) ↔ ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜))))
8887biimprd 157 . . . . . . . . . 10 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → (({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜)) → (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))
8988reximdva 2493 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜)) → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))
9069, 73, 893syld 57 . . . . . . . 8 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))
9190exp32 360 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → ((𝐹𝐴) ∈ 𝑜 → (𝑜𝐾 → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
9291com24 87 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝑜𝐾 → ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
9392imp 123 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → (𝑜𝐾 → ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜))))
9493ralrimiv 2463 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))
95113ad2ant1 970 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴𝑋) → 𝐽 ∈ (TopOn‘𝑋))
96163ad2ant2 971 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴𝑋) → 𝐾 ∈ (TopOn‘𝑌))
97 simp3 951 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴𝑋) → 𝐴𝑋)
98 iscnp 12149 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
9995, 96, 97, 98syl3anc 1184 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
100993expa 1149 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
1011003adantl3 1107 . . . . 5 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
102101adantr 272 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
10360, 94, 102mpbir2and 896 . . 3 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
104103ex 114 . 2 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)))
10559, 104impbid 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)
 Copyright terms: Public domain W3C validator