limciun

Description: A point is a limit of F on the finite union U_ x e. A B ( x ) iff it is the limit of the restriction of F to each B ( x ) . (Contributed by Mario Carneiro, 30-Dec-2016)

	Ref	Expression
Hypotheses	limciun.1	$⊢ φ \to A \in Fin$
	limciun.2	$⊢ φ \to \forall x \in A B \subseteq ℂ$
	limciun.3	$⊢ φ \to F : ⋃_{x \in A} B ⟶ ℂ$
	limciun.4	$⊢ φ \to C \in ℂ$
Assertion	limciun	$⊢ φ \to F {lim}_{ℂ} C = ℂ \cap ⋂_{x \in A} (({F ↾}_{B}) {lim}_{ℂ} C)$

Proof

Step	Hyp	Ref	Expression
1		limciun.1	$⊢ φ \to A \in Fin$
2		limciun.2	$⊢ φ \to \forall x \in A B \subseteq ℂ$
3		limciun.3	$⊢ φ \to F : ⋃_{x \in A} B ⟶ ℂ$
4		limciun.4	$⊢ φ \to C \in ℂ$
5		limccl	$⊢ F {lim}_{ℂ} C \subseteq ℂ$
6		limcresi	$⊢ F {lim}_{ℂ} C \subseteq ({F ↾}_{B}) {lim}_{ℂ} C$
7	6	rgenw	$⊢ \forall x \in A F {lim}_{ℂ} C \subseteq ({F ↾}_{B}) {lim}_{ℂ} C$
8		ssiin	$⊢ F {lim}_{ℂ} C \subseteq ⋂_{x \in A} (({F ↾}_{B}) {lim}_{ℂ} C) \leftrightarrow \forall x \in A F {lim}_{ℂ} C \subseteq ({F ↾}_{B}) {lim}_{ℂ} C$
9	7 8	mpbir	$⊢ F {lim}_{ℂ} C \subseteq ⋂_{x \in A} (({F ↾}_{B}) {lim}_{ℂ} C)$
10	5 9	ssini	$⊢ F {lim}_{ℂ} C \subseteq ℂ \cap ⋂_{x \in A} (({F ↾}_{B}) {lim}_{ℂ} C)$
11	10	a1i	$⊢ φ \to F {lim}_{ℂ} C \subseteq ℂ \cap ⋂_{x \in A} (({F ↾}_{B}) {lim}_{ℂ} C)$
12		elriin	$⊢ y \in (ℂ \cap ⋂_{x \in A} (({F ↾}_{B}) {lim}_{ℂ} C)) \leftrightarrow (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))$
13		simprl	$⊢ (φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \to y \in ℂ$
14	1	ad2antrr	$⊢ ((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \to A \in Fin$
15		simplrr	$⊢ ((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \to \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C)$
16		nfcv	$⊢ \underline{Ⅎ} x F$
17		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ a / x ⦌ B$
18	16 17	nfres	$⊢ \underline{Ⅎ} x ({F ↾}_{⦋ a / x ⦌ B})$
19		nfcv	$⊢ \underline{Ⅎ} x {lim}_{ℂ}$
20		nfcv	$⊢ \underline{Ⅎ} x C$
21	18 19 20	nfov	$⊢ \underline{Ⅎ} x (({F ↾}_{⦋ a / x ⦌ B}) {lim}_{ℂ} C)$
22	21	nfcri	$⊢ Ⅎ x y \in (({F ↾}_{⦋ a / x ⦌ B}) {lim}_{ℂ} C)$
23		csbeq1a	$⊢ x = a \to B = ⦋ a / x ⦌ B$
24	23	reseq2d	$⊢ x = a \to {F ↾}_{B} = {F ↾}_{⦋ a / x ⦌ B}$
25	24	oveq1d	$⊢ x = a \to ({F ↾}_{B}) {lim}_{ℂ} C = ({F ↾}_{⦋ a / x ⦌ B}) {lim}_{ℂ} C$
26	25	eleq2d	$⊢ x = a \to (y \in (({F ↾}_{B}) {lim}_{ℂ} C) \leftrightarrow y \in (({F ↾}_{⦋ a / x ⦌ B}) {lim}_{ℂ} C))$
27	22 26	rspc	$⊢ a \in A \to (\forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C) \to y \in (({F ↾}_{⦋ a / x ⦌ B}) {lim}_{ℂ} C))$
28	15 27	mpan9	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land a \in A) \to y \in (({F ↾}_{⦋ a / x ⦌ B}) {lim}_{ℂ} C)$
29	3	ad2antrr	$⊢ ((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land a \in A) \to F : ⋃_{x \in A} B ⟶ ℂ$
30		ssiun2	$⊢ a \in A \to ⦋ a / x ⦌ B \subseteq ⋃_{a \in A} ⦋ a / x ⦌ B$
31		nfcv	$⊢ \underline{Ⅎ} a B$
32	31 17 23	cbviun	$⊢ ⋃_{x \in A} B = ⋃_{a \in A} ⦋ a / x ⦌ B$
33	30 32	sseqtrrdi	$⊢ a \in A \to ⦋ a / x ⦌ B \subseteq ⋃_{x \in A} B$
34	33	adantl	$⊢ ((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land a \in A) \to ⦋ a / x ⦌ B \subseteq ⋃_{x \in A} B$
35	29 34	fssresd	$⊢ ((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land a \in A) \to ({F ↾}_{⦋ a / x ⦌ B}) : ⦋ a / x ⦌ B ⟶ ℂ$
36		simpr	$⊢ ((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land a \in A) \to a \in A$
37	2	ad2antrr	$⊢ ((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land a \in A) \to \forall x \in A B \subseteq ℂ$
38		nfcv	$⊢ \underline{Ⅎ} x ℂ$
39	17 38	nfss	$⊢ Ⅎ x ⦋ a / x ⦌ B \subseteq ℂ$
40	23	sseq1d	$⊢ x = a \to (B \subseteq ℂ \leftrightarrow ⦋ a / x ⦌ B \subseteq ℂ)$
41	39 40	rspc	$⊢ a \in A \to (\forall x \in A B \subseteq ℂ \to ⦋ a / x ⦌ B \subseteq ℂ)$
42	36 37 41	sylc	$⊢ ((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land a \in A) \to ⦋ a / x ⦌ B \subseteq ℂ$
43	4	ad2antrr	$⊢ ((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land a \in A) \to C \in ℂ$
44		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
45	35 42 43 44	ellimc2	$⊢ ((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land a \in A) \to (y \in (({F ↾}_{⦋ a / x ⦌ B}) {lim}_{ℂ} C) \leftrightarrow (y \in ℂ \land \forall u \in TopOpen (ℂ_{fld}) (y \in u \to \exists k \in TopOpen (ℂ_{fld}) (C \in k \land ({F ↾}_{⦋ a / x ⦌ B}) [k \cap (⦋ a / x ⦌ B ∖ \{C\})] \subseteq u))))$
46	45	adantlr	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land a \in A) \to (y \in (({F ↾}_{⦋ a / x ⦌ B}) {lim}_{ℂ} C) \leftrightarrow (y \in ℂ \land \forall u \in TopOpen (ℂ_{fld}) (y \in u \to \exists k \in TopOpen (ℂ_{fld}) (C \in k \land ({F ↾}_{⦋ a / x ⦌ B}) [k \cap (⦋ a / x ⦌ B ∖ \{C\})] \subseteq u))))$
47	28 46	mpbid	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land a \in A) \to (y \in ℂ \land \forall u \in TopOpen (ℂ_{fld}) (y \in u \to \exists k \in TopOpen (ℂ_{fld}) (C \in k \land ({F ↾}_{⦋ a / x ⦌ B}) [k \cap (⦋ a / x ⦌ B ∖ \{C\})] \subseteq u)))$
48	47	simprd	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land a \in A) \to \forall u \in TopOpen (ℂ_{fld}) (y \in u \to \exists k \in TopOpen (ℂ_{fld}) (C \in k \land ({F ↾}_{⦋ a / x ⦌ B}) [k \cap (⦋ a / x ⦌ B ∖ \{C\})] \subseteq u))$
49		simplrl	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land a \in A) \to u \in TopOpen (ℂ_{fld})$
50		simplrr	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land a \in A) \to y \in u$
51		rsp	$⊢ \forall u \in TopOpen (ℂ_{fld}) (y \in u \to \exists k \in TopOpen (ℂ_{fld}) (C \in k \land ({F ↾}_{⦋ a / x ⦌ B}) [k \cap (⦋ a / x ⦌ B ∖ \{C\})] \subseteq u)) \to (u \in TopOpen (ℂ_{fld}) \to (y \in u \to \exists k \in TopOpen (ℂ_{fld}) (C \in k \land ({F ↾}_{⦋ a / x ⦌ B}) [k \cap (⦋ a / x ⦌ B ∖ \{C\})] \subseteq u)))$
52	48 49 50 51	syl3c	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land a \in A) \to \exists k \in TopOpen (ℂ_{fld}) (C \in k \land ({F ↾}_{⦋ a / x ⦌ B}) [k \cap (⦋ a / x ⦌ B ∖ \{C\})] \subseteq u)$
53	52	ralrimiva	$⊢ ((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \to \forall a \in A \exists k \in TopOpen (ℂ_{fld}) (C \in k \land ({F ↾}_{⦋ a / x ⦌ B}) [k \cap (⦋ a / x ⦌ B ∖ \{C\})] \subseteq u)$
54		nfv	$⊢ Ⅎ a \exists k \in TopOpen (ℂ_{fld}) (C \in k \land ({F ↾}_{B}) [k \cap (B ∖ \{C\})] \subseteq u)$
55		nfcv	$⊢ \underline{Ⅎ} x TopOpen (ℂ_{fld})$
56		nfv	$⊢ Ⅎ x C \in k$
57		nfcv	$⊢ \underline{Ⅎ} x k$
58		nfcv	$⊢ \underline{Ⅎ} x \{C\}$
59	17 58	nfdif	$⊢ \underline{Ⅎ} x (⦋ a / x ⦌ B ∖ \{C\})$
60	57 59	nfin	$⊢ \underline{Ⅎ} x (k \cap (⦋ a / x ⦌ B ∖ \{C\}))$
61	18 60	nfima	$⊢ \underline{Ⅎ} x ({F ↾}_{⦋ a / x ⦌ B}) [k \cap (⦋ a / x ⦌ B ∖ \{C\})]$
62		nfcv	$⊢ \underline{Ⅎ} x u$
63	61 62	nfss	$⊢ Ⅎ x ({F ↾}_{⦋ a / x ⦌ B}) [k \cap (⦋ a / x ⦌ B ∖ \{C\})] \subseteq u$
64	56 63	nfan	$⊢ Ⅎ x (C \in k \land ({F ↾}_{⦋ a / x ⦌ B}) [k \cap (⦋ a / x ⦌ B ∖ \{C\})] \subseteq u)$
65	55 64	nfrexw	$⊢ Ⅎ x \exists k \in TopOpen (ℂ_{fld}) (C \in k \land ({F ↾}_{⦋ a / x ⦌ B}) [k \cap (⦋ a / x ⦌ B ∖ \{C\})] \subseteq u)$
66	23	difeq1d	$⊢ x = a \to B ∖ \{C\} = ⦋ a / x ⦌ B ∖ \{C\}$
67	66	ineq2d	$⊢ x = a \to k \cap (B ∖ \{C\}) = k \cap (⦋ a / x ⦌ B ∖ \{C\})$
68	24 67	imaeq12d	$⊢ x = a \to ({F ↾}_{B}) [k \cap (B ∖ \{C\})] = ({F ↾}_{⦋ a / x ⦌ B}) [k \cap (⦋ a / x ⦌ B ∖ \{C\})]$
69	68	sseq1d	$⊢ x = a \to (({F ↾}_{B}) [k \cap (B ∖ \{C\})] \subseteq u \leftrightarrow ({F ↾}_{⦋ a / x ⦌ B}) [k \cap (⦋ a / x ⦌ B ∖ \{C\})] \subseteq u)$
70	69	anbi2d	$⊢ x = a \to ((C \in k \land ({F ↾}_{B}) [k \cap (B ∖ \{C\})] \subseteq u) \leftrightarrow (C \in k \land ({F ↾}_{⦋ a / x ⦌ B}) [k \cap (⦋ a / x ⦌ B ∖ \{C\})] \subseteq u))$
71	70	rexbidv	$⊢ x = a \to (\exists k \in TopOpen (ℂ_{fld}) (C \in k \land ({F ↾}_{B}) [k \cap (B ∖ \{C\})] \subseteq u) \leftrightarrow \exists k \in TopOpen (ℂ_{fld}) (C \in k \land ({F ↾}_{⦋ a / x ⦌ B}) [k \cap (⦋ a / x ⦌ B ∖ \{C\})] \subseteq u))$
72	54 65 71	cbvralw	$⊢ \forall x \in A \exists k \in TopOpen (ℂ_{fld}) (C \in k \land ({F ↾}_{B}) [k \cap (B ∖ \{C\})] \subseteq u) \leftrightarrow \forall a \in A \exists k \in TopOpen (ℂ_{fld}) (C \in k \land ({F ↾}_{⦋ a / x ⦌ B}) [k \cap (⦋ a / x ⦌ B ∖ \{C\})] \subseteq u)$
73	53 72	sylibr	$⊢ ((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \to \forall x \in A \exists k \in TopOpen (ℂ_{fld}) (C \in k \land ({F ↾}_{B}) [k \cap (B ∖ \{C\})] \subseteq u)$
74		eleq2	$⊢ k = g (x) \to (C \in k \leftrightarrow C \in g (x))$
75		ineq1	$⊢ k = g (x) \to k \cap (B ∖ \{C\}) = g (x) \cap (B ∖ \{C\})$
76	75	imaeq2d	$⊢ k = g (x) \to ({F ↾}_{B}) [k \cap (B ∖ \{C\})] = ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})]$
77	76	sseq1d	$⊢ k = g (x) \to (({F ↾}_{B}) [k \cap (B ∖ \{C\})] \subseteq u \leftrightarrow ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u)$
78	74 77	anbi12d	$⊢ k = g (x) \to ((C \in k \land ({F ↾}_{B}) [k \cap (B ∖ \{C\})] \subseteq u) \leftrightarrow (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))$
79	78	ac6sfi	$⊢ (A \in Fin \land \forall x \in A \exists k \in TopOpen (ℂ_{fld}) (C \in k \land ({F ↾}_{B}) [k \cap (B ∖ \{C\})] \subseteq u)) \to \exists g (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))$
80	14 73 79	syl2anc	$⊢ ((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \to \exists g (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))$
81	44	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
82		frn	$⊢ g : A ⟶ TopOpen (ℂ_{fld}) \to ran g \subseteq TopOpen (ℂ_{fld})$
83	82	ad2antrl	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))) \to ran g \subseteq TopOpen (ℂ_{fld})$
84	14	adantr	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))) \to A \in Fin$
85		ffn	$⊢ g : A ⟶ TopOpen (ℂ_{fld}) \to g Fn A$
86	85	ad2antrl	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))) \to g Fn A$
87		dffn4	$⊢ g Fn A \leftrightarrow g : A \underset{onto}{⟶} ran g$
88	86 87	sylib	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))) \to g : A \underset{onto}{⟶} ran g$
89		fofi	$⊢ (A \in Fin \land g : A \underset{onto}{⟶} ran g) \to ran g \in Fin$
90	84 88 89	syl2anc	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))) \to ran g \in Fin$
91		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
92	91	rintopn	$⊢ (TopOpen (ℂ_{fld}) \in Top \land ran g \subseteq TopOpen (ℂ_{fld}) \land ran g \in Fin) \to ℂ \cap ⋂ ran g \in TopOpen (ℂ_{fld})$
93	81 83 90 92	mp3an2i	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))) \to ℂ \cap ⋂ ran g \in TopOpen (ℂ_{fld})$
94	4	adantr	$⊢ (φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \to C \in ℂ$
95	94	ad2antrr	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))) \to C \in ℂ$
96		simpl	$⊢ (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u) \to C \in g (x)$
97	96	ralimi	$⊢ \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u) \to \forall x \in A C \in g (x)$
98	97	ad2antll	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))) \to \forall x \in A C \in g (x)$
99		eleq2	$⊢ z = g (x) \to (C \in z \leftrightarrow C \in g (x))$
100	99	ralrn	$⊢ g Fn A \to (\forall z \in ran g C \in z \leftrightarrow \forall x \in A C \in g (x))$
101	86 100	syl	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))) \to (\forall z \in ran g C \in z \leftrightarrow \forall x \in A C \in g (x))$
102	98 101	mpbird	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))) \to \forall z \in ran g C \in z$
103		elrint	$⊢ C \in (ℂ \cap ⋂ ran g) \leftrightarrow (C \in ℂ \land \forall z \in ran g C \in z)$
104	95 102 103	sylanbrc	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))) \to C \in (ℂ \cap ⋂ ran g)$
105		indifcom	$⊢ (ℂ \cap ⋂ ran g) \cap (⋃_{x \in A} B ∖ \{C\}) = ⋃_{x \in A} B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})$
106		iunin1	$⊢ ⋃_{x \in A} (B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})) = ⋃_{x \in A} B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})$
107	105 106	eqtr4i	$⊢ (ℂ \cap ⋂ ran g) \cap (⋃_{x \in A} B ∖ \{C\}) = ⋃_{x \in A} (B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\}))$
108	107	imaeq2i	$⊢ F [(ℂ \cap ⋂ ran g) \cap (⋃_{x \in A} B ∖ \{C\})] = F [⋃_{x \in A} (B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\}))]$
109		imaiun	$⊢ F [⋃_{x \in A} (B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\}))] = ⋃_{x \in A} F [B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})]$
110	108 109	eqtri	$⊢ F [(ℂ \cap ⋂ ran g) \cap (⋃_{x \in A} B ∖ \{C\})] = ⋃_{x \in A} F [B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})]$
111		inss2	$⊢ ℂ \cap ⋂ ran g \subseteq ⋂ ran g$
112		fnfvelrn	$⊢ (g Fn A \land x \in A) \to g (x) \in ran g$
113	85 112	sylan	$⊢ (g : A ⟶ TopOpen (ℂ_{fld}) \land x \in A) \to g (x) \in ran g$
114		intss1	$⊢ g (x) \in ran g \to ⋂ ran g \subseteq g (x)$
115	113 114	syl	$⊢ (g : A ⟶ TopOpen (ℂ_{fld}) \land x \in A) \to ⋂ ran g \subseteq g (x)$
116	111 115	sstrid	$⊢ (g : A ⟶ TopOpen (ℂ_{fld}) \land x \in A) \to ℂ \cap ⋂ ran g \subseteq g (x)$
117	116	ssdifd	$⊢ (g : A ⟶ TopOpen (ℂ_{fld}) \land x \in A) \to (ℂ \cap ⋂ ran g) ∖ \{C\} \subseteq g (x) ∖ \{C\}$
118		sslin	$⊢ (ℂ \cap ⋂ ran g) ∖ \{C\} \subseteq g (x) ∖ \{C\} \to B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\}) \subseteq B \cap (g (x) ∖ \{C\})$
119		imass2	$⊢ B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\}) \subseteq B \cap (g (x) ∖ \{C\}) \to F [B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})] \subseteq F [B \cap (g (x) ∖ \{C\})]$
120	117 118 119	3syl	$⊢ (g : A ⟶ TopOpen (ℂ_{fld}) \land x \in A) \to F [B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})] \subseteq F [B \cap (g (x) ∖ \{C\})]$
121		indifcom	$⊢ g (x) \cap (B ∖ \{C\}) = B \cap (g (x) ∖ \{C\})$
122	121	imaeq2i	$⊢ ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] = ({F ↾}_{B}) [B \cap (g (x) ∖ \{C\})]$
123		inss1	$⊢ B \cap (g (x) ∖ \{C\}) \subseteq B$
124		resima2	$⊢ B \cap (g (x) ∖ \{C\}) \subseteq B \to ({F ↾}_{B}) [B \cap (g (x) ∖ \{C\})] = F [B \cap (g (x) ∖ \{C\})]$
125	123 124	ax-mp	$⊢ ({F ↾}_{B}) [B \cap (g (x) ∖ \{C\})] = F [B \cap (g (x) ∖ \{C\})]$
126	122 125	eqtri	$⊢ ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] = F [B \cap (g (x) ∖ \{C\})]$
127	120 126	sseqtrrdi	$⊢ (g : A ⟶ TopOpen (ℂ_{fld}) \land x \in A) \to F [B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})] \subseteq ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})]$
128		sstr2	$⊢ F [B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})] \subseteq ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \to (({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u \to F [B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})] \subseteq u)$
129	127 128	syl	$⊢ (g : A ⟶ TopOpen (ℂ_{fld}) \land x \in A) \to (({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u \to F [B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})] \subseteq u)$
130	129	adantld	$⊢ (g : A ⟶ TopOpen (ℂ_{fld}) \land x \in A) \to ((C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u) \to F [B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})] \subseteq u)$
131	130	ralimdva	$⊢ g : A ⟶ TopOpen (ℂ_{fld}) \to (\forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u) \to \forall x \in A F [B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})] \subseteq u)$
132	131	imp	$⊢ (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u)) \to \forall x \in A F [B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})] \subseteq u$
133	132	adantl	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))) \to \forall x \in A F [B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})] \subseteq u$
134		iunss	$⊢ ⋃_{x \in A} F [B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})] \subseteq u \leftrightarrow \forall x \in A F [B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})] \subseteq u$
135	133 134	sylibr	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))) \to ⋃_{x \in A} F [B \cap ((ℂ \cap ⋂ ran g) ∖ \{C\})] \subseteq u$
136	110 135	eqsstrid	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))) \to F [(ℂ \cap ⋂ ran g) \cap (⋃_{x \in A} B ∖ \{C\})] \subseteq u$
137		eleq2	$⊢ v = ℂ \cap ⋂ ran g \to (C \in v \leftrightarrow C \in (ℂ \cap ⋂ ran g))$
138		ineq1	$⊢ v = ℂ \cap ⋂ ran g \to v \cap (⋃_{x \in A} B ∖ \{C\}) = (ℂ \cap ⋂ ran g) \cap (⋃_{x \in A} B ∖ \{C\})$
139	138	imaeq2d	$⊢ v = ℂ \cap ⋂ ran g \to F [v \cap (⋃_{x \in A} B ∖ \{C\})] = F [(ℂ \cap ⋂ ran g) \cap (⋃_{x \in A} B ∖ \{C\})]$
140	139	sseq1d	$⊢ v = ℂ \cap ⋂ ran g \to (F [v \cap (⋃_{x \in A} B ∖ \{C\})] \subseteq u \leftrightarrow F [(ℂ \cap ⋂ ran g) \cap (⋃_{x \in A} B ∖ \{C\})] \subseteq u)$
141	137 140	anbi12d	$⊢ v = ℂ \cap ⋂ ran g \to ((C \in v \land F [v \cap (⋃_{x \in A} B ∖ \{C\})] \subseteq u) \leftrightarrow (C \in (ℂ \cap ⋂ ran g) \land F [(ℂ \cap ⋂ ran g) \cap (⋃_{x \in A} B ∖ \{C\})] \subseteq u))$
142	141	rspcev	$⊢ (ℂ \cap ⋂ ran g \in TopOpen (ℂ_{fld}) \land (C \in (ℂ \cap ⋂ ran g) \land F [(ℂ \cap ⋂ ran g) \cap (⋃_{x \in A} B ∖ \{C\})] \subseteq u)) \to \exists v \in TopOpen (ℂ_{fld}) (C \in v \land F [v \cap (⋃_{x \in A} B ∖ \{C\})] \subseteq u)$
143	93 104 136 142	syl12anc	$⊢ (((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \land (g : A ⟶ TopOpen (ℂ_{fld}) \land \forall x \in A (C \in g (x) \land ({F ↾}_{B}) [g (x) \cap (B ∖ \{C\})] \subseteq u))) \to \exists v \in TopOpen (ℂ_{fld}) (C \in v \land F [v \cap (⋃_{x \in A} B ∖ \{C\})] \subseteq u)$
144	80 143	exlimddv	$⊢ ((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land (u \in TopOpen (ℂ_{fld}) \land y \in u)) \to \exists v \in TopOpen (ℂ_{fld}) (C \in v \land F [v \cap (⋃_{x \in A} B ∖ \{C\})] \subseteq u)$
145	144	expr	$⊢ ((φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \land u \in TopOpen (ℂ_{fld})) \to (y \in u \to \exists v \in TopOpen (ℂ_{fld}) (C \in v \land F [v \cap (⋃_{x \in A} B ∖ \{C\})] \subseteq u))$
146	145	ralrimiva	$⊢ (φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \to \forall u \in TopOpen (ℂ_{fld}) (y \in u \to \exists v \in TopOpen (ℂ_{fld}) (C \in v \land F [v \cap (⋃_{x \in A} B ∖ \{C\})] \subseteq u))$
147	3	adantr	$⊢ (φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \to F : ⋃_{x \in A} B ⟶ ℂ$
148		iunss	$⊢ ⋃_{x \in A} B \subseteq ℂ \leftrightarrow \forall x \in A B \subseteq ℂ$
149	2 148	sylibr	$⊢ φ \to ⋃_{x \in A} B \subseteq ℂ$
150	149	adantr	$⊢ (φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \to ⋃_{x \in A} B \subseteq ℂ$
151	147 150 94 44	ellimc2	$⊢ (φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \to (y \in (F {lim}_{ℂ} C) \leftrightarrow (y \in ℂ \land \forall u \in TopOpen (ℂ_{fld}) (y \in u \to \exists v \in TopOpen (ℂ_{fld}) (C \in v \land F [v \cap (⋃_{x \in A} B ∖ \{C\})] \subseteq u))))$
152	13 146 151	mpbir2and	$⊢ (φ \land (y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C))) \to y \in (F {lim}_{ℂ} C)$
153	152	ex	$⊢ φ \to ((y \in ℂ \land \forall x \in A y \in (({F ↾}_{B}) {lim}_{ℂ} C)) \to y \in (F {lim}_{ℂ} C))$
154	12 153	biimtrid	$⊢ φ \to (y \in (ℂ \cap ⋂_{x \in A} (({F ↾}_{B}) {lim}_{ℂ} C)) \to y \in (F {lim}_{ℂ} C))$
155	154	ssrdv	$⊢ φ \to ℂ \cap ⋂_{x \in A} (({F ↾}_{B}) {lim}_{ℂ} C) \subseteq F {lim}_{ℂ} C$
156	11 155	eqssd	$⊢ φ \to F {lim}_{ℂ} C = ℂ \cap ⋂_{x \in A} (({F ↾}_{B}) {lim}_{ℂ} C)$

Metamath Proof Explorer

Theorem limciun

Proof