Metamath Proof Explorer

Theorem cnmptre

Description: Lemma for iirevcn and related functions. (Contributed by Mario Carneiro, 6-Jun-2014)

Ref Expression
Hypotheses cnmptre.1 ⊢ 𝑅 = ( TopOpen ‘ ℂfld )
cnmptre.2 ⊢ 𝐽 = ( ( topGen ‘ ran (,) ) ↾t 𝐴 )
cnmptre.3 ⊢ 𝐾 = ( ( topGen ‘ ran (,) ) ↾t 𝐵 )
cnmptre.4 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
cnmptre.5 ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
cnmptre.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 ∈ 𝐵 )
cnmptre.7 ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ 𝐹 ) ∈ ( 𝑅 Cn 𝑅 ) )
Assertion cnmptre ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 cnmptre.1 ⊢ 𝑅 = ( TopOpen ‘ ℂfld )
2 cnmptre.2 ⊢ 𝐽 = ( ( topGen ‘ ran (,) ) ↾t 𝐴 )
3 cnmptre.3 ⊢ 𝐾 = ( ( topGen ‘ ran (,) ) ↾t 𝐵 )
4 cnmptre.4 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
5 cnmptre.5 ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
6 cnmptre.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 ∈ 𝐵 )
7 cnmptre.7 ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ 𝐹 ) ∈ ( 𝑅 Cn 𝑅 ) )
8 eqid ⊢ ( 𝑅 ↾t 𝐴 ) = ( 𝑅 ↾t 𝐴 )
9 1 cnfldtopon ⊢ 𝑅 ∈ ( TopOn ‘ ℂ )
10 9 a1i ⊢ ( 𝜑 → 𝑅 ∈ ( TopOn ‘ ℂ ) )
11 ax-resscn ⊢ ℝ ⊆ ℂ
12 4 11 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
13 8 10 12 7 cnmpt1res ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( ( 𝑅 ↾t 𝐴 ) Cn 𝑅 ) )
14 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
15 1 14 rerest ⊢ ( 𝐴 ⊆ ℝ → ( 𝑅 ↾t 𝐴 ) = ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) )
16 4 15 syl ⊢ ( 𝜑 → ( 𝑅 ↾t 𝐴 ) = ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) )
17 16 2 eqtr4di ⊢ ( 𝜑 → ( 𝑅 ↾t 𝐴 ) = 𝐽 )
18 17 oveq1d ⊢ ( 𝜑 → ( ( 𝑅 ↾t 𝐴 ) Cn 𝑅 ) = ( 𝐽 Cn 𝑅 ) )
19 13 18 eleqtrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐽 Cn 𝑅 ) )
20 6 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) : 𝐴 ⟶ 𝐵 )
21 20 frnd ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ⊆ 𝐵 )
22 5 11 sstrdi ⊢ ( 𝜑 → 𝐵 ⊆ ℂ )
23 cnrest2 ⊢ ( ( 𝑅 ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ⊆ 𝐵 ∧ 𝐵 ⊆ ℂ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐽 Cn 𝑅 ) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐽 Cn ( 𝑅 ↾t 𝐵 ) ) ) )
24 9 21 22 23 mp3an2i ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐽 Cn 𝑅 ) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐽 Cn ( 𝑅 ↾t 𝐵 ) ) ) )
25 19 24 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐽 Cn ( 𝑅 ↾t 𝐵 ) ) )
26 1 14 rerest ⊢ ( 𝐵 ⊆ ℝ → ( 𝑅 ↾t 𝐵 ) = ( ( topGen ‘ ran (,) ) ↾t 𝐵 ) )
27 5 26 syl ⊢ ( 𝜑 → ( 𝑅 ↾t 𝐵 ) = ( ( topGen ‘ ran (,) ) ↾t 𝐵 ) )
28 27 3 eqtr4di ⊢ ( 𝜑 → ( 𝑅 ↾t 𝐵 ) = 𝐾 )
29 28 oveq2d ⊢ ( 𝜑 → ( 𝐽 Cn ( 𝑅 ↾t 𝐵 ) ) = ( 𝐽 Cn 𝐾 ) )
30 25 29 eleqtrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) )