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	$⊢ (F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \to G \circ F \in (J CnP L) (P)$

Proof

Step	Hyp	Ref	Expression
1		cnptop1	$⊢ F \in (J CnP K) (P) \to J \in Top$
2	1	adantr	$⊢ (F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \to J \in Top$
3		cnptop2	$⊢ G \in (K CnP L) (F (P)) \to L \in Top$
4	3	adantl	$⊢ (F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \to L \in Top$
5		eqid	$⊢ ⋃ J = ⋃ J$
6	5	cnprcl	$⊢ F \in (J CnP K) (P) \to P \in ⋃ J$
7	6	adantr	$⊢ (F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \to P \in ⋃ J$
8	2 4 7	3jca	$⊢ (F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \to (J \in Top \land L \in Top \land P \in ⋃ J)$
9		eqid	$⊢ ⋃ K = ⋃ K$
10		eqid	$⊢ ⋃ L = ⋃ L$
11	9 10	cnpf	$⊢ G \in (K CnP L) (F (P)) \to G : ⋃ K ⟶ ⋃ L$
12	11	adantl	$⊢ (F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \to G : ⋃ K ⟶ ⋃ L$
13	5 9	cnpf	$⊢ F \in (J CnP K) (P) \to F : ⋃ J ⟶ ⋃ K$
14	13	adantr	$⊢ (F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \to F : ⋃ J ⟶ ⋃ K$
15		fco	$⊢ (G : ⋃ K ⟶ ⋃ L \land F : ⋃ J ⟶ ⋃ K) \to (G \circ F) : ⋃ J ⟶ ⋃ L$
16	12 14 15	syl2anc	$⊢ (F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \to (G \circ F) : ⋃ J ⟶ ⋃ L$
17		simplr	$⊢ ((F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \land (z \in L \land (G \circ F) (P) \in z)) \to G \in (K CnP L) (F (P))$
18		simprl	$⊢ ((F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \land (z \in L \land (G \circ F) (P) \in z)) \to z \in L$
19		fvco3	$⊢ (F : ⋃ J ⟶ ⋃ K \land P \in ⋃ J) \to (G \circ F) (P) = G (F (P))$
20	14 7 19	syl2anc	$⊢ (F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \to (G \circ F) (P) = G (F (P))$
21	20	adantr	$⊢ ((F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \land (z \in L \land (G \circ F) (P) \in z)) \to (G \circ F) (P) = G (F (P))$
22		simprr	$⊢ ((F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \land (z \in L \land (G \circ F) (P) \in z)) \to (G \circ F) (P) \in z$
23	21 22	eqeltrrd	$⊢ ((F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \land (z \in L \land (G \circ F) (P) \in z)) \to G (F (P)) \in z$
24		cnpimaex	$⊢ (G \in (K CnP L) (F (P)) \land z \in L \land G (F (P)) \in z) \to \exists y \in K (F (P) \in y \land G [y] \subseteq z)$
25	17 18 23 24	syl3anc	$⊢ ((F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \land (z \in L \land (G \circ F) (P) \in z)) \to \exists y \in K (F (P) \in y \land G [y] \subseteq z)$
26		simplll	$⊢ (((F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \land (z \in L \land (G \circ F) (P) \in z)) \land (y \in K \land (F (P) \in y \land G [y] \subseteq z))) \to F \in (J CnP K) (P)$
27		simprl	$⊢ (((F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \land (z \in L \land (G \circ F) (P) \in z)) \land (y \in K \land (F (P) \in y \land G [y] \subseteq z))) \to y \in K$
28		simprrl	$⊢ (((F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \land (z \in L \land (G \circ F) (P) \in z)) \land (y \in K \land (F (P) \in y \land G [y] \subseteq z))) \to F (P) \in y$
29		cnpimaex	$⊢ (F \in (J CnP K) (P) \land y \in K \land F (P) \in y) \to \exists x \in J (P \in x \land F [x] \subseteq y)$
30	26 27 28 29	syl3anc	$⊢ (((F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \land (z \in L \land (G \circ F) (P) \in z)) \land (y \in K \land (F (P) \in y \land G [y] \subseteq z))) \to \exists x \in J (P \in x \land F [x] \subseteq y)$
31		imaco	$⊢ (G \circ F) [x] = G [F [x]]$
32		imass2	$⊢ F [x] \subseteq y \to G [F [x]] \subseteq G [y]$
33	31 32	eqsstrid	$⊢ F [x] \subseteq y \to (G \circ F) [x] \subseteq G [y]$
34		simprrr	$⊢ (((F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \land (z \in L \land (G \circ F) (P) \in z)) \land (y \in K \land (F (P) \in y \land G [y] \subseteq z))) \to G [y] \subseteq z$
35		sstr2	$⊢ (G \circ F) [x] \subseteq G [y] \to (G [y] \subseteq z \to (G \circ F) [x] \subseteq z)$
36	33 34 35	syl2imc	$⊢ (((F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \land (z \in L \land (G \circ F) (P) \in z)) \land (y \in K \land (F (P) \in y \land G [y] \subseteq z))) \to (F [x] \subseteq y \to (G \circ F) [x] \subseteq z)$
37	36	anim2d	$⊢ (((F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \land (z \in L \land (G \circ F) (P) \in z)) \land (y \in K \land (F (P) \in y \land G [y] \subseteq z))) \to ((P \in x \land F [x] \subseteq y) \to (P \in x \land (G \circ F) [x] \subseteq z))$
38	37	reximdv	$⊢ (((F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \land (z \in L \land (G \circ F) (P) \in z)) \land (y \in K \land (F (P) \in y \land G [y] \subseteq z))) \to (\exists x \in J (P \in x \land F [x] \subseteq y) \to \exists x \in J (P \in x \land (G \circ F) [x] \subseteq z))$
39	30 38	mpd	$⊢ (((F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \land (z \in L \land (G \circ F) (P) \in z)) \land (y \in K \land (F (P) \in y \land G [y] \subseteq z))) \to \exists x \in J (P \in x \land (G \circ F) [x] \subseteq z)$
40	25 39	rexlimddv	$⊢ ((F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \land (z \in L \land (G \circ F) (P) \in z)) \to \exists x \in J (P \in x \land (G \circ F) [x] \subseteq z)$
41	40	expr	$⊢ ((F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \land z \in L) \to ((G \circ F) (P) \in z \to \exists x \in J (P \in x \land (G \circ F) [x] \subseteq z))$
42	41	ralrimiva	$⊢ (F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \to \forall z \in L ((G \circ F) (P) \in z \to \exists x \in J (P \in x \land (G \circ F) [x] \subseteq z))$
43	16 42	jca	$⊢ (F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \to ((G \circ F) : ⋃ J ⟶ ⋃ L \land \forall z \in L ((G \circ F) (P) \in z \to \exists x \in J (P \in x \land (G \circ F) [x] \subseteq z)))$
44	5 10	iscnp2	$⊢ G \circ F \in (J CnP L) (P) \leftrightarrow ((J \in Top \land L \in Top \land P \in ⋃ J) \land ((G \circ F) : ⋃ J ⟶ ⋃ L \land \forall z \in L ((G \circ F) (P) \in z \to \exists x \in J (P \in x \land (G \circ F) [x] \subseteq z))))$
45	8 43 44	sylanbrc	$⊢ (F \in (J CnP K) (P) \land G \in (K CnP L) (F (P))) \to G \circ F \in (J CnP L) (P)$

Metamath Proof Explorer

Theorem cnpco

Proof