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

Theorem iscnp4 12462
 Description: The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾 at point 𝑃 " in terms of neighborhoods. (Contributed by FL, 18-Jul-2011.) (Revised by Mario Carneiro, 10-Sep-2015.)
Assertion
Ref Expression
iscnp4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹𝑥) ⊆ 𝑦)))
Distinct variable groups:   𝑥,𝑦,𝐹   𝑥,𝐽,𝑦   𝑥,𝐾,𝑦   𝑥,𝑃,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦

Proof of Theorem iscnp4
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 cnpf2 12451 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋𝑌)
213expa 1182 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋𝑌)
323adantl3 1140 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋𝑌)
4 simpll1 1021 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → 𝐽 ∈ (TopOn‘𝑋))
5 simpll2 1022 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → 𝐾 ∈ (TopOn‘𝑌))
6 simpll3 1023 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → 𝑃𝑋)
7 simplr 520 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃))
8 topontop 12256 . . . . . . . . 9 (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
95, 8syl 14 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → 𝐾 ∈ Top)
10 eqid 2141 . . . . . . . . . 10 𝐾 = 𝐾
1110neii1 12391 . . . . . . . . 9 ((𝐾 ∈ Top ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → 𝑦 𝐾)
129, 11sylancom 417 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → 𝑦 𝐾)
1310ntropn 12361 . . . . . . . 8 ((𝐾 ∈ Top ∧ 𝑦 𝐾) → ((int‘𝐾)‘𝑦) ∈ 𝐾)
149, 12, 13syl2anc 409 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → ((int‘𝐾)‘𝑦) ∈ 𝐾)
15 simpr 109 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)}))
163adantr 274 . . . . . . . . . . . . 13 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → 𝐹:𝑋𝑌)
1716, 6ffvelrnd 5568 . . . . . . . . . . . 12 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → (𝐹𝑃) ∈ 𝑌)
18 toponuni 12257 . . . . . . . . . . . . 13 (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = 𝐾)
195, 18syl 14 . . . . . . . . . . . 12 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → 𝑌 = 𝐾)
2017, 19eleqtrd 2220 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → (𝐹𝑃) ∈ 𝐾)
2120snssd 3675 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → {(𝐹𝑃)} ⊆ 𝐾)
2210neiint 12389 . . . . . . . . . 10 ((𝐾 ∈ Top ∧ {(𝐹𝑃)} ⊆ 𝐾𝑦 𝐾) → (𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)}) ↔ {(𝐹𝑃)} ⊆ ((int‘𝐾)‘𝑦)))
239, 21, 12, 22syl3anc 1217 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → (𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)}) ↔ {(𝐹𝑃)} ⊆ ((int‘𝐾)‘𝑦)))
2415, 23mpbid 146 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → {(𝐹𝑃)} ⊆ ((int‘𝐾)‘𝑦))
25 fvexg 5452 . . . . . . . . . 10 ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝑃𝑋) → (𝐹𝑃) ∈ V)
267, 6, 25syl2anc 409 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → (𝐹𝑃) ∈ V)
27 snssg 3666 . . . . . . . . 9 ((𝐹𝑃) ∈ V → ((𝐹𝑃) ∈ ((int‘𝐾)‘𝑦) ↔ {(𝐹𝑃)} ⊆ ((int‘𝐾)‘𝑦)))
2826, 27syl 14 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → ((𝐹𝑃) ∈ ((int‘𝐾)‘𝑦) ↔ {(𝐹𝑃)} ⊆ ((int‘𝐾)‘𝑦)))
2924, 28mpbird 166 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → (𝐹𝑃) ∈ ((int‘𝐾)‘𝑦))
30 icnpimaex 12455 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ ((int‘𝐾)‘𝑦) ∈ 𝐾 ∧ (𝐹𝑃) ∈ ((int‘𝐾)‘𝑦))) → ∃𝑥𝐽 (𝑃𝑥 ∧ (𝐹𝑥) ⊆ ((int‘𝐾)‘𝑦)))
314, 5, 6, 7, 14, 29, 30syl33anc 1232 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → ∃𝑥𝐽 (𝑃𝑥 ∧ (𝐹𝑥) ⊆ ((int‘𝐾)‘𝑦)))
32 simpl1 985 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐽 ∈ (TopOn‘𝑋))
3332ad2antrr 480 . . . . . . . 8 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) ∧ (𝑥𝐽 ∧ (𝑃𝑥 ∧ (𝐹𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → 𝐽 ∈ (TopOn‘𝑋))
34 topontop 12256 . . . . . . . 8 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
3533, 34syl 14 . . . . . . 7 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) ∧ (𝑥𝐽 ∧ (𝑃𝑥 ∧ (𝐹𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → 𝐽 ∈ Top)
36 simprl 521 . . . . . . 7 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) ∧ (𝑥𝐽 ∧ (𝑃𝑥 ∧ (𝐹𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → 𝑥𝐽)
37 simprrl 529 . . . . . . 7 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) ∧ (𝑥𝐽 ∧ (𝑃𝑥 ∧ (𝐹𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → 𝑃𝑥)
38 opnneip 12403 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝑥𝐽𝑃𝑥) → 𝑥 ∈ ((nei‘𝐽)‘{𝑃}))
3935, 36, 37, 38syl3anc 1217 . . . . . 6 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) ∧ (𝑥𝐽 ∧ (𝑃𝑥 ∧ (𝐹𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → 𝑥 ∈ ((nei‘𝐽)‘{𝑃}))
40 simprrr 530 . . . . . . 7 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) ∧ (𝑥𝐽 ∧ (𝑃𝑥 ∧ (𝐹𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → (𝐹𝑥) ⊆ ((int‘𝐾)‘𝑦))
4110ntrss2 12365 . . . . . . . . 9 ((𝐾 ∈ Top ∧ 𝑦 𝐾) → ((int‘𝐾)‘𝑦) ⊆ 𝑦)
429, 12, 41syl2anc 409 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → ((int‘𝐾)‘𝑦) ⊆ 𝑦)
4342adantr 274 . . . . . . 7 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) ∧ (𝑥𝐽 ∧ (𝑃𝑥 ∧ (𝐹𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → ((int‘𝐾)‘𝑦) ⊆ 𝑦)
4440, 43sstrd 3114 . . . . . 6 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) ∧ (𝑥𝐽 ∧ (𝑃𝑥 ∧ (𝐹𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → (𝐹𝑥) ⊆ 𝑦)
4531, 39, 44reximssdv 2541 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})) → ∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹𝑥) ⊆ 𝑦)
4645ralrimiva 2510 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹𝑥) ⊆ 𝑦)
473, 46jca 304 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹𝑥) ⊆ 𝑦))
4847ex 114 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹𝑥) ⊆ 𝑦)))
49 simpll2 1022 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) → 𝐾 ∈ (TopOn‘𝑌))
5049, 8syl 14 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) → 𝐾 ∈ Top)
51 simprl 521 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) → 𝑦𝐾)
52 simprr 522 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) → (𝐹𝑃) ∈ 𝑦)
53 opnneip 12403 . . . . . . . . . 10 ((𝐾 ∈ Top ∧ 𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦) → 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)}))
5450, 51, 52, 53syl3anc 1217 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) → 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)}))
55 simpl1 985 . . . . . . . . . . . . . 14 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) → 𝐽 ∈ (TopOn‘𝑋))
5655ad2antrr 480 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → 𝐽 ∈ (TopOn‘𝑋))
5756, 34syl 14 . . . . . . . . . . . 12 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → 𝐽 ∈ Top)
58 simprl 521 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → 𝑥 ∈ ((nei‘𝐽)‘{𝑃}))
59 eqid 2141 . . . . . . . . . . . . . 14 𝐽 = 𝐽
6059neii1 12391 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑥 𝐽)
6157, 58, 60syl2anc 409 . . . . . . . . . . . 12 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → 𝑥 𝐽)
6259ntropn 12361 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑥 𝐽) → ((int‘𝐽)‘𝑥) ∈ 𝐽)
6357, 61, 62syl2anc 409 . . . . . . . . . . 11 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → ((int‘𝐽)‘𝑥) ∈ 𝐽)
64 simpll3 1023 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) → 𝑃𝑋)
6564adantr 274 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → 𝑃𝑋)
66 toponuni 12257 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
6756, 66syl 14 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → 𝑋 = 𝐽)
6865, 67eleqtrd 2220 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → 𝑃 𝐽)
6968snssd 3675 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → {𝑃} ⊆ 𝐽)
7059neiint 12389 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ {𝑃} ⊆ 𝐽𝑥 𝐽) → (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ↔ {𝑃} ⊆ ((int‘𝐽)‘𝑥)))
7157, 69, 61, 70syl3anc 1217 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ↔ {𝑃} ⊆ ((int‘𝐽)‘𝑥)))
7258, 71mpbid 146 . . . . . . . . . . . 12 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → {𝑃} ⊆ ((int‘𝐽)‘𝑥))
73 snssg 3666 . . . . . . . . . . . . 13 (𝑃𝑋 → (𝑃 ∈ ((int‘𝐽)‘𝑥) ↔ {𝑃} ⊆ ((int‘𝐽)‘𝑥)))
7465, 73syl 14 . . . . . . . . . . . 12 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → (𝑃 ∈ ((int‘𝐽)‘𝑥) ↔ {𝑃} ⊆ ((int‘𝐽)‘𝑥)))
7572, 74mpbird 166 . . . . . . . . . . 11 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → 𝑃 ∈ ((int‘𝐽)‘𝑥))
7659ntrss2 12365 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑥 𝐽) → ((int‘𝐽)‘𝑥) ⊆ 𝑥)
7757, 61, 76syl2anc 409 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → ((int‘𝐽)‘𝑥) ⊆ 𝑥)
78 imass2 4927 . . . . . . . . . . . . 13 (((int‘𝐽)‘𝑥) ⊆ 𝑥 → (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ (𝐹𝑥))
7977, 78syl 14 . . . . . . . . . . . 12 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ (𝐹𝑥))
80 simprr 522 . . . . . . . . . . . 12 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → (𝐹𝑥) ⊆ 𝑦)
8179, 80sstrd 3114 . . . . . . . . . . 11 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ 𝑦)
82 eleq2 2205 . . . . . . . . . . . . 13 (𝑧 = ((int‘𝐽)‘𝑥) → (𝑃𝑧𝑃 ∈ ((int‘𝐽)‘𝑥)))
83 imaeq2 4889 . . . . . . . . . . . . . 14 (𝑧 = ((int‘𝐽)‘𝑥) → (𝐹𝑧) = (𝐹 “ ((int‘𝐽)‘𝑥)))
8483sseq1d 3133 . . . . . . . . . . . . 13 (𝑧 = ((int‘𝐽)‘𝑥) → ((𝐹𝑧) ⊆ 𝑦 ↔ (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ 𝑦))
8582, 84anbi12d 465 . . . . . . . . . . . 12 (𝑧 = ((int‘𝐽)‘𝑥) → ((𝑃𝑧 ∧ (𝐹𝑧) ⊆ 𝑦) ↔ (𝑃 ∈ ((int‘𝐽)‘𝑥) ∧ (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ 𝑦)))
8685rspcev 2795 . . . . . . . . . . 11 ((((int‘𝐽)‘𝑥) ∈ 𝐽 ∧ (𝑃 ∈ ((int‘𝐽)‘𝑥) ∧ (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ 𝑦)) → ∃𝑧𝐽 (𝑃𝑧 ∧ (𝐹𝑧) ⊆ 𝑦))
8763, 75, 81, 86syl12anc 1215 . . . . . . . . . 10 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹𝑥) ⊆ 𝑦)) → ∃𝑧𝐽 (𝑃𝑧 ∧ (𝐹𝑧) ⊆ 𝑦))
8887rexlimdvaa 2555 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) → (∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹𝑥) ⊆ 𝑦 → ∃𝑧𝐽 (𝑃𝑧 ∧ (𝐹𝑧) ⊆ 𝑦)))
8954, 88embantd 56 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦)) → ((𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)}) → ∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹𝑥) ⊆ 𝑦) → ∃𝑧𝐽 (𝑃𝑧 ∧ (𝐹𝑧) ⊆ 𝑦)))
9089ex 114 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) → ((𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦) → ((𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)}) → ∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹𝑥) ⊆ 𝑦) → ∃𝑧𝐽 (𝑃𝑧 ∧ (𝐹𝑧) ⊆ 𝑦))))
9190com23 78 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) → ((𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)}) → ∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹𝑥) ⊆ 𝑦) → ((𝑦𝐾 ∧ (𝐹𝑃) ∈ 𝑦) → ∃𝑧𝐽 (𝑃𝑧 ∧ (𝐹𝑧) ⊆ 𝑦))))
9291exp4a 364 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) → ((𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)}) → ∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹𝑥) ⊆ 𝑦) → (𝑦𝐾 → ((𝐹𝑃) ∈ 𝑦 → ∃𝑧𝐽 (𝑃𝑧 ∧ (𝐹𝑧) ⊆ 𝑦)))))
9392ralimdv2 2507 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) ∧ 𝐹:𝑋𝑌) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹𝑥) ⊆ 𝑦 → ∀𝑦𝐾 ((𝐹𝑃) ∈ 𝑦 → ∃𝑧𝐽 (𝑃𝑧 ∧ (𝐹𝑧) ⊆ 𝑦))))
9493imdistanda 445 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) → ((𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹𝑥) ⊆ 𝑦) → (𝐹:𝑋𝑌 ∧ ∀𝑦𝐾 ((𝐹𝑃) ∈ 𝑦 → ∃𝑧𝐽 (𝑃𝑧 ∧ (𝐹𝑧) ⊆ 𝑦)))))
95 iscnp 12443 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦𝐾 ((𝐹𝑃) ∈ 𝑦 → ∃𝑧𝐽 (𝑃𝑧 ∧ (𝐹𝑧) ⊆ 𝑦)))))
9694, 95sylibrd 168 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) → ((𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹𝑥) ⊆ 𝑦) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)))
9748, 96impbid 128 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹𝑥) ⊆ 𝑦)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 963   = wceq 1332   ∈ wcel 1481  ∀wral 2418  ∃wrex 2419  Vcvv 2691   ⊆ wss 3078  {csn 3534  ∪ cuni 3746   “ cima 4554  ⟶wf 5131  ‘cfv 5135  (class class class)co 5786  Topctop 12239  TopOnctopon 12252  intcnt 12337  neicnei 12382   CnP ccnp 12430 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 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2123  ax-coll 4053  ax-sep 4056  ax-pow 4108  ax-pr 4142  ax-un 4366  ax-setind 4463 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1738  df-eu 2004  df-mo 2005  df-clab 2128  df-cleq 2134  df-clel 2137  df-nfc 2272  df-ne 2311  df-ral 2423  df-rex 2424  df-reu 2425  df-rab 2427  df-v 2693  df-sbc 2916  df-csb 3010  df-dif 3080  df-un 3082  df-in 3084  df-ss 3091  df-pw 3519  df-sn 3540  df-pr 3541  df-op 3543  df-uni 3747  df-iun 3825  df-br 3940  df-opab 4000  df-mpt 4001  df-id 4226  df-xp 4557  df-rel 4558  df-cnv 4559  df-co 4560  df-dm 4561  df-rn 4562  df-res 4563  df-ima 4564  df-iota 5100  df-fun 5137  df-fn 5138  df-f 5139  df-f1 5140  df-fo 5141  df-f1o 5142  df-fv 5143  df-ov 5789  df-oprab 5790  df-mpo 5791  df-1st 6050  df-2nd 6051  df-map 6556  df-top 12240  df-topon 12253  df-ntr 12340  df-nei 12383  df-cnp 12433 This theorem is referenced by:  cnnei  12476
 Copyright terms: Public domain W3C validator