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 𝐿 ) ‘ 𝑃 ) )