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

Metamath Proof Explorer

Theorem iscnp2

Description: The predicate "the class F is a continuous function from topology J to topology K at point P ". Based on Theorem 7.2(g) of Munkres p. 107. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypotheses iscn.1 ⊢ 𝑋 = ∪ 𝐽
iscn.2 ⊢ 𝑌 = ∪ 𝐾
Assertion iscnp2 ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 iscn.1 ⊢ 𝑋 = ∪ 𝐽
2 iscn.2 ⊢ 𝑌 = ∪ 𝐾
3 n0i ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ¬ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) = ∅ )
4 df-ov ⊢ ( 𝐽 CnP 𝐾 ) = ( CnP ‘ ⟨ 𝐽 , 𝐾 ⟩ )
5 ndmfv ⊢ ( ¬ ⟨ 𝐽 , 𝐾 ⟩ ∈ dom CnP → ( CnP ‘ ⟨ 𝐽 , 𝐾 ⟩ ) = ∅ )
6 4 5 eqtrid ⊢ ( ¬ ⟨ 𝐽 , 𝐾 ⟩ ∈ dom CnP → ( 𝐽 CnP 𝐾 ) = ∅ )
7 6 fveq1d ⊢ ( ¬ ⟨ 𝐽 , 𝐾 ⟩ ∈ dom CnP → ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) = ( ∅ ‘ 𝑃 ) )
8 0fv ⊢ ( ∅ ‘ 𝑃 ) = ∅
9 7 8 eqtrdi ⊢ ( ¬ ⟨ 𝐽 , 𝐾 ⟩ ∈ dom CnP → ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) = ∅ )
10 3 9 nsyl2 ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ⟨ 𝐽 , 𝐾 ⟩ ∈ dom CnP )
11 df-cnp ⊢ CnP = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) )
12 ovex ⊢ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∈ V
13 ssrab2 ⊢ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ⊆ ( ∪ 𝑘 ↑m ∪ 𝑗 )
14 12 13 elpwi2 ⊢ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ∈ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 )
15 14 rgenw ⊢ ∀ 𝑥 ∈ ∪ 𝑗 { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ∈ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 )
16 eqid ⊢ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) = ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } )
17 16 fmpt ⊢ ( ∀ 𝑥 ∈ ∪ 𝑗 { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ∈ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) ↔ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) : ∪ 𝑗 ⟶ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) )
18 15 17 mpbi ⊢ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) : ∪ 𝑗 ⟶ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 )
19 vuniex ⊢ ∪ 𝑗 ∈ V
20 12 pwex ⊢ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∈ V
21 fex2 ⊢ ( ( ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) : ∪ 𝑗 ⟶ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∧ ∪ 𝑗 ∈ V ∧ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∈ V ) → ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) ∈ V )
22 18 19 20 21 mp3an ⊢ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) ∈ V
23 11 22 dmmpo ⊢ dom CnP = ( Top × Top )
24 10 23 eleqtrdi ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ⟨ 𝐽 , 𝐾 ⟩ ∈ ( Top × Top ) )
25 opelxp ⊢ ( ⟨ 𝐽 , 𝐾 ⟩ ∈ ( Top × Top ) ↔ ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) )
26 24 25 sylib ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) )
27 26 simpld ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐽 ∈ Top )
28 26 simprd ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐾 ∈ Top )
29 elfvdm ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝑃 ∈ dom ( 𝐽 CnP 𝐾 ) )
30 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
31 2 toptopon ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
32 cnpfval ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 CnP 𝐾 ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) )
33 30 31 32 syl2anb ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 CnP 𝐾 ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) )
34 26 33 syl ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ( 𝐽 CnP 𝐾 ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) )
35 34 dmeqd ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → dom ( 𝐽 CnP 𝐾 ) = dom ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) )
36 ovex ⊢ ( 𝑌 ↑m 𝑋 ) ∈ V
37 36 rabex ⊢ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ∈ V
38 37 rgenw ⊢ ∀ 𝑥 ∈ 𝑋 { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ∈ V
39 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝑋 { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ∈ V → dom ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) = 𝑋 )
40 38 39 ax-mp ⊢ dom ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) = 𝑋
41 35 40 eqtrdi ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → dom ( 𝐽 CnP 𝐾 ) = 𝑋 )
42 29 41 eleqtrd ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝑃 ∈ 𝑋 )
43 27 28 42 3jca ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋 ) )
44 biid ⊢ ( 𝑃 ∈ 𝑋 ↔ 𝑃 ∈ 𝑋 )
45 iscnp ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )
46 30 31 44 45 syl3anb ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )
47 43 46 biadanii ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )