limccog

Description: Limit of the composition of two functions. If the limit of F at A is B and the limit of G at B is C , then the limit of G o. F at A is C . With respect to limcco and limccnp , here we drop continuity assumptions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	limccog.1	$⊢ φ \to ran F \subseteq dom G ∖ \{B\}$
	limccog.2	$⊢ φ \to B \in (F {lim}_{ℂ} A)$
	limccog.3	$⊢ φ \to C \in (G {lim}_{ℂ} B)$
Assertion	limccog	$⊢ φ \to C \in ((G \circ F) {lim}_{ℂ} A)$

Proof

Step	Hyp	Ref	Expression
1		limccog.1	$⊢ φ \to ran F \subseteq dom G ∖ \{B\}$
2		limccog.2	$⊢ φ \to B \in (F {lim}_{ℂ} A)$
3		limccog.3	$⊢ φ \to C \in (G {lim}_{ℂ} B)$
4		limccl	$⊢ G {lim}_{ℂ} B \subseteq ℂ$
5	4 3	sseldi	$⊢ φ \to C \in ℂ$
6		limcrcl	$⊢ C \in (G {lim}_{ℂ} B) \to (G : dom G ⟶ ℂ \land dom G \subseteq ℂ \land B \in ℂ)$
7	3 6	syl	$⊢ φ \to (G : dom G ⟶ ℂ \land dom G \subseteq ℂ \land B \in ℂ)$
8	7	simp1d	$⊢ φ \to G : dom G ⟶ ℂ$
9	7	simp2d	$⊢ φ \to dom G \subseteq ℂ$
10	7	simp3d	$⊢ φ \to B \in ℂ$
11		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
12	8 9 10 11	ellimc2	$⊢ φ \to (C \in (G {lim}_{ℂ} B) \leftrightarrow (C \in ℂ \land \forall u \in TopOpen (ℂ_{fld}) (C \in u \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u))))$
13	3 12	mpbid	$⊢ φ \to (C \in ℂ \land \forall u \in TopOpen (ℂ_{fld}) (C \in u \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u)))$
14	13	simprd	$⊢ φ \to \forall u \in TopOpen (ℂ_{fld}) (C \in u \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u))$
15	14	r19.21bi	$⊢ (φ \land u \in TopOpen (ℂ_{fld})) \to (C \in u \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u))$
16	15	imp	$⊢ ((φ \land u \in TopOpen (ℂ_{fld})) \land C \in u) \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u)$
17		simp1ll	$⊢ (((φ \land u \in TopOpen (ℂ_{fld})) \land C \in u) \land v \in TopOpen (ℂ_{fld}) \land (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u)) \to φ$
18		simp2	$⊢ (((φ \land u \in TopOpen (ℂ_{fld})) \land C \in u) \land v \in TopOpen (ℂ_{fld}) \land (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u)) \to v \in TopOpen (ℂ_{fld})$
19		simp3l	$⊢ (((φ \land u \in TopOpen (ℂ_{fld})) \land C \in u) \land v \in TopOpen (ℂ_{fld}) \land (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u)) \to B \in v$
20		limcrcl	$⊢ B \in (F {lim}_{ℂ} A) \to (F : dom F ⟶ ℂ \land dom F \subseteq ℂ \land A \in ℂ)$
21	2 20	syl	$⊢ φ \to (F : dom F ⟶ ℂ \land dom F \subseteq ℂ \land A \in ℂ)$
22	21	simp1d	$⊢ φ \to F : dom F ⟶ ℂ$
23	21	simp2d	$⊢ φ \to dom F \subseteq ℂ$
24	21	simp3d	$⊢ φ \to A \in ℂ$
25	22 23 24 11	ellimc2	$⊢ φ \to (B \in (F {lim}_{ℂ} A) \leftrightarrow (B \in ℂ \land \forall v \in TopOpen (ℂ_{fld}) (B \in v \to \exists w \in TopOpen (ℂ_{fld}) (A \in w \land F [w \cap (dom F ∖ \{A\})] \subseteq v))))$
26	2 25	mpbid	$⊢ φ \to (B \in ℂ \land \forall v \in TopOpen (ℂ_{fld}) (B \in v \to \exists w \in TopOpen (ℂ_{fld}) (A \in w \land F [w \cap (dom F ∖ \{A\})] \subseteq v)))$
27	26	simprd	$⊢ φ \to \forall v \in TopOpen (ℂ_{fld}) (B \in v \to \exists w \in TopOpen (ℂ_{fld}) (A \in w \land F [w \cap (dom F ∖ \{A\})] \subseteq v))$
28	27	r19.21bi	$⊢ (φ \land v \in TopOpen (ℂ_{fld})) \to (B \in v \to \exists w \in TopOpen (ℂ_{fld}) (A \in w \land F [w \cap (dom F ∖ \{A\})] \subseteq v))$
29	28	imp	$⊢ ((φ \land v \in TopOpen (ℂ_{fld})) \land B \in v) \to \exists w \in TopOpen (ℂ_{fld}) (A \in w \land F [w \cap (dom F ∖ \{A\})] \subseteq v)$
30	17 18 19 29	syl21anc	$⊢ (((φ \land u \in TopOpen (ℂ_{fld})) \land C \in u) \land v \in TopOpen (ℂ_{fld}) \land (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u)) \to \exists w \in TopOpen (ℂ_{fld}) (A \in w \land F [w \cap (dom F ∖ \{A\})] \subseteq v)$
31		imaco	$⊢ (G \circ F) [w \cap (dom F ∖ \{A\})] = G [F [w \cap (dom F ∖ \{A\})]]$
32	17	ad2antrr	$⊢ (((((φ \land u \in TopOpen (ℂ_{fld})) \land C \in u) \land v \in TopOpen (ℂ_{fld}) \land (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u)) \land w \in TopOpen (ℂ_{fld})) \land F [w \cap (dom F ∖ \{A\})] \subseteq v) \to φ$
33		simpl3r	$⊢ ((((φ \land u \in TopOpen (ℂ_{fld})) \land C \in u) \land v \in TopOpen (ℂ_{fld}) \land (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u)) \land w \in TopOpen (ℂ_{fld})) \to G [v \cap (dom G ∖ \{B\})] \subseteq u$
34	33	adantr	$⊢ (((((φ \land u \in TopOpen (ℂ_{fld})) \land C \in u) \land v \in TopOpen (ℂ_{fld}) \land (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u)) \land w \in TopOpen (ℂ_{fld})) \land F [w \cap (dom F ∖ \{A\})] \subseteq v) \to G [v \cap (dom G ∖ \{B\})] \subseteq u$
35		simpr	$⊢ (((((φ \land u \in TopOpen (ℂ_{fld})) \land C \in u) \land v \in TopOpen (ℂ_{fld}) \land (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u)) \land w \in TopOpen (ℂ_{fld})) \land F [w \cap (dom F ∖ \{A\})] \subseteq v) \to F [w \cap (dom F ∖ \{A\})] \subseteq v$
36		simpr	$⊢ (φ \land F [w \cap (dom F ∖ \{A\})] \subseteq v) \to F [w \cap (dom F ∖ \{A\})] \subseteq v$
37		imassrn	$⊢ F [w \cap (dom F ∖ \{A\})] \subseteq ran F$
38	37 1	sstrid	$⊢ φ \to F [w \cap (dom F ∖ \{A\})] \subseteq dom G ∖ \{B\}$
39	38	adantr	$⊢ (φ \land F [w \cap (dom F ∖ \{A\})] \subseteq v) \to F [w \cap (dom F ∖ \{A\})] \subseteq dom G ∖ \{B\}$
40	36 39	ssind	$⊢ (φ \land F [w \cap (dom F ∖ \{A\})] \subseteq v) \to F [w \cap (dom F ∖ \{A\})] \subseteq v \cap (dom G ∖ \{B\})$
41		imass2	$⊢ F [w \cap (dom F ∖ \{A\})] \subseteq v \cap (dom G ∖ \{B\}) \to G [F [w \cap (dom F ∖ \{A\})]] \subseteq G [v \cap (dom G ∖ \{B\})]$
42	40 41	syl	$⊢ (φ \land F [w \cap (dom F ∖ \{A\})] \subseteq v) \to G [F [w \cap (dom F ∖ \{A\})]] \subseteq G [v \cap (dom G ∖ \{B\})]$
43	42	adantlr	$⊢ ((φ \land G [v \cap (dom G ∖ \{B\})] \subseteq u) \land F [w \cap (dom F ∖ \{A\})] \subseteq v) \to G [F [w \cap (dom F ∖ \{A\})]] \subseteq G [v \cap (dom G ∖ \{B\})]$
44		simplr	$⊢ ((φ \land G [v \cap (dom G ∖ \{B\})] \subseteq u) \land F [w \cap (dom F ∖ \{A\})] \subseteq v) \to G [v \cap (dom G ∖ \{B\})] \subseteq u$
45	43 44	sstrd	$⊢ ((φ \land G [v \cap (dom G ∖ \{B\})] \subseteq u) \land F [w \cap (dom F ∖ \{A\})] \subseteq v) \to G [F [w \cap (dom F ∖ \{A\})]] \subseteq u$
46	32 34 35 45	syl21anc	$⊢ (((((φ \land u \in TopOpen (ℂ_{fld})) \land C \in u) \land v \in TopOpen (ℂ_{fld}) \land (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u)) \land w \in TopOpen (ℂ_{fld})) \land F [w \cap (dom F ∖ \{A\})] \subseteq v) \to G [F [w \cap (dom F ∖ \{A\})]] \subseteq u$
47	31 46	eqsstrid	$⊢ (((((φ \land u \in TopOpen (ℂ_{fld})) \land C \in u) \land v \in TopOpen (ℂ_{fld}) \land (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u)) \land w \in TopOpen (ℂ_{fld})) \land F [w \cap (dom F ∖ \{A\})] \subseteq v) \to (G \circ F) [w \cap (dom F ∖ \{A\})] \subseteq u$
48	47	ex	$⊢ ((((φ \land u \in TopOpen (ℂ_{fld})) \land C \in u) \land v \in TopOpen (ℂ_{fld}) \land (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u)) \land w \in TopOpen (ℂ_{fld})) \to (F [w \cap (dom F ∖ \{A\})] \subseteq v \to (G \circ F) [w \cap (dom F ∖ \{A\})] \subseteq u)$
49	48	anim2d	$⊢ ((((φ \land u \in TopOpen (ℂ_{fld})) \land C \in u) \land v \in TopOpen (ℂ_{fld}) \land (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u)) \land w \in TopOpen (ℂ_{fld})) \to ((A \in w \land F [w \cap (dom F ∖ \{A\})] \subseteq v) \to (A \in w \land (G \circ F) [w \cap (dom F ∖ \{A\})] \subseteq u))$
50	49	reximdva	$⊢ (((φ \land u \in TopOpen (ℂ_{fld})) \land C \in u) \land v \in TopOpen (ℂ_{fld}) \land (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u)) \to (\exists w \in TopOpen (ℂ_{fld}) (A \in w \land F [w \cap (dom F ∖ \{A\})] \subseteq v) \to \exists w \in TopOpen (ℂ_{fld}) (A \in w \land (G \circ F) [w \cap (dom F ∖ \{A\})] \subseteq u))$
51	30 50	mpd	$⊢ (((φ \land u \in TopOpen (ℂ_{fld})) \land C \in u) \land v \in TopOpen (ℂ_{fld}) \land (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u)) \to \exists w \in TopOpen (ℂ_{fld}) (A \in w \land (G \circ F) [w \cap (dom F ∖ \{A\})] \subseteq u)$
52	51	rexlimdv3a	$⊢ ((φ \land u \in TopOpen (ℂ_{fld})) \land C \in u) \to (\exists v \in TopOpen (ℂ_{fld}) (B \in v \land G [v \cap (dom G ∖ \{B\})] \subseteq u) \to \exists w \in TopOpen (ℂ_{fld}) (A \in w \land (G \circ F) [w \cap (dom F ∖ \{A\})] \subseteq u))$
53	16 52	mpd	$⊢ ((φ \land u \in TopOpen (ℂ_{fld})) \land C \in u) \to \exists w \in TopOpen (ℂ_{fld}) (A \in w \land (G \circ F) [w \cap (dom F ∖ \{A\})] \subseteq u)$
54	53	ex	$⊢ (φ \land u \in TopOpen (ℂ_{fld})) \to (C \in u \to \exists w \in TopOpen (ℂ_{fld}) (A \in w \land (G \circ F) [w \cap (dom F ∖ \{A\})] \subseteq u))$
55	54	ralrimiva	$⊢ φ \to \forall u \in TopOpen (ℂ_{fld}) (C \in u \to \exists w \in TopOpen (ℂ_{fld}) (A \in w \land (G \circ F) [w \cap (dom F ∖ \{A\})] \subseteq u))$
56	22	ffund	$⊢ φ \to Fun F$
57		fdmrn	$⊢ Fun F \leftrightarrow F : dom F ⟶ ran F$
58	56 57	sylib	$⊢ φ \to F : dom F ⟶ ran F$
59	1	difss2d	$⊢ φ \to ran F \subseteq dom G$
60	58 59	fssd	$⊢ φ \to F : dom F ⟶ dom G$
61		fco	$⊢ (G : dom G ⟶ ℂ \land F : dom F ⟶ dom G) \to (G \circ F) : dom F ⟶ ℂ$
62	8 60 61	syl2anc	$⊢ φ \to (G \circ F) : dom F ⟶ ℂ$
63	62 23 24 11	ellimc2	$⊢ φ \to (C \in ((G \circ F) {lim}_{ℂ} A) \leftrightarrow (C \in ℂ \land \forall u \in TopOpen (ℂ_{fld}) (C \in u \to \exists w \in TopOpen (ℂ_{fld}) (A \in w \land (G \circ F) [w \cap (dom F ∖ \{A\})] \subseteq u))))$
64	5 55 63	mpbir2and	$⊢ φ \to C \in ((G \circ F) {lim}_{ℂ} A)$

Metamath Proof Explorer

Theorem limccog

Proof