Metamath Proof Explorer

Theorem cncfmpt2ss

Description: Composition of continuous functions in a subset. (Contributed by Mario Carneiro, 17-May-2016)

Ref Expression
Hypotheses cncfmpt2ss.1 ⊢ J = TopOpen ⁡ ℂ fld
cncfmpt2ss.2 ⊢ F ∈ J × t J Cn J
cncfmpt2ss.3 ⊢ φ → x ∈ X ⟼ A : X ⟶cn S
cncfmpt2ss.4 ⊢ φ → x ∈ X ⟼ B : X ⟶cn S
cncfmpt2ss.5 ⊢ S ⊆ ℂ
cncfmpt2ss.6 ⊢ A ∈ S ∧ B ∈ S → A F B ∈ S
Assertion cncfmpt2ss ⊢ φ → x ∈ X ⟼ A F B : X ⟶cn S

Proof

Step Hyp Ref Expression
1 cncfmpt2ss.1 ⊢ J = TopOpen ⁡ ℂ fld
2 cncfmpt2ss.2 ⊢ F ∈ J × t J Cn J
3 cncfmpt2ss.3 ⊢ φ → x ∈ X ⟼ A : X ⟶cn S
4 cncfmpt2ss.4 ⊢ φ → x ∈ X ⟼ B : X ⟶cn S
5 cncfmpt2ss.5 ⊢ S ⊆ ℂ
6 cncfmpt2ss.6 ⊢ A ∈ S ∧ B ∈ S → A F B ∈ S
7 cncff ⊢ x ∈ X ⟼ A : X ⟶cn S → x ∈ X ⟼ A : X ⟶ S
8 3 7 syl ⊢ φ → x ∈ X ⟼ A : X ⟶ S
9 8 fvmptelrn ⊢ φ ∧ x ∈ X → A ∈ S
10 cncff ⊢ x ∈ X ⟼ B : X ⟶cn S → x ∈ X ⟼ B : X ⟶ S
11 4 10 syl ⊢ φ → x ∈ X ⟼ B : X ⟶ S
12 11 fvmptelrn ⊢ φ ∧ x ∈ X → B ∈ S
13 9 12 6 syl2anc ⊢ φ ∧ x ∈ X → A F B ∈ S
14 13 fmpttd ⊢ φ → x ∈ X ⟼ A F B : X ⟶ S
15 2 a1i ⊢ φ → F ∈ J × t J Cn J
16 ssid ⊢ ℂ ⊆ ℂ
17 cncfss ⊢ S ⊆ ℂ ∧ ℂ ⊆ ℂ → X ⟶cn S ⊆ X ⟶cn ℂ
18 5 16 17 mp2an ⊢ X ⟶cn S ⊆ X ⟶cn ℂ
19 18 3 sseldi ⊢ φ → x ∈ X ⟼ A : X ⟶cn ℂ
20 18 4 sseldi ⊢ φ → x ∈ X ⟼ B : X ⟶cn ℂ
21 1 15 19 20 cncfmpt2f ⊢ φ → x ∈ X ⟼ A F B : X ⟶cn ℂ
22 cncffvrn ⊢ S ⊆ ℂ ∧ x ∈ X ⟼ A F B : X ⟶cn ℂ → x ∈ X ⟼ A F B : X ⟶cn S ↔ x ∈ X ⟼ A F B : X ⟶ S
23 5 21 22 sylancr ⊢ φ → x ∈ X ⟼ A F B : X ⟶cn S ↔ x ∈ X ⟼ A F B : X ⟶ S
24 14 23 mpbird ⊢ φ → x ∈ X ⟼ A F B : X ⟶cn S