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

Theorem 1stccnp 21184
 Description: A mapping is continuous at 𝑃 in a first-countable space 𝑋 iff it is sequentially continuous at 𝑃, meaning that the image under 𝐹 of every sequence converging at 𝑃 converges to 𝐹(𝑃). This proof uses ax-cc 9208, but only via 1stcelcls 21183, so it could be refactored into a proof that continuity and sequential continuity are the same in sequential spaces. (Contributed by Mario Carneiro, 7-Sep-2015.)
Hypotheses
Ref Expression
1stccnp.1 (𝜑𝐽 ∈ 1st𝜔)
1stccnp.2 (𝜑𝐽 ∈ (TopOn‘𝑋))
1stccnp.3 (𝜑𝐾 ∈ (TopOn‘𝑌))
1stccnp.4 (𝜑𝑃𝑋)
Assertion
Ref Expression
1stccnp (𝜑 → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))))
Distinct variable groups:   𝑓,𝐹   𝑓,𝐽   𝜑,𝑓   𝑓,𝐾   𝑓,𝑋   𝑓,𝑌   𝑃,𝑓

Proof of Theorem 1stccnp
Dummy variables 𝑗 𝑘 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1stccnp.2 . . . . 5 (𝜑𝐽 ∈ (TopOn‘𝑋))
2 1stccnp.3 . . . . 5 (𝜑𝐾 ∈ (TopOn‘𝑌))
31, 2jca 554 . . . 4 (𝜑 → (𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)))
4 cnpf2 20973 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋𝑌)
543expa 1262 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋𝑌)
63, 5sylan 488 . . 3 ((𝜑𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋𝑌)
7 simprr 795 . . . . . 6 (((𝜑𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ (𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃)) → 𝑓(⇝𝑡𝐽)𝑃)
8 simplr 791 . . . . . 6 (((𝜑𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ (𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃))
97, 8lmcnp 21027 . . . . 5 (((𝜑𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ (𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃)) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))
109ex 450 . . . 4 ((𝜑𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))
1110alrimiv 1852 . . 3 ((𝜑𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))
126, 11jca 554 . 2 ((𝜑𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))))
13 simprl 793 . . 3 ((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) → 𝐹:𝑋𝑌)
14 fal 1487 . . . . . . . . 9 ¬ ⊥
15 19.29 1798 . . . . . . . . . . . . . 14 ((∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)) ∧ ∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃)) → ∃𝑓(((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃)))
16 simprl 793 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃)) → 𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)))
17 difss 3720 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 ∖ (𝐹𝑢)) ⊆ 𝑋
18 fss 6018 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ (𝑋 ∖ (𝐹𝑢)) ⊆ 𝑋) → 𝑓:ℕ⟶𝑋)
1916, 17, 18sylancl 693 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃)) → 𝑓:ℕ⟶𝑋)
20 simprr 795 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃)) → 𝑓(⇝𝑡𝐽)𝑃)
2119, 20jca 554 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃)) → (𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃))
22 nnuz 11674 . . . . . . . . . . . . . . . . . . . . . 22 ℕ = (ℤ‘1)
23 simplrr 800 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) → (𝐹𝑃) ∈ 𝑢)
24 1zzd 11359 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) → 1 ∈ ℤ)
25 simprr 795 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))
26 simplrl 799 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) → 𝑢𝐾)
2722, 23, 24, 25, 26lmcvg 20985 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑓)‘𝑘) ∈ 𝑢)
2822r19.2uz 14032 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑓)‘𝑘) ∈ 𝑢 → ∃𝑘 ∈ ℕ ((𝐹𝑓)‘𝑘) ∈ 𝑢)
29 simprll 801 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) → 𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)))
30 ffn 6007 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) → 𝑓 Fn ℕ)
3129, 30syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) → 𝑓 Fn ℕ)
32 fvco2 6235 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 Fn ℕ ∧ 𝑘 ∈ ℕ) → ((𝐹𝑓)‘𝑘) = (𝐹‘(𝑓𝑘)))
3331, 32sylan 488 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) ∧ 𝑘 ∈ ℕ) → ((𝐹𝑓)‘𝑘) = (𝐹‘(𝑓𝑘)))
3433eleq1d 2683 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) ∧ 𝑘 ∈ ℕ) → (((𝐹𝑓)‘𝑘) ∈ 𝑢 ↔ (𝐹‘(𝑓𝑘)) ∈ 𝑢))
3529ffvelrnda 6320 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) ∧ 𝑘 ∈ ℕ) → (𝑓𝑘) ∈ (𝑋 ∖ (𝐹𝑢)))
3635eldifad 3571 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) ∧ 𝑘 ∈ ℕ) → (𝑓𝑘) ∈ 𝑋)
37 simplr 791 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → 𝐹:𝑋𝑌)
3837ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) ∧ 𝑘 ∈ ℕ) → 𝐹:𝑋𝑌)
39 ffn 6007 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹:𝑋𝑌𝐹 Fn 𝑋)
40 elpreima 6298 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 Fn 𝑋 → ((𝑓𝑘) ∈ (𝐹𝑢) ↔ ((𝑓𝑘) ∈ 𝑋 ∧ (𝐹‘(𝑓𝑘)) ∈ 𝑢)))
4138, 39, 403syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) ∧ 𝑘 ∈ ℕ) → ((𝑓𝑘) ∈ (𝐹𝑢) ↔ ((𝑓𝑘) ∈ 𝑋 ∧ (𝐹‘(𝑓𝑘)) ∈ 𝑢)))
4235eldifbd 3572 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) ∧ 𝑘 ∈ ℕ) → ¬ (𝑓𝑘) ∈ (𝐹𝑢))
4342pm2.21d 118 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) ∧ 𝑘 ∈ ℕ) → ((𝑓𝑘) ∈ (𝐹𝑢) → ⊥))
4441, 43sylbird 250 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) ∧ 𝑘 ∈ ℕ) → (((𝑓𝑘) ∈ 𝑋 ∧ (𝐹‘(𝑓𝑘)) ∈ 𝑢) → ⊥))
4536, 44mpand 710 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) ∧ 𝑘 ∈ ℕ) → ((𝐹‘(𝑓𝑘)) ∈ 𝑢 → ⊥))
4634, 45sylbid 230 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) ∧ 𝑘 ∈ ℕ) → (((𝐹𝑓)‘𝑘) ∈ 𝑢 → ⊥))
4746rexlimdva 3025 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) → (∃𝑘 ∈ ℕ ((𝐹𝑓)‘𝑘) ∈ 𝑢 → ⊥))
4828, 47syl5 34 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑓)‘𝑘) ∈ 𝑢 → ⊥))
4927, 48mpd 15 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) ∧ (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃))) → ⊥)
5049expr 642 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃)) → ((𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃) → ⊥))
5121, 50embantd 59 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃)) → (((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)) → ⊥))
5251ex 450 . . . . . . . . . . . . . . . . 17 (((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) → (((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)) → ⊥)))
5352com23 86 . . . . . . . . . . . . . . . 16 (((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → (((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)) → ((𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) → ⊥)))
5453impd 447 . . . . . . . . . . . . . . 15 (((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → ((((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃)) → ⊥))
5554exlimdv 1858 . . . . . . . . . . . . . 14 (((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → (∃𝑓(((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃)) → ⊥))
5615, 55syl5 34 . . . . . . . . . . . . 13 (((𝜑𝐹:𝑋𝑌) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → ((∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)) ∧ ∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃)) → ⊥))
5756exp4b 631 . . . . . . . . . . . 12 ((𝜑𝐹:𝑋𝑌) → ((𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢) → (∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)) → (∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) → ⊥))))
5857com23 86 . . . . . . . . . . 11 ((𝜑𝐹:𝑋𝑌) → (∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)) → ((𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢) → (∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) → ⊥))))
5958impr 648 . . . . . . . . . 10 ((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) → ((𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢) → (∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) → ⊥)))
6059imp 445 . . . . . . . . 9 (((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → (∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃) → ⊥))
6114, 60mtoi 190 . . . . . . . 8 (((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → ¬ ∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃))
62 1stccnp.1 . . . . . . . . . 10 (𝜑𝐽 ∈ 1st𝜔)
6362ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → 𝐽 ∈ 1st𝜔)
641ad2antrr 761 . . . . . . . . . . 11 (((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → 𝐽 ∈ (TopOn‘𝑋))
65 toponuni 20647 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
6664, 65syl 17 . . . . . . . . . 10 (((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → 𝑋 = 𝐽)
6717, 66syl5sseq 3637 . . . . . . . . 9 (((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → (𝑋 ∖ (𝐹𝑢)) ⊆ 𝐽)
68 eqid 2621 . . . . . . . . . 10 𝐽 = 𝐽
69681stcelcls 21183 . . . . . . . . 9 ((𝐽 ∈ 1st𝜔 ∧ (𝑋 ∖ (𝐹𝑢)) ⊆ 𝐽) → (𝑃 ∈ ((cls‘𝐽)‘(𝑋 ∖ (𝐹𝑢))) ↔ ∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃)))
7063, 67, 69syl2anc 692 . . . . . . . 8 (((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → (𝑃 ∈ ((cls‘𝐽)‘(𝑋 ∖ (𝐹𝑢))) ↔ ∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (𝐹𝑢)) ∧ 𝑓(⇝𝑡𝐽)𝑃)))
7161, 70mtbird 315 . . . . . . 7 (((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → ¬ 𝑃 ∈ ((cls‘𝐽)‘(𝑋 ∖ (𝐹𝑢))))
72 topontop 20646 . . . . . . . . 9 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
7364, 72syl 17 . . . . . . . 8 (((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → 𝐽 ∈ Top)
74 1stccnp.4 . . . . . . . . . 10 (𝜑𝑃𝑋)
7574ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → 𝑃𝑋)
7675, 66eleqtrd 2700 . . . . . . . 8 (((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → 𝑃 𝐽)
7768elcls 20796 . . . . . . . 8 ((𝐽 ∈ Top ∧ (𝑋 ∖ (𝐹𝑢)) ⊆ 𝐽𝑃 𝐽) → (𝑃 ∈ ((cls‘𝐽)‘(𝑋 ∖ (𝐹𝑢))) ↔ ∀𝑣𝐽 (𝑃𝑣 → (𝑣 ∩ (𝑋 ∖ (𝐹𝑢))) ≠ ∅)))
7873, 67, 76, 77syl3anc 1323 . . . . . . 7 (((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → (𝑃 ∈ ((cls‘𝐽)‘(𝑋 ∖ (𝐹𝑢))) ↔ ∀𝑣𝐽 (𝑃𝑣 → (𝑣 ∩ (𝑋 ∖ (𝐹𝑢))) ≠ ∅)))
7971, 78mtbid 314 . . . . . 6 (((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → ¬ ∀𝑣𝐽 (𝑃𝑣 → (𝑣 ∩ (𝑋 ∖ (𝐹𝑢))) ≠ ∅))
8013ad2antrr 761 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ 𝑣𝐽) → 𝐹:𝑋𝑌)
81 ffun 6010 . . . . . . . . . . . . 13 (𝐹:𝑋𝑌 → Fun 𝐹)
8280, 81syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ 𝑣𝐽) → Fun 𝐹)
83 toponss 20649 . . . . . . . . . . . . . 14 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑣𝐽) → 𝑣𝑋)
8464, 83sylan 488 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ 𝑣𝐽) → 𝑣𝑋)
85 fdm 6013 . . . . . . . . . . . . . 14 (𝐹:𝑋𝑌 → dom 𝐹 = 𝑋)
8680, 85syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ 𝑣𝐽) → dom 𝐹 = 𝑋)
8784, 86sseqtr4d 3626 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ 𝑣𝐽) → 𝑣 ⊆ dom 𝐹)
88 funimass3 6294 . . . . . . . . . . . 12 ((Fun 𝐹𝑣 ⊆ dom 𝐹) → ((𝐹𝑣) ⊆ 𝑢𝑣 ⊆ (𝐹𝑢)))
8982, 87, 88syl2anc 692 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ 𝑣𝐽) → ((𝐹𝑣) ⊆ 𝑢𝑣 ⊆ (𝐹𝑢)))
90 df-ss 3573 . . . . . . . . . . . . 13 (𝑣𝑋 ↔ (𝑣𝑋) = 𝑣)
9184, 90sylib 208 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ 𝑣𝐽) → (𝑣𝑋) = 𝑣)
9291sseq1d 3616 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ 𝑣𝐽) → ((𝑣𝑋) ⊆ (𝐹𝑢) ↔ 𝑣 ⊆ (𝐹𝑢)))
9389, 92bitr4d 271 . . . . . . . . . 10 ((((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ 𝑣𝐽) → ((𝐹𝑣) ⊆ 𝑢 ↔ (𝑣𝑋) ⊆ (𝐹𝑢)))
94 nne 2794 . . . . . . . . . . 11 (¬ (𝑣 ∩ (𝑋 ∖ (𝐹𝑢))) ≠ ∅ ↔ (𝑣 ∩ (𝑋 ∖ (𝐹𝑢))) = ∅)
95 inssdif0 3926 . . . . . . . . . . 11 ((𝑣𝑋) ⊆ (𝐹𝑢) ↔ (𝑣 ∩ (𝑋 ∖ (𝐹𝑢))) = ∅)
9694, 95bitr4i 267 . . . . . . . . . 10 (¬ (𝑣 ∩ (𝑋 ∖ (𝐹𝑢))) ≠ ∅ ↔ (𝑣𝑋) ⊆ (𝐹𝑢))
9793, 96syl6bbr 278 . . . . . . . . 9 ((((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ 𝑣𝐽) → ((𝐹𝑣) ⊆ 𝑢 ↔ ¬ (𝑣 ∩ (𝑋 ∖ (𝐹𝑢))) ≠ ∅))
9897anbi2d 739 . . . . . . . 8 ((((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) ∧ 𝑣𝐽) → ((𝑃𝑣 ∧ (𝐹𝑣) ⊆ 𝑢) ↔ (𝑃𝑣 ∧ ¬ (𝑣 ∩ (𝑋 ∖ (𝐹𝑢))) ≠ ∅)))
9998rexbidva 3043 . . . . . . 7 (((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → (∃𝑣𝐽 (𝑃𝑣 ∧ (𝐹𝑣) ⊆ 𝑢) ↔ ∃𝑣𝐽 (𝑃𝑣 ∧ ¬ (𝑣 ∩ (𝑋 ∖ (𝐹𝑢))) ≠ ∅)))
100 rexanali 2993 . . . . . . 7 (∃𝑣𝐽 (𝑃𝑣 ∧ ¬ (𝑣 ∩ (𝑋 ∖ (𝐹𝑢))) ≠ ∅) ↔ ¬ ∀𝑣𝐽 (𝑃𝑣 → (𝑣 ∩ (𝑋 ∖ (𝐹𝑢))) ≠ ∅))
10199, 100syl6bb 276 . . . . . 6 (((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → (∃𝑣𝐽 (𝑃𝑣 ∧ (𝐹𝑣) ⊆ 𝑢) ↔ ¬ ∀𝑣𝐽 (𝑃𝑣 → (𝑣 ∩ (𝑋 ∖ (𝐹𝑢))) ≠ ∅)))
10279, 101mpbird 247 . . . . 5 (((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ (𝑢𝐾 ∧ (𝐹𝑃) ∈ 𝑢)) → ∃𝑣𝐽 (𝑃𝑣 ∧ (𝐹𝑣) ⊆ 𝑢))
103102expr 642 . . . 4 (((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) ∧ 𝑢𝐾) → ((𝐹𝑃) ∈ 𝑢 → ∃𝑣𝐽 (𝑃𝑣 ∧ (𝐹𝑣) ⊆ 𝑢)))
104103ralrimiva 2961 . . 3 ((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) → ∀𝑢𝐾 ((𝐹𝑃) ∈ 𝑢 → ∃𝑣𝐽 (𝑃𝑣 ∧ (𝐹𝑣) ⊆ 𝑢)))
105 iscnp 20960 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑢𝐾 ((𝐹𝑃) ∈ 𝑢 → ∃𝑣𝐽 (𝑃𝑣 ∧ (𝐹𝑣) ⊆ 𝑢)))))
1061, 2, 74, 105syl3anc 1323 . . . 4 (𝜑 → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑢𝐾 ((𝐹𝑃) ∈ 𝑢 → ∃𝑣𝐽 (𝑃𝑣 ∧ (𝐹𝑣) ⊆ 𝑢)))))
107106adantr 481 . . 3 ((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑢𝐾 ((𝐹𝑃) ∈ 𝑢 → ∃𝑣𝐽 (𝑃𝑣 ∧ (𝐹𝑣) ⊆ 𝑢)))))
10813, 104, 107mpbir2and 956 . 2 ((𝜑 ∧ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃))
10912, 108impbida 876 1 (𝜑 → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋𝑓(⇝𝑡𝐽)𝑃) → (𝐹𝑓)(⇝𝑡𝐾)(𝐹𝑃)))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1478   = wceq 1480  ⊥wfal 1485  ∃wex 1701   ∈ wcel 1987   ≠ wne 2790  ∀wral 2907  ∃wrex 2908   ∖ cdif 3556   ∩ cin 3558   ⊆ wss 3559  ∅c0 3896  ∪ cuni 4407   class class class wbr 4618  ◡ccnv 5078  dom cdm 5079   “ cima 5082   ∘ ccom 5083  Fun wfun 5846   Fn wfn 5847  ⟶wf 5848  ‘cfv 5852  (class class class)co 6610  1c1 9888  ℕcn 10971  ℤ≥cuz 11638  Topctop 20626  TopOnctopon 20643  clsccl 20741   CnP ccnp 20948  ⇝𝑡clm 20949  1st𝜔c1stc 21159 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8489  ax-cc 9208  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-nn 10972  df-n0 11244  df-z 11329  df-uz 11639  df-fz 12276  df-top 20627  df-topon 20644  df-cld 20742  df-ntr 20743  df-cls 20744  df-cnp 20951  df-lm 20952  df-1stc 21161 This theorem is referenced by:  1stccn  21185  metcnp4  23027
 Copyright terms: Public domain W3C validator