This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmda ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) ) ∧ ( ( 𝑓 : ℕ ⟶ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ∧ ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑓 ‘ 𝑘 ) ∈ ( 𝑋 ∖ ( ◡ 𝐹 “ 𝑢 ) ) )
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 dfss2 ⊢ ( 𝑣 ⊆ 𝑋 ↔ ( 𝑣 ∩ 𝑋 ) = 𝑣 )
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 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) )