filuni

Description: The union of a nonempty set of filters with a common base and closed under pairwise union is a filter. (Contributed by Mario Carneiro, 28-Nov-2013) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	filuni	$⊢ (F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \to ⋃ F \in Fil (X)$

Proof

Step	Hyp	Ref	Expression
1		eluni2	$⊢ x \in ⋃ F \leftrightarrow \exists f \in F x \in f$
2		ssel2	$⊢ (F \subseteq Fil (X) \land f \in F) \to f \in Fil (X)$
3		filelss	$⊢ (f \in Fil (X) \land x \in f) \to x \subseteq X$
4	3	ex	$⊢ f \in Fil (X) \to (x \in f \to x \subseteq X)$
5	2 4	syl	$⊢ (F \subseteq Fil (X) \land f \in F) \to (x \in f \to x \subseteq X)$
6	5	rexlimdva	$⊢ F \subseteq Fil (X) \to (\exists f \in F x \in f \to x \subseteq X)$
7	6	3ad2ant1	$⊢ (F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \to (\exists f \in F x \in f \to x \subseteq X)$
8	1 7	biimtrid	$⊢ (F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \to (x \in ⋃ F \to x \subseteq X)$
9	8	pm4.71rd	$⊢ (F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \to (x \in ⋃ F \leftrightarrow (x \subseteq X \land x \in ⋃ F))$
10		ssn0	$⊢ (F \subseteq Fil (X) \land F \neq \emptyset) \to Fil (X) \neq \emptyset$
11		fvprc	$⊢ \neg X \in V \to Fil (X) = \emptyset$
12	11	necon1ai	$⊢ Fil (X) \neq \emptyset \to X \in V$
13	10 12	syl	$⊢ (F \subseteq Fil (X) \land F \neq \emptyset) \to X \in V$
14	13	3adant3	$⊢ (F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \to X \in V$
15		filtop	$⊢ f \in Fil (X) \to X \in f$
16	2 15	syl	$⊢ (F \subseteq Fil (X) \land f \in F) \to X \in f$
17	16	a1d	$⊢ (F \subseteq Fil (X) \land f \in F) \to (\forall g \in F f \cup g \in F \to X \in f)$
18	17	ralimdva	$⊢ F \subseteq Fil (X) \to (\forall f \in F \forall g \in F f \cup g \in F \to \forall f \in F X \in f)$
19		r19.2z	$⊢ (F \neq \emptyset \land \forall f \in F X \in f) \to \exists f \in F X \in f$
20	19	ex	$⊢ F \neq \emptyset \to (\forall f \in F X \in f \to \exists f \in F X \in f)$
21	18 20	sylan9	$⊢ (F \subseteq Fil (X) \land F \neq \emptyset) \to (\forall f \in F \forall g \in F f \cup g \in F \to \exists f \in F X \in f)$
22	21	3impia	$⊢ (F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \to \exists f \in F X \in f$
23		eluni2	$⊢ X \in ⋃ F \leftrightarrow \exists f \in F X \in f$
24	22 23	sylibr	$⊢ (F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \to X \in ⋃ F$
25		sbcel1v	$⊢ \underset{˙}{[} X / x \underset{˙}{]} x \in ⋃ F \leftrightarrow X \in ⋃ F$
26	24 25	sylibr	$⊢ (F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \to \underset{˙}{[} X / x \underset{˙}{]} x \in ⋃ F$
27		0nelfil	$⊢ f \in Fil (X) \to \neg \emptyset \in f$
28	2 27	syl	$⊢ (F \subseteq Fil (X) \land f \in F) \to \neg \emptyset \in f$
29	28	ralrimiva	$⊢ F \subseteq Fil (X) \to \forall f \in F \neg \emptyset \in f$
30	29	3ad2ant1	$⊢ (F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \to \forall f \in F \neg \emptyset \in f$
31		sbcel1v	$⊢ \underset{˙}{[} \emptyset / x \underset{˙}{]} x \in ⋃ F \leftrightarrow \emptyset \in ⋃ F$
32		eluni2	$⊢ \emptyset \in ⋃ F \leftrightarrow \exists f \in F \emptyset \in f$
33	31 32	bitri	$⊢ \underset{˙}{[} \emptyset / x \underset{˙}{]} x \in ⋃ F \leftrightarrow \exists f \in F \emptyset \in f$
34	33	notbii	$⊢ \neg \underset{˙}{[} \emptyset / x \underset{˙}{]} x \in ⋃ F \leftrightarrow \neg \exists f \in F \emptyset \in f$
35		ralnex	$⊢ \forall f \in F \neg \emptyset \in f \leftrightarrow \neg \exists f \in F \emptyset \in f$
36	34 35	bitr4i	$⊢ \neg \underset{˙}{[} \emptyset / x \underset{˙}{]} x \in ⋃ F \leftrightarrow \forall f \in F \neg \emptyset \in f$
37	30 36	sylibr	$⊢ (F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \to \neg \underset{˙}{[} \emptyset / x \underset{˙}{]} x \in ⋃ F$
38		simp13	$⊢ ((F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \land y \subseteq X \land x \subseteq y) \to \forall f \in F \forall g \in F f \cup g \in F$
39		r19.29	$⊢ (\forall f \in F \forall g \in F f \cup g \in F \land \exists f \in F x \in f) \to \exists f \in F (\forall g \in F f \cup g \in F \land x \in f)$
40	39	ex	$⊢ \forall f \in F \forall g \in F f \cup g \in F \to (\exists f \in F x \in f \to \exists f \in F (\forall g \in F f \cup g \in F \land x \in f))$
41	38 40	syl	$⊢ ((F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \land y \subseteq X \land x \subseteq y) \to (\exists f \in F x \in f \to \exists f \in F (\forall g \in F f \cup g \in F \land x \in f))$
42		simp1	$⊢ (F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \to F \subseteq Fil (X)$
43		simp1	$⊢ (F \subseteq Fil (X) \land y \subseteq X \land x \subseteq y) \to F \subseteq Fil (X)$
44		simpl	$⊢ (f \in F \land (\forall g \in F f \cup g \in F \land x \in f)) \to f \in F$
45	43 44 2	syl2an	$⊢ ((F \subseteq Fil (X) \land y \subseteq X \land x \subseteq y) \land (f \in F \land (\forall g \in F f \cup g \in F \land x \in f))) \to f \in Fil (X)$
46		simprrr	$⊢ ((F \subseteq Fil (X) \land y \subseteq X \land x \subseteq y) \land (f \in F \land (\forall g \in F f \cup g \in F \land x \in f))) \to x \in f$
47		simpl2	$⊢ ((F \subseteq Fil (X) \land y \subseteq X \land x \subseteq y) \land (f \in F \land (\forall g \in F f \cup g \in F \land x \in f))) \to y \subseteq X$
48		simpl3	$⊢ ((F \subseteq Fil (X) \land y \subseteq X \land x \subseteq y) \land (f \in F \land (\forall g \in F f \cup g \in F \land x \in f))) \to x \subseteq y$
49		filss	$⊢ (f \in Fil (X) \land (x \in f \land y \subseteq X \land x \subseteq y)) \to y \in f$
50	45 46 47 48 49	syl13anc	$⊢ ((F \subseteq Fil (X) \land y \subseteq X \land x \subseteq y) \land (f \in F \land (\forall g \in F f \cup g \in F \land x \in f))) \to y \in f$
51	50	expr	$⊢ ((F \subseteq Fil (X) \land y \subseteq X \land x \subseteq y) \land f \in F) \to ((\forall g \in F f \cup g \in F \land x \in f) \to y \in f)$
52	51	reximdva	$⊢ (F \subseteq Fil (X) \land y \subseteq X \land x \subseteq y) \to (\exists f \in F (\forall g \in F f \cup g \in F \land x \in f) \to \exists f \in F y \in f)$
53	42 52	syl3an1	$⊢ ((F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \land y \subseteq X \land x \subseteq y) \to (\exists f \in F (\forall g \in F f \cup g \in F \land x \in f) \to \exists f \in F y \in f)$
54	41 53	syld	$⊢ ((F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \land y \subseteq X \land x \subseteq y) \to (\exists f \in F x \in f \to \exists f \in F y \in f)$
55		sbcel1v	$⊢ \underset{˙}{[} x / x \underset{˙}{]} x \in ⋃ F \leftrightarrow x \in ⋃ F$
56	55 1	bitri	$⊢ \underset{˙}{[} x / x \underset{˙}{]} x \in ⋃ F \leftrightarrow \exists f \in F x \in f$
57		sbcel1v	$⊢ \underset{˙}{[} y / x \underset{˙}{]} x \in ⋃ F \leftrightarrow y \in ⋃ F$
58		eluni2	$⊢ y \in ⋃ F \leftrightarrow \exists f \in F y \in f$
59	57 58	bitri	$⊢ \underset{˙}{[} y / x \underset{˙}{]} x \in ⋃ F \leftrightarrow \exists f \in F y \in f$
60	54 56 59	3imtr4g	$⊢ ((F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \land y \subseteq X \land x \subseteq y) \to (\underset{˙}{[} x / x \underset{˙}{]} x \in ⋃ F \to \underset{˙}{[} y / x \underset{˙}{]} x \in ⋃ F)$
61		simp13	$⊢ ((F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \land y \subseteq X \land x \subseteq X) \to \forall f \in F \forall g \in F f \cup g \in F$
62		r19.29	$⊢ (\forall f \in F \forall g \in F f \cup g \in F \land \exists f \in F y \in f) \to \exists f \in F (\forall g \in F f \cup g \in F \land y \in f)$
63	62	ex	$⊢ \forall f \in F \forall g \in F f \cup g \in F \to (\exists f \in F y \in f \to \exists f \in F (\forall g \in F f \cup g \in F \land y \in f))$
64	61 63	syl	$⊢ ((F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \land y \subseteq X \land x \subseteq X) \to (\exists f \in F y \in f \to \exists f \in F (\forall g \in F f \cup g \in F \land y \in f))$
65		simp11	$⊢ ((F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \land y \subseteq X \land x \subseteq X) \to F \subseteq Fil (X)$
66		r19.29	$⊢ (\forall g \in F f \cup g \in F \land \exists g \in F x \in g) \to \exists g \in F (f \cup g \in F \land x \in g)$
67	66	ex	$⊢ \forall g \in F f \cup g \in F \to (\exists g \in F x \in g \to \exists g \in F (f \cup g \in F \land x \in g))$
68		elun1	$⊢ y \in f \to y \in (f \cup g)$
69		elun2	$⊢ x \in g \to x \in (f \cup g)$
70	68 69	anim12i	$⊢ (y \in f \land x \in g) \to (y \in (f \cup g) \land x \in (f \cup g))$
71		eleq2	$⊢ h = f \cup g \to (y \in h \leftrightarrow y \in (f \cup g))$
72		eleq2	$⊢ h = f \cup g \to (x \in h \leftrightarrow x \in (f \cup g))$
73	71 72	anbi12d	$⊢ h = f \cup g \to ((y \in h \land x \in h) \leftrightarrow (y \in (f \cup g) \land x \in (f \cup g)))$
74	73	rspcev	$⊢ (f \cup g \in F \land (y \in (f \cup g) \land x \in (f \cup g))) \to \exists h \in F (y \in h \land x \in h)$
75	70 74	sylan2	$⊢ (f \cup g \in F \land (y \in f \land x \in g)) \to \exists h \in F (y \in h \land x \in h)$
76	75	an12s	$⊢ (y \in f \land (f \cup g \in F \land x \in g)) \to \exists h \in F (y \in h \land x \in h)$
77	76	ex	$⊢ y \in f \to ((f \cup g \in F \land x \in g) \to \exists h \in F (y \in h \land x \in h))$
78	77	ad2antlr	$⊢ ((f \in F \land y \in f) \land g \in F) \to ((f \cup g \in F \land x \in g) \to \exists h \in F (y \in h \land x \in h))$
79	78	rexlimdva	$⊢ (f \in F \land y \in f) \to (\exists g \in F (f \cup g \in F \land x \in g) \to \exists h \in F (y \in h \land x \in h))$
80	67 79	syl9r	$⊢ (f \in F \land y \in f) \to (\forall g \in F f \cup g \in F \to (\exists g \in F x \in g \to \exists h \in F (y \in h \land x \in h)))$
81	80	impr	$⊢ (f \in F \land (y \in f \land \forall g \in F f \cup g \in F)) \to (\exists g \in F x \in g \to \exists h \in F (y \in h \land x \in h))$
82	81	ancom2s	$⊢ (f \in F \land (\forall g \in F f \cup g \in F \land y \in f)) \to (\exists g \in F x \in g \to \exists h \in F (y \in h \land x \in h))$
83	82	rexlimiva	$⊢ \exists f \in F (\forall g \in F f \cup g \in F \land y \in f) \to (\exists g \in F x \in g \to \exists h \in F (y \in h \land x \in h))$
84	83	imp	$⊢ (\exists f \in F (\forall g \in F f \cup g \in F \land y \in f) \land \exists g \in F x \in g) \to \exists h \in F (y \in h \land x \in h)$
85		ssel2	$⊢ (F \subseteq Fil (X) \land h \in F) \to h \in Fil (X)$
86		filin	$⊢ (h \in Fil (X) \land y \in h \land x \in h) \to y \cap x \in h$
87	86	3expib	$⊢ h \in Fil (X) \to ((y \in h \land x \in h) \to y \cap x \in h)$
88	85 87	syl	$⊢ (F \subseteq Fil (X) \land h \in F) \to ((y \in h \land x \in h) \to y \cap x \in h)$
89	88	reximdva	$⊢ F \subseteq Fil (X) \to (\exists h \in F (y \in h \land x \in h) \to \exists h \in F y \cap x \in h)$
90	65 84 89	syl2im	$⊢ ((F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \land y \subseteq X \land x \subseteq X) \to ((\exists f \in F (\forall g \in F f \cup g \in F \land y \in f) \land \exists g \in F x \in g) \to \exists h \in F y \cap x \in h)$
91	64 90	syland	$⊢ ((F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \land y \subseteq X \land x \subseteq X) \to ((\exists f \in F y \in f \land \exists g \in F x \in g) \to \exists h \in F y \cap x \in h)$
92		eluni2	$⊢ x \in ⋃ F \leftrightarrow \exists g \in F x \in g$
93	55 92	bitri	$⊢ \underset{˙}{[} x / x \underset{˙}{]} x \in ⋃ F \leftrightarrow \exists g \in F x \in g$
94	59 93	anbi12i	$⊢ (\underset{˙}{[} y / x \underset{˙}{]} x \in ⋃ F \land \underset{˙}{[} x / x \underset{˙}{]} x \in ⋃ F) \leftrightarrow (\exists f \in F y \in f \land \exists g \in F x \in g)$
95		sbcel1v	$⊢ \underset{˙}{[} (y \cap x) / x \underset{˙}{]} x \in ⋃ F \leftrightarrow y \cap x \in ⋃ F$
96		eluni2	$⊢ y \cap x \in ⋃ F \leftrightarrow \exists h \in F y \cap x \in h$
97	95 96	bitri	$⊢ \underset{˙}{[} (y \cap x) / x \underset{˙}{]} x \in ⋃ F \leftrightarrow \exists h \in F y \cap x \in h$
98	91 94 97	3imtr4g	$⊢ ((F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \land y \subseteq X \land x \subseteq X) \to ((\underset{˙}{[} y / x \underset{˙}{]} x \in ⋃ F \land \underset{˙}{[} x / x \underset{˙}{]} x \in ⋃ F) \to \underset{˙}{[} (y \cap x) / x \underset{˙}{]} x \in ⋃ F)$
99	9 14 26 37 60 98	isfild	$⊢ (F \subseteq Fil (X) \land F \neq \emptyset \land \forall f \in F \forall g \in F f \cup g \in F) \to ⋃ F \in Fil (X)$

Metamath Proof Explorer

Theorem filuni

Proof