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 ∧ 𝑃𝑋 ) ∧ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑦𝐾 ( ( 𝐹𝑃 ) ∈ 𝑦 → ∃ 𝑥𝐽 ( 𝑃𝑥 ∧ ( 𝐹𝑥 ) ⊆ 𝑦 ) ) ) ) )