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

Metamath Proof Explorer

Theorem cnpco

Description: The composition of a function F continuous at P with a function continuous at ( FP ) is continuous at P . Proposition 2 of BourbakiTop1 p. I.9. (Contributed by FL, 16-Nov-2006) (Proof shortened by Mario Carneiro, 27-Dec-2014)

Ref Expression
Assertion cnpco ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) → ( 𝐺 ∘ 𝐹 ) ∈ ( ( 𝐽 CnP 𝐿 ) ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 cnptop1 ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐽 ∈ Top )
2 1 adantr ⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) → 𝐽 ∈ Top )
3 cnptop2 ⊢ ( 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) → 𝐿 ∈ Top )
4 3 adantl ⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) → 𝐿 ∈ Top )
5 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
6 5 cnprcl ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝑃 ∈ ∪ 𝐽 )
7 6 adantr ⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) → 𝑃 ∈ ∪ 𝐽 )
8 2 4 7 3jca ⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) → ( 𝐽 ∈ Top ∧ 𝐿 ∈ Top ∧ 𝑃 ∈ ∪ 𝐽 ) )
9 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
10 eqid ⊢ ∪ 𝐿 = ∪ 𝐿
11 9 10 cnpf ⊢ ( 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) → 𝐺 : ∪ 𝐾 ⟶ ∪ 𝐿 )
12 11 adantl ⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) → 𝐺 : ∪ 𝐾 ⟶ ∪ 𝐿 )
13 5 9 cnpf ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
14 13 adantr ⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
15 fco ⊢ ( ( 𝐺 : ∪ 𝐾 ⟶ ∪ 𝐿 ∧ 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 ) → ( 𝐺 ∘ 𝐹 ) : ∪ 𝐽 ⟶ ∪ 𝐿 )
16 12 14 15 syl2anc ⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) → ( 𝐺 ∘ 𝐹 ) : ∪ 𝐽 ⟶ ∪ 𝐿 )
17 simplr ⊢ ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝑧 ∈ 𝐿 ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 ) ) → 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) )
18 simprl ⊢ ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝑧 ∈ 𝐿 ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 ) ) → 𝑧 ∈ 𝐿 )
19 fvco3 ⊢ ( ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 ∧ 𝑃 ∈ ∪ 𝐽 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑃 ) ) )
20 14 7 19 syl2anc ⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑃 ) ) )
21 20 adantr ⊢ ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝑧 ∈ 𝐿 ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 ) ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑃 ) ) )
22 simprr ⊢ ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝑧 ∈ 𝐿 ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 ) ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 )
23 21 22 eqeltrrd ⊢ ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝑧 ∈ 𝐿 ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 ) ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑃 ) ) ∈ 𝑧 )
24 cnpimaex ⊢ ( ( 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑧 ∈ 𝐿 ∧ ( 𝐺 ‘ ( 𝐹 ‘ 𝑃 ) ) ∈ 𝑧 ) → ∃ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ ( 𝐺 “ 𝑦 ) ⊆ 𝑧 ) )
25 17 18 23 24 syl3anc ⊢ ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝑧 ∈ 𝐿 ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 ) ) → ∃ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ ( 𝐺 “ 𝑦 ) ⊆ 𝑧 ) )
26 simplll ⊢ ( ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝑧 ∈ 𝐿 ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 ) ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ ( 𝐺 “ 𝑦 ) ⊆ 𝑧 ) ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) )
27 simprl ⊢ ( ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝑧 ∈ 𝐿 ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 ) ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ ( 𝐺 “ 𝑦 ) ⊆ 𝑧 ) ) ) → 𝑦 ∈ 𝐾 )
28 simprrl ⊢ ( ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝑧 ∈ 𝐿 ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 ) ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ ( 𝐺 “ 𝑦 ) ⊆ 𝑧 ) ) ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 )
29 cnpimaex ⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) )
30 26 27 28 29 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝑧 ∈ 𝐿 ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 ) ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ ( 𝐺 “ 𝑦 ) ⊆ 𝑧 ) ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) )
31 imaco ⊢ ( ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) = ( 𝐺 “ ( 𝐹 “ 𝑥 ) )
32 imass2 ⊢ ( ( 𝐹 “ 𝑥 ) ⊆ 𝑦 → ( 𝐺 “ ( 𝐹 “ 𝑥 ) ) ⊆ ( 𝐺 “ 𝑦 ) )
33 31 32 eqsstrid ⊢ ( ( 𝐹 “ 𝑥 ) ⊆ 𝑦 → ( ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ⊆ ( 𝐺 “ 𝑦 ) )
34 simprrr ⊢ ( ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝑧 ∈ 𝐿 ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 ) ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ ( 𝐺 “ 𝑦 ) ⊆ 𝑧 ) ) ) → ( 𝐺 “ 𝑦 ) ⊆ 𝑧 )
35 sstr2 ⊢ ( ( ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ⊆ ( 𝐺 “ 𝑦 ) → ( ( 𝐺 “ 𝑦 ) ⊆ 𝑧 → ( ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ⊆ 𝑧 ) )
36 33 34 35 syl2imc ⊢ ( ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝑧 ∈ 𝐿 ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 ) ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ ( 𝐺 “ 𝑦 ) ⊆ 𝑧 ) ) ) → ( ( 𝐹 “ 𝑥 ) ⊆ 𝑦 → ( ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ⊆ 𝑧 ) )
37 36 anim2d ⊢ ( ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝑧 ∈ 𝐿 ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 ) ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ ( 𝐺 “ 𝑦 ) ⊆ 𝑧 ) ) ) → ( ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) → ( 𝑃 ∈ 𝑥 ∧ ( ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ⊆ 𝑧 ) ) )
38 37 reximdv ⊢ ( ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝑧 ∈ 𝐿 ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 ) ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ ( 𝐺 “ 𝑦 ) ⊆ 𝑧 ) ) ) → ( ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ⊆ 𝑧 ) ) )
39 30 38 mpd ⊢ ( ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝑧 ∈ 𝐿 ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 ) ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ ( 𝐺 “ 𝑦 ) ⊆ 𝑧 ) ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ⊆ 𝑧 ) )
40 25 39 rexlimddv ⊢ ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝑧 ∈ 𝐿 ∧ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ⊆ 𝑧 ) )
41 40 expr ⊢ ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) ∧ 𝑧 ∈ 𝐿 ) → ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ⊆ 𝑧 ) ) )
42 41 ralrimiva ⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) → ∀ 𝑧 ∈ 𝐿 ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ⊆ 𝑧 ) ) )
43 16 42 jca ⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) → ( ( 𝐺 ∘ 𝐹 ) : ∪ 𝐽 ⟶ ∪ 𝐿 ∧ ∀ 𝑧 ∈ 𝐿 ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ⊆ 𝑧 ) ) ) )
44 5 10 iscnp2 ⊢ ( ( 𝐺 ∘ 𝐹 ) ∈ ( ( 𝐽 CnP 𝐿 ) ‘ 𝑃 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐿 ∈ Top ∧ 𝑃 ∈ ∪ 𝐽 ) ∧ ( ( 𝐺 ∘ 𝐹 ) : ∪ 𝐽 ⟶ ∪ 𝐿 ∧ ∀ 𝑧 ∈ 𝐿 ( ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑧 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( ( 𝐺 ∘ 𝐹 ) “ 𝑥 ) ⊆ 𝑧 ) ) ) ) )
45 8 43 44 sylanbrc ⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐺 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ ( 𝐹 ‘ 𝑃 ) ) ) → ( 𝐺 ∘ 𝐹 ) ∈ ( ( 𝐽 CnP 𝐿 ) ‘ 𝑃 ) )