Theorem 1stccnp

Description: A mapping is continuous at P in a first-countable space X iff it is sequentially continuous at P , meaning that the image under F of every sequence converging at P converges to F ( P ) . This proof uses ax-cc , but only via 1stcelcls , 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)

	Ref	Expression
Hypotheses	1stccnp.1	⊢ ( 𝜑 → 𝐽 ∈ 1stω )
	1stccnp.2	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	1stccnp.3	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
	1stccnp.4	⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
Assertion	1stccnp	⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		1stccnp.1	⊢ ( 𝜑 → 𝐽 ∈ 1stω )
2		1stccnp.2	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3		1stccnp.3	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
4		1stccnp.4	⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
5	2 3	jca	⊢ ( 𝜑 → ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) )
6		cnpf2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
7	6	3expa	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
8	5 7	sylan	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
9		simprr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) → 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )
10		simplr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) )
11	9 10	lmcnp	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) )
12	11	ex	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) )
13	12	alrimiv	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) )
14	8 13	jca	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) )
15		simprl	⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
16		fal	⊢ ¬ ⊥
17		19.29	⊢ ( ( ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ∧ ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) → ∃ 𝑓 ( ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) )
18		simprl	⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) → 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) )
19		difss	⊢ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ⊆ 𝑋
20		fss	⊢ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ⊆ 𝑋 ) → 𝑓 : ℕ ⟶ 𝑋 )
21	18 19 20	sylancl	⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) → 𝑓 : ℕ ⟶ 𝑋 )
22		simprr	⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) → 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )
23	21 22	jca	⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) → ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) )
24		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
25		simplrr	⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 )
26		1zzd	⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) → 1 ∈ ℤ )
27		simprr	⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) )
28		simplrl	⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) → 𝑢 ∈ 𝐾 )
29	24 25 26 27 28	lmcvg	⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑘 ) ∈ 𝑢 )
30	24	r19.2uz	⊢ ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑘 ) ∈ 𝑢 → ∃ 𝑘 ∈ ℕ ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑘 ) ∈ 𝑢 )
31		simprll	⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) → 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) )
32	31	ffnd	⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) → 𝑓 Fn ℕ )
33		fvco2	⊢ ( ( 𝑓 Fn ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑘 ) ) )
34	32 33	sylan	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑘 ) ) )
35	34	eleq1d	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑘 ) ∈ 𝑢 ↔ ( 𝐹 ‘ ( 𝑓 ‘ 𝑘 ) ) ∈ 𝑢 ) )
36	31	ffvelrnda	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑓 ‘ 𝑘 ) ∈ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) )
37	36	eldifad	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑓 ‘ 𝑘 ) ∈ 𝑋 )
38		simplr	⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
39	38	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ∧ 𝑘 ∈ ℕ ) → 𝐹 : 𝑋 ⟶ 𝑌 )
40		ffn	⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → 𝐹 Fn 𝑋 )
41		elpreima	⊢ ( 𝐹 Fn 𝑋 → ( ( 𝑓 ‘ 𝑘 ) ∈ ( ◡ 𝐹 “ 𝑢 ) ↔ ( ( 𝑓 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ ( 𝑓 ‘ 𝑘 ) ) ∈ 𝑢 ) ) )
42	39 40 41	3syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑓 ‘ 𝑘 ) ∈ ( ◡ 𝐹 “ 𝑢 ) ↔ ( ( 𝑓 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ ( 𝑓 ‘ 𝑘 ) ) ∈ 𝑢 ) ) )
43	36	eldifbd	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ∧ 𝑘 ∈ ℕ ) → ¬ ( 𝑓 ‘ 𝑘 ) ∈ ( ◡ 𝐹 “ 𝑢 ) )
44	43	pm2.21d	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑓 ‘ 𝑘 ) ∈ ( ◡ 𝐹 “ 𝑢 ) → ⊥ ) )
45	42 44	sylbird	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝑓 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ ( 𝑓 ‘ 𝑘 ) ) ∈ 𝑢 ) → ⊥ ) )
46	37 45	mpand	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝑓 ‘ 𝑘 ) ) ∈ 𝑢 → ⊥ ) )
47	35 46	sylbid	⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑘 ) ∈ 𝑢 → ⊥ ) )
48	47	rexlimdva	⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) → ( ∃ 𝑘 ∈ ℕ ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑘 ) ∈ 𝑢 → ⊥ ) )
49	30 48	syl5	⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑘 ) ∈ 𝑢 → ⊥ ) )
50	29 49	mpd	⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) → ⊥ )
51	50	expr	⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) → ( ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) → ⊥ ) )
52	23 51	embantd	⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) → ( ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) → ⊥ ) )
53	52	ex	⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) → ⊥ ) ) )
54	53	impcomd	⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → ( ( ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) → ⊥ ) )
55	54	exlimdv	⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → ( ∃ 𝑓 ( ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ∧ ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) → ⊥ ) )
56	17 55	syl5	⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → ( ( ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ∧ ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) → ⊥ ) )
57	56	exp4b	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) → ( ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) → ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ⊥ ) ) ) )
58	57	com23	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) → ( ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) → ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ⊥ ) ) ) )
59	58	impr	⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) → ( ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) → ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ⊥ ) ) )
60	59	imp	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ⊥ ) )
61	16 60	mtoi	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → ¬ ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) )
62	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → 𝐽 ∈ 1stω )
63	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
64		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
65	63 64	syl	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → 𝑋 = ∪ 𝐽 )
66	19 65	sseqtrid	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ⊆ ∪ 𝐽 )
67		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
68	67	1stcelcls	⊢ ( ( 𝐽 ∈ 1stω ∧ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ⊆ ∪ 𝐽 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) )
69	62 66 68	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) )
70	61 69	mtbird	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → ¬ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) )
71		topontop	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
72	63 71	syl	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → 𝐽 ∈ Top )
73	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → 𝑃 ∈ 𝑋 )
74	73 65	eleqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → 𝑃 ∈ ∪ 𝐽 )
75	67	elcls	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ⊆ ∪ 𝐽 ∧ 𝑃 ∈ ∪ 𝐽 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) ↔ ∀ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 → ( 𝑣 ∩ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) ≠ ∅ ) ) )
76	72 66 74 75	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) ↔ ∀ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 → ( 𝑣 ∩ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) ≠ ∅ ) ) )
77	70 76	mtbid	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → ¬ ∀ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 → ( 𝑣 ∩ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) ≠ ∅ ) )
78	15	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ 𝑣 ∈ 𝐽 ) → 𝐹 : 𝑋 ⟶ 𝑌 )
79	78	ffund	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ 𝑣 ∈ 𝐽 ) → Fun 𝐹 )
80		toponss	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ) → 𝑣 ⊆ 𝑋 )
81	63 80	sylan	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ 𝑣 ∈ 𝐽 ) → 𝑣 ⊆ 𝑋 )
82	78	fdmd	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ 𝑣 ∈ 𝐽 ) → dom 𝐹 = 𝑋 )
83	81 82	sseqtrrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ 𝑣 ∈ 𝐽 ) → 𝑣 ⊆ dom 𝐹 )
84		funimass3	⊢ ( ( Fun 𝐹 ∧ 𝑣 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ↔ 𝑣 ⊆ ( ◡ 𝐹 “ 𝑢 ) ) )
85	79 83 84	syl2anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ 𝑣 ∈ 𝐽 ) → ( ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ↔ 𝑣 ⊆ ( ◡ 𝐹 “ 𝑢 ) ) )
86		df-ss	⊢ ( 𝑣 ⊆ 𝑋 ↔ ( 𝑣 ∩ 𝑋 ) = 𝑣 )
87	81 86	sylib	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ 𝑣 ∈ 𝐽 ) → ( 𝑣 ∩ 𝑋 ) = 𝑣 )
88	87	sseq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ 𝑣 ∈ 𝐽 ) → ( ( 𝑣 ∩ 𝑋 ) ⊆ ( ◡ 𝐹 “ 𝑢 ) ↔ 𝑣 ⊆ ( ◡ 𝐹 “ 𝑢 ) ) )
89	85 88	bitr4d	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ 𝑣 ∈ 𝐽 ) → ( ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ↔ ( 𝑣 ∩ 𝑋 ) ⊆ ( ◡ 𝐹 “ 𝑢 ) ) )
90		nne	⊢ ( ¬ ( 𝑣 ∩ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) ≠ ∅ ↔ ( 𝑣 ∩ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) = ∅ )
91		inssdif0	⊢ ( ( 𝑣 ∩ 𝑋 ) ⊆ ( ◡ 𝐹 “ 𝑢 ) ↔ ( 𝑣 ∩ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) = ∅ )
92	90 91	bitr4i	⊢ ( ¬ ( 𝑣 ∩ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) ≠ ∅ ↔ ( 𝑣 ∩ 𝑋 ) ⊆ ( ◡ 𝐹 “ 𝑢 ) )
93	89 92	bitr4di	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ 𝑣 ∈ 𝐽 ) → ( ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ↔ ¬ ( 𝑣 ∩ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) ≠ ∅ ) )
94	93	anbi2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ 𝑣 ∈ 𝐽 ) → ( ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ↔ ( 𝑃 ∈ 𝑣 ∧ ¬ ( 𝑣 ∩ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) ≠ ∅ ) ) )
95	94	rexbidva	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → ( ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ↔ ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ¬ ( 𝑣 ∩ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) ≠ ∅ ) ) )
96		rexanali	⊢ ( ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ¬ ( 𝑣 ∩ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) ≠ ∅ ) ↔ ¬ ∀ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 → ( 𝑣 ∩ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) ≠ ∅ ) )
97	95 96	bitrdi	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → ( ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ↔ ¬ ∀ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 → ( 𝑣 ∩ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ) ≠ ∅ ) ) )
98	77 97	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) )
99	98	expr	⊢ ( ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) ∧ 𝑢 ∈ 𝐾 ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) )
100	99	ralrimiva	⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) → ∀ 𝑢 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) )
101		iscnp	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) ) )
102	2 3 4 101	syl3anc	⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) ) )
103	102	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) ) )
104	15 100 103	mpbir2and	⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) )
105	14 104	impbida	⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) )