fbun

Description: A necessary and sufficient condition for the union of two filter bases to also be a filter base. (Contributed by Mario Carneiro, 28-Nov-2013) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	fbun	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (F \cup G \in fBas (X) \leftrightarrow \forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y)$

Proof

Step	Hyp	Ref	Expression
1		elun1	$⊢ x \in F \to x \in (F \cup G)$
2		elun2	$⊢ y \in G \to y \in (F \cup G)$
3	1 2	anim12i	$⊢ (x \in F \land y \in G) \to (x \in (F \cup G) \land y \in (F \cup G))$
4		fbasssin	$⊢ (F \cup G \in fBas (X) \land x \in (F \cup G) \land y \in (F \cup G)) \to \exists z \in (F \cup G) z \subseteq x \cap y$
5	4	3expb	$⊢ (F \cup G \in fBas (X) \land (x \in (F \cup G) \land y \in (F \cup G))) \to \exists z \in (F \cup G) z \subseteq x \cap y$
6	3 5	sylan2	$⊢ (F \cup G \in fBas (X) \land (x \in F \land y \in G)) \to \exists z \in (F \cup G) z \subseteq x \cap y$
7	6	ralrimivva	$⊢ F \cup G \in fBas (X) \to \forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y$
8		fbsspw	$⊢ F \in fBas (X) \to F \subseteq 𝒫 X$
9	8	adantr	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to F \subseteq 𝒫 X$
10		fbsspw	$⊢ G \in fBas (X) \to G \subseteq 𝒫 X$
11	10	adantl	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to G \subseteq 𝒫 X$
12	9 11	unssd	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to F \cup G \subseteq 𝒫 X$
13	12	a1d	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (\forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y \to F \cup G \subseteq 𝒫 X)$
14		ssun1	$⊢ F \subseteq F \cup G$
15		fbasne0	$⊢ F \in fBas (X) \to F \neq \emptyset$
16		ssn0	$⊢ (F \subseteq F \cup G \land F \neq \emptyset) \to F \cup G \neq \emptyset$
17	14 15 16	sylancr	$⊢ F \in fBas (X) \to F \cup G \neq \emptyset$
18	17	adantr	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to F \cup G \neq \emptyset$
19	18	a1d	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (\forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y \to F \cup G \neq \emptyset)$
20		0nelfb	$⊢ F \in fBas (X) \to \neg \emptyset \in F$
21		0nelfb	$⊢ G \in fBas (X) \to \neg \emptyset \in G$
22		df-nel	$⊢ \emptyset \notin (F \cup G) \leftrightarrow \neg \emptyset \in (F \cup G)$
23		elun	$⊢ \emptyset \in (F \cup G) \leftrightarrow (\emptyset \in F \lor \emptyset \in G)$
24	23	notbii	$⊢ \neg \emptyset \in (F \cup G) \leftrightarrow \neg (\emptyset \in F \lor \emptyset \in G)$
25		ioran	$⊢ \neg (\emptyset \in F \lor \emptyset \in G) \leftrightarrow (\neg \emptyset \in F \land \neg \emptyset \in G)$
26	22 24 25	3bitri	$⊢ \emptyset \notin (F \cup G) \leftrightarrow (\neg \emptyset \in F \land \neg \emptyset \in G)$
27	26	biimpri	$⊢ (\neg \emptyset \in F \land \neg \emptyset \in G) \to \emptyset \notin (F \cup G)$
28	20 21 27	syl2an	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to \emptyset \notin (F \cup G)$
29	28	a1d	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (\forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y \to \emptyset \notin (F \cup G))$
30		fbasssin	$⊢ (F \in fBas (X) \land x \in F \land y \in F) \to \exists z \in F z \subseteq x \cap y$
31		ssrexv	$⊢ F \subseteq F \cup G \to (\exists z \in F z \subseteq x \cap y \to \exists z \in (F \cup G) z \subseteq x \cap y)$
32	14 30 31	mpsyl	$⊢ (F \in fBas (X) \land x \in F \land y \in F) \to \exists z \in (F \cup G) z \subseteq x \cap y$
33	32	3expb	$⊢ (F \in fBas (X) \land (x \in F \land y \in F)) \to \exists z \in (F \cup G) z \subseteq x \cap y$
34	33	ralrimivva	$⊢ F \in fBas (X) \to \forall x \in F \forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y$
35	34	adantr	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to \forall x \in F \forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y$
36		pm3.2	$⊢ \forall x \in F \forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y \to (\forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y \to (\forall x \in F \forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y \land \forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y))$
37	35 36	syl	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (\forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y \to (\forall x \in F \forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y \land \forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y))$
38		r19.26	$⊢ \forall x \in F (\forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y \land \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y) \leftrightarrow (\forall x \in F \forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y \land \forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y)$
39		ralun	$⊢ (\forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y \land \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y) \to \forall y \in (F \cup G) \exists z \in (F \cup G) z \subseteq x \cap y$
40	39	ralimi	$⊢ \forall x \in F (\forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y \land \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y) \to \forall x \in F \forall y \in (F \cup G) \exists z \in (F \cup G) z \subseteq x \cap y$
41	38 40	sylbir	$⊢ (\forall x \in F \forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y \land \forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y) \to \forall x \in F \forall y \in (F \cup G) \exists z \in (F \cup G) z \subseteq x \cap y$
42	37 41	syl6	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (\forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y \to \forall x \in F \forall y \in (F \cup G) \exists z \in (F \cup G) z \subseteq x \cap y)$
43		ralcom	$⊢ \forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y \leftrightarrow \forall y \in G \forall x \in F \exists z \in (F \cup G) z \subseteq x \cap y$
44		ineq1	$⊢ x = w \to x \cap y = w \cap y$
45	44	sseq2d	$⊢ x = w \to (z \subseteq x \cap y \leftrightarrow z \subseteq w \cap y)$
46	45	rexbidv	$⊢ x = w \to (\exists z \in (F \cup G) z \subseteq x \cap y \leftrightarrow \exists z \in (F \cup G) z \subseteq w \cap y)$
47	46	cbvralvw	$⊢ \forall x \in F \exists z \in (F \cup G) z \subseteq x \cap y \leftrightarrow \forall w \in F \exists z \in (F \cup G) z \subseteq w \cap y$
48	47	ralbii	$⊢ \forall y \in G \forall x \in F \exists z \in (F \cup G) z \subseteq x \cap y \leftrightarrow \forall y \in G \forall w \in F \exists z \in (F \cup G) z \subseteq w \cap y$
49		ineq2	$⊢ y = x \to w \cap y = w \cap x$
50	49	sseq2d	$⊢ y = x \to (z \subseteq w \cap y \leftrightarrow z \subseteq w \cap x)$
51	50	rexbidv	$⊢ y = x \to (\exists z \in (F \cup G) z \subseteq w \cap y \leftrightarrow \exists z \in (F \cup G) z \subseteq w \cap x)$
52		ineq1	$⊢ w = y \to w \cap x = y \cap x$
53		incom	$⊢ y \cap x = x \cap y$
54	52 53	syl6eq	$⊢ w = y \to w \cap x = x \cap y$
55	54	sseq2d	$⊢ w = y \to (z \subseteq w \cap x \leftrightarrow z \subseteq x \cap y)$
56	55	rexbidv	$⊢ w = y \to (\exists z \in (F \cup G) z \subseteq w \cap x \leftrightarrow \exists z \in (F \cup G) z \subseteq x \cap y)$
57	51 56	cbvral2vw	$⊢ \forall y \in G \forall w \in F \exists z \in (F \cup G) z \subseteq w \cap y \leftrightarrow \forall x \in G \forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y$
58	43 48 57	3bitri	$⊢ \forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y \leftrightarrow \forall x \in G \forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y$
59	58	biimpi	$⊢ \forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y \to \forall x \in G \forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y$
60		ssun2	$⊢ G \subseteq F \cup G$
61		fbasssin	$⊢ (G \in fBas (X) \land x \in G \land y \in G) \to \exists z \in G z \subseteq x \cap y$
62		ssrexv	$⊢ G \subseteq F \cup G \to (\exists z \in G z \subseteq x \cap y \to \exists z \in (F \cup G) z \subseteq x \cap y)$
63	60 61 62	mpsyl	$⊢ (G \in fBas (X) \land x \in G \land y \in G) \to \exists z \in (F \cup G) z \subseteq x \cap y$
64	63	3expb	$⊢ (G \in fBas (X) \land (x \in G \land y \in G)) \to \exists z \in (F \cup G) z \subseteq x \cap y$
65	64	ralrimivva	$⊢ G \in fBas (X) \to \forall x \in G \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y$
66	65	adantl	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to \forall x \in G \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y$
67	59 66	anim12i	$⊢ (\forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y \land (F \in fBas (X) \land G \in fBas (X))) \to (\forall x \in G \forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y \land \forall x \in G \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y)$
68	67	expcom	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (\forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y \to (\forall x \in G \forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y \land \forall x \in G \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y))$
69		r19.26	$⊢ \forall x \in G (\forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y \land \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y) \leftrightarrow (\forall x \in G \forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y \land \forall x \in G \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y)$
70	39	ralimi	$⊢ \forall x \in G (\forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y \land \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y) \to \forall x \in G \forall y \in (F \cup G) \exists z \in (F \cup G) z \subseteq x \cap y$
71	69 70	sylbir	$⊢ (\forall x \in G \forall y \in F \exists z \in (F \cup G) z \subseteq x \cap y \land \forall x \in G \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y) \to \forall x \in G \forall y \in (F \cup G) \exists z \in (F \cup G) z \subseteq x \cap y$
72	68 71	syl6	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (\forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y \to \forall x \in G \forall y \in (F \cup G) \exists z \in (F \cup G) z \subseteq x \cap y)$
73	42 72	jcad	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (\forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y \to (\forall x \in F \forall y \in (F \cup G) \exists z \in (F \cup G) z \subseteq x \cap y \land \forall x \in G \forall y \in (F \cup G) \exists z \in (F \cup G) z \subseteq x \cap y))$
74		ralun	$⊢ (\forall x \in F \forall y \in (F \cup G) \exists z \in (F \cup G) z \subseteq x \cap y \land \forall x \in G \forall y \in (F \cup G) \exists z \in (F \cup G) z \subseteq x \cap y) \to \forall x \in (F \cup G) \forall y \in (F \cup G) \exists z \in (F \cup G) z \subseteq x \cap y$
75	73 74	syl6	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (\forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y \to \forall x \in (F \cup G) \forall y \in (F \cup G) \exists z \in (F \cup G) z \subseteq x \cap y)$
76	19 29 75	3jcad	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (\forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y \to (F \cup G \neq \emptyset \land \emptyset \notin (F \cup G) \land \forall x \in (F \cup G) \forall y \in (F \cup G) \exists z \in (F \cup G) z \subseteq x \cap y))$
77	13 76	jcad	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (\forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y \to (F \cup G \subseteq 𝒫 X \land (F \cup G \neq \emptyset \land \emptyset \notin (F \cup G) \land \forall x \in (F \cup G) \forall y \in (F \cup G) \exists z \in (F \cup G) z \subseteq x \cap y)))$
78		elfvdm	$⊢ F \in fBas (X) \to X \in dom fBas$
79	78	adantr	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to X \in dom fBas$
80		isfbas2	$⊢ X \in dom fBas \to (F \cup G \in fBas (X) \leftrightarrow (F \cup G \subseteq 𝒫 X \land (F \cup G \neq \emptyset \land \emptyset \notin (F \cup G) \land \forall x \in (F \cup G) \forall y \in (F \cup G) \exists z \in (F \cup G) z \subseteq x \cap y)))$
81	79 80	syl	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (F \cup G \in fBas (X) \leftrightarrow (F \cup G \subseteq 𝒫 X \land (F \cup G \neq \emptyset \land \emptyset \notin (F \cup G) \land \forall x \in (F \cup G) \forall y \in (F \cup G) \exists z \in (F \cup G) z \subseteq x \cap y)))$
82	77 81	sylibrd	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (\forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y \to F \cup G \in fBas (X))$
83	7 82	impbid2	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (F \cup G \in fBas (X) \leftrightarrow \forall x \in F \forall y \in G \exists z \in (F \cup G) z \subseteq x \cap y)$

Metamath Proof Explorer

Theorem fbun

Proof