limcun

Description: A point is a limit of F on A u. B iff it is the limit of the restriction of F to A and to B . (Contributed by Mario Carneiro, 30-Dec-2016)

	Ref	Expression
Hypotheses	limcun.1	$⊢ φ \to A \subseteq ℂ$
	limcun.2	$⊢ φ \to B \subseteq ℂ$
	limcun.3	$⊢ φ \to F : A \cup B ⟶ ℂ$
Assertion	limcun	$⊢ φ \to F {lim}_{ℂ} C = (({F ↾}_{A}) {lim}_{ℂ} C) \cap (({F ↾}_{B}) {lim}_{ℂ} C)$

Proof

Step	Hyp	Ref	Expression
1		limcun.1	$⊢ φ \to A \subseteq ℂ$
2		limcun.2	$⊢ φ \to B \subseteq ℂ$
3		limcun.3	$⊢ φ \to F : A \cup B ⟶ ℂ$
4		limcrcl	$⊢ x \in (F {lim}_{ℂ} C) \to (F : dom F ⟶ ℂ \land dom F \subseteq ℂ \land C \in ℂ)$
5	4	simp3d	$⊢ x \in (F {lim}_{ℂ} C) \to C \in ℂ$
6	5	a1i	$⊢ φ \to (x \in (F {lim}_{ℂ} C) \to C \in ℂ)$
7		elinel1	$⊢ x \in ((({F ↾}_{A}) {lim}_{ℂ} C) \cap (({F ↾}_{B}) {lim}_{ℂ} C)) \to x \in (({F ↾}_{A}) {lim}_{ℂ} C)$
8		limcrcl	$⊢ x \in (({F ↾}_{A}) {lim}_{ℂ} C) \to (({F ↾}_{A}) : dom ({F ↾}_{A}) ⟶ ℂ \land dom ({F ↾}_{A}) \subseteq ℂ \land C \in ℂ)$
9	8	simp3d	$⊢ x \in (({F ↾}_{A}) {lim}_{ℂ} C) \to C \in ℂ$
10	7 9	syl	$⊢ x \in ((({F ↾}_{A}) {lim}_{ℂ} C) \cap (({F ↾}_{B}) {lim}_{ℂ} C)) \to C \in ℂ$
11	10	a1i	$⊢ φ \to (x \in ((({F ↾}_{A}) {lim}_{ℂ} C) \cap (({F ↾}_{B}) {lim}_{ℂ} C)) \to C \in ℂ)$
12		prfi	$⊢ \{A, B\} \in Fin$
13	12	a1i	$⊢ (φ \land C \in ℂ) \to \{A, B\} \in Fin$
14	1	adantr	$⊢ (φ \land C \in ℂ) \to A \subseteq ℂ$
15	2	adantr	$⊢ (φ \land C \in ℂ) \to B \subseteq ℂ$
16		cnex	$⊢ ℂ \in V$
17	16	ssex	$⊢ A \subseteq ℂ \to A \in V$
18	14 17	syl	$⊢ (φ \land C \in ℂ) \to A \in V$
19	16	ssex	$⊢ B \subseteq ℂ \to B \in V$
20	15 19	syl	$⊢ (φ \land C \in ℂ) \to B \in V$
21		sseq1	$⊢ y = A \to (y \subseteq ℂ \leftrightarrow A \subseteq ℂ)$
22		sseq1	$⊢ y = B \to (y \subseteq ℂ \leftrightarrow B \subseteq ℂ)$
23	21 22	ralprg	$⊢ (A \in V \land B \in V) \to (\forall y \in \{A, B\} y \subseteq ℂ \leftrightarrow (A \subseteq ℂ \land B \subseteq ℂ))$
24	18 20 23	syl2anc	$⊢ (φ \land C \in ℂ) \to (\forall y \in \{A, B\} y \subseteq ℂ \leftrightarrow (A \subseteq ℂ \land B \subseteq ℂ))$
25	14 15 24	mpbir2and	$⊢ (φ \land C \in ℂ) \to \forall y \in \{A, B\} y \subseteq ℂ$
26	3	adantr	$⊢ (φ \land C \in ℂ) \to F : A \cup B ⟶ ℂ$
27		uniiun	$⊢ ⋃ \{A, B\} = ⋃_{y \in \{A, B\}} y$
28		uniprg	$⊢ (A \in V \land B \in V) \to ⋃ \{A, B\} = A \cup B$
29	18 20 28	syl2anc	$⊢ (φ \land C \in ℂ) \to ⋃ \{A, B\} = A \cup B$
30	27 29	eqtr3id	$⊢ (φ \land C \in ℂ) \to ⋃_{y \in \{A, B\}} y = A \cup B$
31	30	feq2d	$⊢ (φ \land C \in ℂ) \to (F : ⋃_{y \in \{A, B\}} y ⟶ ℂ \leftrightarrow F : A \cup B ⟶ ℂ)$
32	26 31	mpbird	$⊢ (φ \land C \in ℂ) \to F : ⋃_{y \in \{A, B\}} y ⟶ ℂ$
33		simpr	$⊢ (φ \land C \in ℂ) \to C \in ℂ$
34	13 25 32 33	limciun	$⊢ (φ \land C \in ℂ) \to F {lim}_{ℂ} C = ℂ \cap ⋂_{y \in \{A, B\}} (({F ↾}_{y}) {lim}_{ℂ} C)$
35	34	eleq2d	$⊢ (φ \land C \in ℂ) \to (x \in (F {lim}_{ℂ} C) \leftrightarrow x \in (ℂ \cap ⋂_{y \in \{A, B\}} (({F ↾}_{y}) {lim}_{ℂ} C)))$
36		reseq2	$⊢ y = A \to {F ↾}_{y} = {F ↾}_{A}$
37	36	oveq1d	$⊢ y = A \to ({F ↾}_{y}) {lim}_{ℂ} C = ({F ↾}_{A}) {lim}_{ℂ} C$
38	37	eleq2d	$⊢ y = A \to (x \in (({F ↾}_{y}) {lim}_{ℂ} C) \leftrightarrow x \in (({F ↾}_{A}) {lim}_{ℂ} C))$
39		reseq2	$⊢ y = B \to {F ↾}_{y} = {F ↾}_{B}$
40	39	oveq1d	$⊢ y = B \to ({F ↾}_{y}) {lim}_{ℂ} C = ({F ↾}_{B}) {lim}_{ℂ} C$
41	40	eleq2d	$⊢ y = B \to (x \in (({F ↾}_{y}) {lim}_{ℂ} C) \leftrightarrow x \in (({F ↾}_{B}) {lim}_{ℂ} C))$
42	38 41	ralprg	$⊢ (A \in V \land B \in V) \to (\forall y \in \{A, B\} x \in (({F ↾}_{y}) {lim}_{ℂ} C) \leftrightarrow (x \in (({F ↾}_{A}) {lim}_{ℂ} C) \land x \in (({F ↾}_{B}) {lim}_{ℂ} C)))$
43	18 20 42	syl2anc	$⊢ (φ \land C \in ℂ) \to (\forall y \in \{A, B\} x \in (({F ↾}_{y}) {lim}_{ℂ} C) \leftrightarrow (x \in (({F ↾}_{A}) {lim}_{ℂ} C) \land x \in (({F ↾}_{B}) {lim}_{ℂ} C)))$
44	43	anbi2d	$⊢ (φ \land C \in ℂ) \to ((x \in ℂ \land \forall y \in \{A, B\} x \in (({F ↾}_{y}) {lim}_{ℂ} C)) \leftrightarrow (x \in ℂ \land (x \in (({F ↾}_{A}) {lim}_{ℂ} C) \land x \in (({F ↾}_{B}) {lim}_{ℂ} C))))$
45		limccl	$⊢ ({F ↾}_{A}) {lim}_{ℂ} C \subseteq ℂ$
46	45	sseli	$⊢ x \in (({F ↾}_{A}) {lim}_{ℂ} C) \to x \in ℂ$
47	46	adantr	$⊢ (x \in (({F ↾}_{A}) {lim}_{ℂ} C) \land x \in (({F ↾}_{B}) {lim}_{ℂ} C)) \to x \in ℂ$
48	47	pm4.71ri	$⊢ (x \in (({F ↾}_{A}) {lim}_{ℂ} C) \land x \in (({F ↾}_{B}) {lim}_{ℂ} C)) \leftrightarrow (x \in ℂ \land (x \in (({F ↾}_{A}) {lim}_{ℂ} C) \land x \in (({F ↾}_{B}) {lim}_{ℂ} C)))$
49	44 48	bitr4di	$⊢ (φ \land C \in ℂ) \to ((x \in ℂ \land \forall y \in \{A, B\} x \in (({F ↾}_{y}) {lim}_{ℂ} C)) \leftrightarrow (x \in (({F ↾}_{A}) {lim}_{ℂ} C) \land x \in (({F ↾}_{B}) {lim}_{ℂ} C)))$
50		elriin	$⊢ x \in (ℂ \cap ⋂_{y \in \{A, B\}} (({F ↾}_{y}) {lim}_{ℂ} C)) \leftrightarrow (x \in ℂ \land \forall y \in \{A, B\} x \in (({F ↾}_{y}) {lim}_{ℂ} C))$
51		elin	$⊢ x \in ((({F ↾}_{A}) {lim}_{ℂ} C) \cap (({F ↾}_{B}) {lim}_{ℂ} C)) \leftrightarrow (x \in (({F ↾}_{A}) {lim}_{ℂ} C) \land x \in (({F ↾}_{B}) {lim}_{ℂ} C))$
52	49 50 51	3bitr4g	$⊢ (φ \land C \in ℂ) \to (x \in (ℂ \cap ⋂_{y \in \{A, B\}} (({F ↾}_{y}) {lim}_{ℂ} C)) \leftrightarrow x \in ((({F ↾}_{A}) {lim}_{ℂ} C) \cap (({F ↾}_{B}) {lim}_{ℂ} C)))$
53	35 52	bitrd	$⊢ (φ \land C \in ℂ) \to (x \in (F {lim}_{ℂ} C) \leftrightarrow x \in ((({F ↾}_{A}) {lim}_{ℂ} C) \cap (({F ↾}_{B}) {lim}_{ℂ} C)))$
54	53	ex	$⊢ φ \to (C \in ℂ \to (x \in (F {lim}_{ℂ} C) \leftrightarrow x \in ((({F ↾}_{A}) {lim}_{ℂ} C) \cap (({F ↾}_{B}) {lim}_{ℂ} C))))$
55	6 11 54	pm5.21ndd	$⊢ φ \to (x \in (F {lim}_{ℂ} C) \leftrightarrow x \in ((({F ↾}_{A}) {lim}_{ℂ} C) \cap (({F ↾}_{B}) {lim}_{ℂ} C)))$
56	55	eqrdv	$⊢ φ \to F {lim}_{ℂ} C = (({F ↾}_{A}) {lim}_{ℂ} C) \cap (({F ↾}_{B}) {lim}_{ℂ} C)$

Metamath Proof Explorer

Theorem limcun

Proof