Theorem 1stccnp 21265

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 9257, but only via 1stcelcls 21264, 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.

Step	Hyp	Ref	Expression
1		1stccnp.2	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
2		1stccnp.3	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))
3	1, 2	jca 554	. . . 4 ⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)))
4		cnpf2 21054	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋⟶𝑌)
5	4	3expa 1265	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋⟶𝑌)
6	3, 5	sylan 488	. . 3 ⊢ ((𝜑 ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋⟶𝑌)
7		simprr 796	. . . . . 6 ⊢ (((𝜑 ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ (𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑓(⇝𝑡‘𝐽)𝑃)
8		simplr 792	. . . . . 6 ⊢ (((𝜑 ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ (𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃))
9	7, 8	lmcnp 21108	. . . . 5 ⊢ (((𝜑 ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ (𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))
10	9	ex 450	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))
11	10	alrimiv 1855	. . 3 ⊢ ((𝜑 ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))
12	6, 11	jca 554	. 2 ⊢ ((𝜑 ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))))
13		simprl 794	. . 3 ⊢ ((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) → 𝐹:𝑋⟶𝑌)
14		fal 1490	. . . . . . . . 9 ⊢ ¬ ⊥
15		19.29 1801	. . . . . . . . . . . . . 14 ⊢ ((∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)) ∧ ∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → ∃𝑓(((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
16		simprl 794	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)))
17		difss 3737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 ∖ (◡𝐹 “ 𝑢)) ⊆ 𝑋
18		fss 6056	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ (𝑋 ∖ (◡𝐹 “ 𝑢)) ⊆ 𝑋) → 𝑓:ℕ⟶𝑋)
19	16, 17, 18	sylancl 694	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑓:ℕ⟶𝑋)
20		simprr 796	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → 𝑓(⇝𝑡‘𝐽)𝑃)
21	19, 20	jca 554	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → (𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃))
22		nnuz 11723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ = (ℤ≥‘1)
23		simplrr 801	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) → (𝐹‘𝑃) ∈ 𝑢)
24		1zzd 11408	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) → 1 ∈ ℤ)
25		simprr 796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))
26		simplrl 800	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) → 𝑢 ∈ 𝐾)
27	22, 23, 24, 25, 26	lmcvg 21066	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝑢)
28	22	r19.2uz 14091	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝑢 → ∃𝑘 ∈ ℕ ((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝑢)
29		simprll 802	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) → 𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)))
30		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) → 𝑓 Fn ℕ)
31	29, 30	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) → 𝑓 Fn ℕ)
32		fvco2 6273	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓 Fn ℕ ∧ 𝑘 ∈ ℕ) → ((𝐹 ∘ 𝑓)‘𝑘) = (𝐹‘(𝑓‘𝑘)))
33	31, 32	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) ∧ 𝑘 ∈ ℕ) → ((𝐹 ∘ 𝑓)‘𝑘) = (𝐹‘(𝑓‘𝑘)))
34	33	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) ∧ 𝑘 ∈ ℕ) → (((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝑢 ↔ (𝐹‘(𝑓‘𝑘)) ∈ 𝑢))
35	29	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ (𝑋 ∖ (◡𝐹 “ 𝑢)))
36	35	eldifad 3586	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ 𝑋)
37		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → 𝐹:𝑋⟶𝑌)
38	37	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) ∧ 𝑘 ∈ ℕ) → 𝐹:𝑋⟶𝑌)
39		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹:𝑋⟶𝑌 → 𝐹 Fn 𝑋)
40		elpreima 6337	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹 Fn 𝑋 → ((𝑓‘𝑘) ∈ (◡𝐹 “ 𝑢) ↔ ((𝑓‘𝑘) ∈ 𝑋 ∧ (𝐹‘(𝑓‘𝑘)) ∈ 𝑢)))
41	38, 39, 40	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) ∧ 𝑘 ∈ ℕ) → ((𝑓‘𝑘) ∈ (◡𝐹 “ 𝑢) ↔ ((𝑓‘𝑘) ∈ 𝑋 ∧ (𝐹‘(𝑓‘𝑘)) ∈ 𝑢)))
42	35	eldifbd 3587	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) ∧ 𝑘 ∈ ℕ) → ¬ (𝑓‘𝑘) ∈ (◡𝐹 “ 𝑢))
43	42	pm2.21d 118	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) ∧ 𝑘 ∈ ℕ) → ((𝑓‘𝑘) ∈ (◡𝐹 “ 𝑢) → ⊥))
44	41, 43	sylbird 250	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) ∧ 𝑘 ∈ ℕ) → (((𝑓‘𝑘) ∈ 𝑋 ∧ (𝐹‘(𝑓‘𝑘)) ∈ 𝑢) → ⊥))
45	36, 44	mpand 711	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) ∧ 𝑘 ∈ ℕ) → ((𝐹‘(𝑓‘𝑘)) ∈ 𝑢 → ⊥))
46	34, 45	sylbid 230	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) ∧ 𝑘 ∈ ℕ) → (((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝑢 → ⊥))
47	46	rexlimdva 3031	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) → (∃𝑘 ∈ ℕ ((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝑢 → ⊥))
48	28, 47	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹 ∘ 𝑓)‘𝑘) ∈ 𝑢 → ⊥))
49	27, 48	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) ∧ (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))) → ⊥)
50	49	expr 643	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → ((𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃) → ⊥))
51	21, 50	embantd 59	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → (((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)) → ⊥))
52	51	ex 450	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)) → ⊥)))
53	52	com23 86	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → (((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)) → ((𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → ⊥)))
54	53	impd 447	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → ((((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → ⊥))
55	54	exlimdv 1861	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → (∃𝑓(((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)) ∧ (𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → ⊥))
56	15, 55	syl5 34	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → ((∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)) ∧ ∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃)) → ⊥))
57	56	exp4b 632	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → ((𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢) → (∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)) → (∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → ⊥))))
58	57	com23 86	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)) → ((𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢) → (∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → ⊥))))
59	58	impr 649	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) → ((𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢) → (∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → ⊥)))
60	59	imp 445	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → (∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → ⊥))
61	14, 60	mtoi 190	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → ¬ ∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃))
62		1stccnp.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ 1st𝜔)
63	62	ad2antrr 762	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → 𝐽 ∈ 1st𝜔)
64	1	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → 𝐽 ∈ (TopOn‘𝑋))
65		toponuni 20719	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
66	64, 65	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → 𝑋 = ∪ 𝐽)
67	17, 66	syl5sseq 3653	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → (𝑋 ∖ (◡𝐹 “ 𝑢)) ⊆ ∪ 𝐽)
68		eqid 2622	. . . . . . . . . 10 ⊢ ∪ 𝐽 = ∪ 𝐽
69	68	1stcelcls 21264	. . . . . . . . 9 ⊢ ((𝐽 ∈ 1st𝜔 ∧ (𝑋 ∖ (◡𝐹 “ 𝑢)) ⊆ ∪ 𝐽) → (𝑃 ∈ ((cls‘𝐽)‘(𝑋 ∖ (◡𝐹 “ 𝑢))) ↔ ∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
70	63, 67, 69	syl2anc 693	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → (𝑃 ∈ ((cls‘𝐽)‘(𝑋 ∖ (◡𝐹 “ 𝑢))) ↔ ∃𝑓(𝑓:ℕ⟶(𝑋 ∖ (◡𝐹 “ 𝑢)) ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
71	61, 70	mtbird 315	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → ¬ 𝑃 ∈ ((cls‘𝐽)‘(𝑋 ∖ (◡𝐹 “ 𝑢))))
72		topontop 20718	. . . . . . . . 9 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
73	64, 72	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → 𝐽 ∈ Top)
74		1stccnp.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ 𝑋)
75	74	ad2antrr 762	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → 𝑃 ∈ 𝑋)
76	75, 66	eleqtrd 2703	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → 𝑃 ∈ ∪ 𝐽)
77	68	elcls 20877	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ (𝑋 ∖ (◡𝐹 “ 𝑢)) ⊆ ∪ 𝐽 ∧ 𝑃 ∈ ∪ 𝐽) → (𝑃 ∈ ((cls‘𝐽)‘(𝑋 ∖ (◡𝐹 “ 𝑢))) ↔ ∀𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 → (𝑣 ∩ (𝑋 ∖ (◡𝐹 “ 𝑢))) ≠ ∅)))
78	73, 67, 76, 77	syl3anc 1326	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → (𝑃 ∈ ((cls‘𝐽)‘(𝑋 ∖ (◡𝐹 “ 𝑢))) ↔ ∀𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 → (𝑣 ∩ (𝑋 ∖ (◡𝐹 “ 𝑢))) ≠ ∅)))
79	71, 78	mtbid 314	. . . . . 6 ⊢ (((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → ¬ ∀𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 → (𝑣 ∩ (𝑋 ∖ (◡𝐹 “ 𝑢))) ≠ ∅))
80	13	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ 𝑣 ∈ 𝐽) → 𝐹:𝑋⟶𝑌)
81		ffun 6048	. . . . . . . . . . . . 13 ⊢ (𝐹:𝑋⟶𝑌 → Fun 𝐹)
82	80, 81	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ 𝑣 ∈ 𝐽) → Fun 𝐹)
83		toponss 20731	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑣 ∈ 𝐽) → 𝑣 ⊆ 𝑋)
84	64, 83	sylan 488	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ 𝑣 ∈ 𝐽) → 𝑣 ⊆ 𝑋)
85		fdm 6051	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝑋⟶𝑌 → dom 𝐹 = 𝑋)
86	80, 85	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ 𝑣 ∈ 𝐽) → dom 𝐹 = 𝑋)
87	84, 86	sseqtr4d 3642	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ 𝑣 ∈ 𝐽) → 𝑣 ⊆ dom 𝐹)
88		funimass3 6333	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ 𝑣 ⊆ dom 𝐹) → ((𝐹 “ 𝑣) ⊆ 𝑢 ↔ 𝑣 ⊆ (◡𝐹 “ 𝑢)))
89	82, 87, 88	syl2anc 693	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ 𝑣 ∈ 𝐽) → ((𝐹 “ 𝑣) ⊆ 𝑢 ↔ 𝑣 ⊆ (◡𝐹 “ 𝑢)))
90		df-ss 3588	. . . . . . . . . . . . 13 ⊢ (𝑣 ⊆ 𝑋 ↔ (𝑣 ∩ 𝑋) = 𝑣)
91	84, 90	sylib 208	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ 𝑣 ∈ 𝐽) → (𝑣 ∩ 𝑋) = 𝑣)
92	91	sseq1d 3632	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ 𝑣 ∈ 𝐽) → ((𝑣 ∩ 𝑋) ⊆ (◡𝐹 “ 𝑢) ↔ 𝑣 ⊆ (◡𝐹 “ 𝑢)))
93	89, 92	bitr4d 271	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ 𝑣 ∈ 𝐽) → ((𝐹 “ 𝑣) ⊆ 𝑢 ↔ (𝑣 ∩ 𝑋) ⊆ (◡𝐹 “ 𝑢)))
94		nne 2798	. . . . . . . . . . 11 ⊢ (¬ (𝑣 ∩ (𝑋 ∖ (◡𝐹 “ 𝑢))) ≠ ∅ ↔ (𝑣 ∩ (𝑋 ∖ (◡𝐹 “ 𝑢))) = ∅)
95		inssdif0 3947	. . . . . . . . . . 11 ⊢ ((𝑣 ∩ 𝑋) ⊆ (◡𝐹 “ 𝑢) ↔ (𝑣 ∩ (𝑋 ∖ (◡𝐹 “ 𝑢))) = ∅)
96	94, 95	bitr4i 267	. . . . . . . . . 10 ⊢ (¬ (𝑣 ∩ (𝑋 ∖ (◡𝐹 “ 𝑢))) ≠ ∅ ↔ (𝑣 ∩ 𝑋) ⊆ (◡𝐹 “ 𝑢))
97	93, 96	syl6bbr 278	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ 𝑣 ∈ 𝐽) → ((𝐹 “ 𝑣) ⊆ 𝑢 ↔ ¬ (𝑣 ∩ (𝑋 ∖ (◡𝐹 “ 𝑢))) ≠ ∅))
98	97	anbi2d 740	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) ∧ 𝑣 ∈ 𝐽) → ((𝑃 ∈ 𝑣 ∧ (𝐹 “ 𝑣) ⊆ 𝑢) ↔ (𝑃 ∈ 𝑣 ∧ ¬ (𝑣 ∩ (𝑋 ∖ (◡𝐹 “ 𝑢))) ≠ ∅)))
99	98	rexbidva 3049	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → (∃𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 ∧ (𝐹 “ 𝑣) ⊆ 𝑢) ↔ ∃𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 ∧ ¬ (𝑣 ∩ (𝑋 ∖ (◡𝐹 “ 𝑢))) ≠ ∅)))
100		rexanali 2998	. . . . . . 7 ⊢ (∃𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 ∧ ¬ (𝑣 ∩ (𝑋 ∖ (◡𝐹 “ 𝑢))) ≠ ∅) ↔ ¬ ∀𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 → (𝑣 ∩ (𝑋 ∖ (◡𝐹 “ 𝑢))) ≠ ∅))
101	99, 100	syl6bb 276	. . . . . 6 ⊢ (((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → (∃𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 ∧ (𝐹 “ 𝑣) ⊆ 𝑢) ↔ ¬ ∀𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 → (𝑣 ∩ (𝑋 ∖ (◡𝐹 “ 𝑢))) ≠ ∅)))
102	79, 101	mpbird 247	. . . . 5 ⊢ (((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ (𝑢 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑢)) → ∃𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 ∧ (𝐹 “ 𝑣) ⊆ 𝑢))
103	102	expr 643	. . . 4 ⊢ (((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) ∧ 𝑢 ∈ 𝐾) → ((𝐹‘𝑃) ∈ 𝑢 → ∃𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 ∧ (𝐹 “ 𝑣) ⊆ 𝑢)))
104	103	ralrimiva 2966	. . 3 ⊢ ((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) → ∀𝑢 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑢 → ∃𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 ∧ (𝐹 “ 𝑣) ⊆ 𝑢)))
105		iscnp 21041	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑢 → ∃𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 ∧ (𝐹 “ 𝑣) ⊆ 𝑢)))))
106	1, 2, 74, 105	syl3anc 1326	. . . 4 ⊢ (𝜑 → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑢 → ∃𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 ∧ (𝐹 “ 𝑣) ⊆ 𝑢)))))
107	106	adantr 481	. . 3 ⊢ ((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑢 → ∃𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 ∧ (𝐹 “ 𝑣) ⊆ 𝑢)))))
108	13, 104, 107	mpbir2and 957	. 2 ⊢ ((𝜑 ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃))
109	12, 108	impbida 877	1 ⊢ (𝜑 → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1481   = wceq 1483  ⊥wfal 1488  ∃wex 1704   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  ∃wrex 2913   ∖ cdif 3571   ∩ cin 3573   ⊆ wss 3574  ∅c0 3915  ∪ cuni 4436   class class class wbr 4653  ^◡ccnv 5113  dom cdm 5114   “ cima 5117   ∘ ccom 5118  Fun wfun 5882   Fn wfn 5883  ⟶wf 5884  ‘cfv 5888  (class class class)co 6650  1c1 9937  ℕcn 11020  ℤ_≥cuz 11687  Topctop 20698  TopOnctopon 20715  clsccl 20822   CnP ccnp 21029  ⇝_𝑡clm 21030  1^st𝜔c1stc 21240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cc 9257  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327  df-top 20699  df-topon 20716  df-cld 20823  df-ntr 20824  df-cls 20825  df-cnp 21032  df-lm 21033  df-1stc 21242

This theorem is referenced by:  1stccn  21266  metcnp4  23108