tsmsfbas

Description: The collection of all sets of the form F ( z ) = { y e. S | z C_ y } , which can be read as the set of all finite subsets of A which contain z as a subset, for each finite subset z of A , form a filter base. (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	tsmsfbas.s	$⊢ S = 𝒫 A \cap Fin$
	tsmsfbas.f	$⊢ F = (z \in S ⟼ \{y \in S \| z \subseteq y\})$
	tsmsfbas.l	$⊢ L = ran F$
	tsmsfbas.a	$⊢ φ \to A \in W$
Assertion	tsmsfbas	$⊢ φ \to L \in fBas (S)$

Proof

Step	Hyp	Ref	Expression
1		tsmsfbas.s	$⊢ S = 𝒫 A \cap Fin$
2		tsmsfbas.f	$⊢ F = (z \in S ⟼ \{y \in S \| z \subseteq y\})$
3		tsmsfbas.l	$⊢ L = ran F$
4		tsmsfbas.a	$⊢ φ \to A \in W$
5		elex	$⊢ A \in W \to A \in V$
6		ssrab2	$⊢ \{y \in S \| z \subseteq y\} \subseteq S$
7		pwexg	$⊢ A \in V \to 𝒫 A \in V$
8		inex1g	$⊢ 𝒫 A \in V \to 𝒫 A \cap Fin \in V$
9	7 8	syl	$⊢ A \in V \to 𝒫 A \cap Fin \in V$
10	1 9	eqeltrid	$⊢ A \in V \to S \in V$
11	10	adantr	$⊢ (A \in V \land z \in S) \to S \in V$
12		elpw2g	$⊢ S \in V \to (\{y \in S \| z \subseteq y\} \in 𝒫 S \leftrightarrow \{y \in S \| z \subseteq y\} \subseteq S)$
13	11 12	syl	$⊢ (A \in V \land z \in S) \to (\{y \in S \| z \subseteq y\} \in 𝒫 S \leftrightarrow \{y \in S \| z \subseteq y\} \subseteq S)$
14	6 13	mpbiri	$⊢ (A \in V \land z \in S) \to \{y \in S \| z \subseteq y\} \in 𝒫 S$
15	14 2	fmptd	$⊢ A \in V \to F : S ⟶ 𝒫 S$
16	15	frnd	$⊢ A \in V \to ran F \subseteq 𝒫 S$
17		0ss	$⊢ \emptyset \subseteq A$
18		0fi	$⊢ \emptyset \in Fin$
19		elfpw	$⊢ \emptyset \in (𝒫 A \cap Fin) \leftrightarrow (\emptyset \subseteq A \land \emptyset \in Fin)$
20	17 18 19	mpbir2an	$⊢ \emptyset \in (𝒫 A \cap Fin)$
21	20 1	eleqtrri	$⊢ \emptyset \in S$
22		0ss	$⊢ \emptyset \subseteq y$
23	22	rgenw	$⊢ \forall y \in S \emptyset \subseteq y$
24		rabid2	$⊢ S = \{y \in S \| z \subseteq y\} \leftrightarrow \forall y \in S z \subseteq y$
25		sseq1	$⊢ z = \emptyset \to (z \subseteq y \leftrightarrow \emptyset \subseteq y)$
26	25	ralbidv	$⊢ z = \emptyset \to (\forall y \in S z \subseteq y \leftrightarrow \forall y \in S \emptyset \subseteq y)$
27	24 26	bitrid	$⊢ z = \emptyset \to (S = \{y \in S \| z \subseteq y\} \leftrightarrow \forall y \in S \emptyset \subseteq y)$
28	27	rspcev	$⊢ (\emptyset \in S \land \forall y \in S \emptyset \subseteq y) \to \exists z \in S S = \{y \in S \| z \subseteq y\}$
29	21 23 28	mp2an	$⊢ \exists z \in S S = \{y \in S \| z \subseteq y\}$
30	2	elrnmpt	$⊢ S \in V \to (S \in ran F \leftrightarrow \exists z \in S S = \{y \in S \| z \subseteq y\})$
31	10 30	syl	$⊢ A \in V \to (S \in ran F \leftrightarrow \exists z \in S S = \{y \in S \| z \subseteq y\})$
32	29 31	mpbiri	$⊢ A \in V \to S \in ran F$
33	32	ne0d	$⊢ A \in V \to ran F \neq \emptyset$
34		simpr	$⊢ (A \in V \land z \in S) \to z \in S$
35		ssid	$⊢ z \subseteq z$
36		sseq2	$⊢ y = z \to (z \subseteq y \leftrightarrow z \subseteq z)$
37	36	rspcev	$⊢ (z \in S \land z \subseteq z) \to \exists y \in S z \subseteq y$
38	34 35 37	sylancl	$⊢ (A \in V \land z \in S) \to \exists y \in S z \subseteq y$
39		rabn0	$⊢ \{y \in S \| z \subseteq y\} \neq \emptyset \leftrightarrow \exists y \in S z \subseteq y$
40	38 39	sylibr	$⊢ (A \in V \land z \in S) \to \{y \in S \| z \subseteq y\} \neq \emptyset$
41	40	necomd	$⊢ (A \in V \land z \in S) \to \emptyset \neq \{y \in S \| z \subseteq y\}$
42	41	neneqd	$⊢ (A \in V \land z \in S) \to \neg \emptyset = \{y \in S \| z \subseteq y\}$
43	42	nrexdv	$⊢ A \in V \to \neg \exists z \in S \emptyset = \{y \in S \| z \subseteq y\}$
44		0ex	$⊢ \emptyset \in V$
45	2	elrnmpt	$⊢ \emptyset \in V \to (\emptyset \in ran F \leftrightarrow \exists z \in S \emptyset = \{y \in S \| z \subseteq y\})$
46	44 45	ax-mp	$⊢ \emptyset \in ran F \leftrightarrow \exists z \in S \emptyset = \{y \in S \| z \subseteq y\}$
47	43 46	sylnibr	$⊢ A \in V \to \neg \emptyset \in ran F$
48		df-nel	$⊢ \emptyset \notin ran F \leftrightarrow \neg \emptyset \in ran F$
49	47 48	sylibr	$⊢ A \in V \to \emptyset \notin ran F$
50		elfpw	$⊢ u \in (𝒫 A \cap Fin) \leftrightarrow (u \subseteq A \land u \in Fin)$
51	50	simplbi	$⊢ u \in (𝒫 A \cap Fin) \to u \subseteq A$
52	51 1	eleq2s	$⊢ u \in S \to u \subseteq A$
53		elfpw	$⊢ v \in (𝒫 A \cap Fin) \leftrightarrow (v \subseteq A \land v \in Fin)$
54	53	simplbi	$⊢ v \in (𝒫 A \cap Fin) \to v \subseteq A$
55	54 1	eleq2s	$⊢ v \in S \to v \subseteq A$
56	52 55	anim12i	$⊢ (u \in S \land v \in S) \to (u \subseteq A \land v \subseteq A)$
57		unss	$⊢ (u \subseteq A \land v \subseteq A) \leftrightarrow u \cup v \subseteq A$
58	56 57	sylib	$⊢ (u \in S \land v \in S) \to u \cup v \subseteq A$
59		elinel2	$⊢ u \in (𝒫 A \cap Fin) \to u \in Fin$
60	59 1	eleq2s	$⊢ u \in S \to u \in Fin$
61		elinel2	$⊢ v \in (𝒫 A \cap Fin) \to v \in Fin$
62	61 1	eleq2s	$⊢ v \in S \to v \in Fin$
63		unfi	$⊢ (u \in Fin \land v \in Fin) \to u \cup v \in Fin$
64	60 62 63	syl2an	$⊢ (u \in S \land v \in S) \to u \cup v \in Fin$
65		elfpw	$⊢ u \cup v \in (𝒫 A \cap Fin) \leftrightarrow (u \cup v \subseteq A \land u \cup v \in Fin)$
66	58 64 65	sylanbrc	$⊢ (u \in S \land v \in S) \to u \cup v \in (𝒫 A \cap Fin)$
67	66	adantl	$⊢ (A \in V \land (u \in S \land v \in S)) \to u \cup v \in (𝒫 A \cap Fin)$
68	67 1	eleqtrrdi	$⊢ (A \in V \land (u \in S \land v \in S)) \to u \cup v \in S$
69		eqidd	$⊢ (A \in V \land (u \in S \land v \in S)) \to \{y \in S \| u \cup v \subseteq y\} = \{y \in S \| u \cup v \subseteq y\}$
70		sseq1	$⊢ a = u \cup v \to (a \subseteq y \leftrightarrow u \cup v \subseteq y)$
71	70	rabbidv	$⊢ a = u \cup v \to \{y \in S \| a \subseteq y\} = \{y \in S \| u \cup v \subseteq y\}$
72	71	rspceeqv	$⊢ (u \cup v \in S \land \{y \in S \| u \cup v \subseteq y\} = \{y \in S \| u \cup v \subseteq y\}) \to \exists a \in S \{y \in S \| u \cup v \subseteq y\} = \{y \in S \| a \subseteq y\}$
73	68 69 72	syl2anc	$⊢ (A \in V \land (u \in S \land v \in S)) \to \exists a \in S \{y \in S \| u \cup v \subseteq y\} = \{y \in S \| a \subseteq y\}$
74	10	adantr	$⊢ (A \in V \land (u \in S \land v \in S)) \to S \in V$
75		rabexg	$⊢ S \in V \to \{y \in S \| u \cup v \subseteq y\} \in V$
76	74 75	syl	$⊢ (A \in V \land (u \in S \land v \in S)) \to \{y \in S \| u \cup v \subseteq y\} \in V$
77		sseq1	$⊢ z = a \to (z \subseteq y \leftrightarrow a \subseteq y)$
78	77	rabbidv	$⊢ z = a \to \{y \in S \| z \subseteq y\} = \{y \in S \| a \subseteq y\}$
79	78	cbvmptv	$⊢ (z \in S ⟼ \{y \in S \| z \subseteq y\}) = (a \in S ⟼ \{y \in S \| a \subseteq y\})$
80	2 79	eqtri	$⊢ F = (a \in S ⟼ \{y \in S \| a \subseteq y\})$
81	80	elrnmpt	$⊢ \{y \in S \| u \cup v \subseteq y\} \in V \to (\{y \in S \| u \cup v \subseteq y\} \in ran F \leftrightarrow \exists a \in S \{y \in S \| u \cup v \subseteq y\} = \{y \in S \| a \subseteq y\})$
82	76 81	syl	$⊢ (A \in V \land (u \in S \land v \in S)) \to (\{y \in S \| u \cup v \subseteq y\} \in ran F \leftrightarrow \exists a \in S \{y \in S \| u \cup v \subseteq y\} = \{y \in S \| a \subseteq y\})$
83	73 82	mpbird	$⊢ (A \in V \land (u \in S \land v \in S)) \to \{y \in S \| u \cup v \subseteq y\} \in ran F$
84		pwidg	$⊢ \{y \in S \| u \cup v \subseteq y\} \in V \to \{y \in S \| u \cup v \subseteq y\} \in 𝒫 \{y \in S \| u \cup v \subseteq y\}$
85	76 84	syl	$⊢ (A \in V \land (u \in S \land v \in S)) \to \{y \in S \| u \cup v \subseteq y\} \in 𝒫 \{y \in S \| u \cup v \subseteq y\}$
86		inelcm	$⊢ (\{y \in S \| u \cup v \subseteq y\} \in ran F \land \{y \in S \| u \cup v \subseteq y\} \in 𝒫 \{y \in S \| u \cup v \subseteq y\}) \to ran F \cap 𝒫 \{y \in S \| u \cup v \subseteq y\} \neq \emptyset$
87	83 85 86	syl2anc	$⊢ (A \in V \land (u \in S \land v \in S)) \to ran F \cap 𝒫 \{y \in S \| u \cup v \subseteq y\} \neq \emptyset$
88	87	ralrimivva	$⊢ A \in V \to \forall u \in S \forall v \in S ran F \cap 𝒫 \{y \in S \| u \cup v \subseteq y\} \neq \emptyset$
89		rabexg	$⊢ S \in V \to \{y \in S \| u \subseteq y\} \in V$
90	10 89	syl	$⊢ A \in V \to \{y \in S \| u \subseteq y\} \in V$
91	90	ralrimivw	$⊢ A \in V \to \forall u \in S \{y \in S \| u \subseteq y\} \in V$
92		sseq1	$⊢ z = u \to (z \subseteq y \leftrightarrow u \subseteq y)$
93	92	rabbidv	$⊢ z = u \to \{y \in S \| z \subseteq y\} = \{y \in S \| u \subseteq y\}$
94	93	cbvmptv	$⊢ (z \in S ⟼ \{y \in S \| z \subseteq y\}) = (u \in S ⟼ \{y \in S \| u \subseteq y\})$
95	2 94	eqtri	$⊢ F = (u \in S ⟼ \{y \in S \| u \subseteq y\})$
96		ineq1	$⊢ a = \{y \in S \| u \subseteq y\} \to a \cap \{y \in S \| v \subseteq y\} = \{y \in S \| u \subseteq y\} \cap \{y \in S \| v \subseteq y\}$
97		inrab	$⊢ \{y \in S \| u \subseteq y\} \cap \{y \in S \| v \subseteq y\} = \{y \in S \| (u \subseteq y \land v \subseteq y)\}$
98		unss	$⊢ (u \subseteq y \land v \subseteq y) \leftrightarrow u \cup v \subseteq y$
99	98	rabbii	$⊢ \{y \in S \| (u \subseteq y \land v \subseteq y)\} = \{y \in S \| u \cup v \subseteq y\}$
100	97 99	eqtri	$⊢ \{y \in S \| u \subseteq y\} \cap \{y \in S \| v \subseteq y\} = \{y \in S \| u \cup v \subseteq y\}$
101	96 100	eqtrdi	$⊢ a = \{y \in S \| u \subseteq y\} \to a \cap \{y \in S \| v \subseteq y\} = \{y \in S \| u \cup v \subseteq y\}$
102	101	pweqd	$⊢ a = \{y \in S \| u \subseteq y\} \to 𝒫 (a \cap \{y \in S \| v \subseteq y\}) = 𝒫 \{y \in S \| u \cup v \subseteq y\}$
103	102	ineq2d	$⊢ a = \{y \in S \| u \subseteq y\} \to ran F \cap 𝒫 (a \cap \{y \in S \| v \subseteq y\}) = ran F \cap 𝒫 \{y \in S \| u \cup v \subseteq y\}$
104	103	neeq1d	$⊢ a = \{y \in S \| u \subseteq y\} \to (ran F \cap 𝒫 (a \cap \{y \in S \| v \subseteq y\}) \neq \emptyset \leftrightarrow ran F \cap 𝒫 \{y \in S \| u \cup v \subseteq y\} \neq \emptyset)$
105	104	ralbidv	$⊢ a = \{y \in S \| u \subseteq y\} \to (\forall v \in S ran F \cap 𝒫 (a \cap \{y \in S \| v \subseteq y\}) \neq \emptyset \leftrightarrow \forall v \in S ran F \cap 𝒫 \{y \in S \| u \cup v \subseteq y\} \neq \emptyset)$
106	95 105	ralrnmptw	$⊢ \forall u \in S \{y \in S \| u \subseteq y\} \in V \to (\forall a \in ran F \forall v \in S ran F \cap 𝒫 (a \cap \{y \in S \| v \subseteq y\}) \neq \emptyset \leftrightarrow \forall u \in S \forall v \in S ran F \cap 𝒫 \{y \in S \| u \cup v \subseteq y\} \neq \emptyset)$
107	91 106	syl	$⊢ A \in V \to (\forall a \in ran F \forall v \in S ran F \cap 𝒫 (a \cap \{y \in S \| v \subseteq y\}) \neq \emptyset \leftrightarrow \forall u \in S \forall v \in S ran F \cap 𝒫 \{y \in S \| u \cup v \subseteq y\} \neq \emptyset)$
108	88 107	mpbird	$⊢ A \in V \to \forall a \in ran F \forall v \in S ran F \cap 𝒫 (a \cap \{y \in S \| v \subseteq y\}) \neq \emptyset$
109		rabexg	$⊢ S \in V \to \{y \in S \| v \subseteq y\} \in V$
110	10 109	syl	$⊢ A \in V \to \{y \in S \| v \subseteq y\} \in V$
111	110	ralrimivw	$⊢ A \in V \to \forall v \in S \{y \in S \| v \subseteq y\} \in V$
112		sseq1	$⊢ z = v \to (z \subseteq y \leftrightarrow v \subseteq y)$
113	112	rabbidv	$⊢ z = v \to \{y \in S \| z \subseteq y\} = \{y \in S \| v \subseteq y\}$
114	113	cbvmptv	$⊢ (z \in S ⟼ \{y \in S \| z \subseteq y\}) = (v \in S ⟼ \{y \in S \| v \subseteq y\})$
115	2 114	eqtri	$⊢ F = (v \in S ⟼ \{y \in S \| v \subseteq y\})$
116		ineq2	$⊢ b = \{y \in S \| v \subseteq y\} \to a \cap b = a \cap \{y \in S \| v \subseteq y\}$
117	116	pweqd	$⊢ b = \{y \in S \| v \subseteq y\} \to 𝒫 (a \cap b) = 𝒫 (a \cap \{y \in S \| v \subseteq y\})$
118	117	ineq2d	$⊢ b = \{y \in S \| v \subseteq y\} \to ran F \cap 𝒫 (a \cap b) = ran F \cap 𝒫 (a \cap \{y \in S \| v \subseteq y\})$
119	118	neeq1d	$⊢ b = \{y \in S \| v \subseteq y\} \to (ran F \cap 𝒫 (a \cap b) \neq \emptyset \leftrightarrow ran F \cap 𝒫 (a \cap \{y \in S \| v \subseteq y\}) \neq \emptyset)$
120	115 119	ralrnmptw	$⊢ \forall v \in S \{y \in S \| v \subseteq y\} \in V \to (\forall b \in ran F ran F \cap 𝒫 (a \cap b) \neq \emptyset \leftrightarrow \forall v \in S ran F \cap 𝒫 (a \cap \{y \in S \| v \subseteq y\}) \neq \emptyset)$
121	111 120	syl	$⊢ A \in V \to (\forall b \in ran F ran F \cap 𝒫 (a \cap b) \neq \emptyset \leftrightarrow \forall v \in S ran F \cap 𝒫 (a \cap \{y \in S \| v \subseteq y\}) \neq \emptyset)$
122	121	ralbidv	$⊢ A \in V \to (\forall a \in ran F \forall b \in ran F ran F \cap 𝒫 (a \cap b) \neq \emptyset \leftrightarrow \forall a \in ran F \forall v \in S ran F \cap 𝒫 (a \cap \{y \in S \| v \subseteq y\}) \neq \emptyset)$
123	108 122	mpbird	$⊢ A \in V \to \forall a \in ran F \forall b \in ran F ran F \cap 𝒫 (a \cap b) \neq \emptyset$
124	33 49 123	3jca	$⊢ A \in V \to (ran F \neq \emptyset \land \emptyset \notin ran F \land \forall a \in ran F \forall b \in ran F ran F \cap 𝒫 (a \cap b) \neq \emptyset)$
125		isfbas	$⊢ S \in V \to (ran F \in fBas (S) \leftrightarrow (ran F \subseteq 𝒫 S \land (ran F \neq \emptyset \land \emptyset \notin ran F \land \forall a \in ran F \forall b \in ran F ran F \cap 𝒫 (a \cap b) \neq \emptyset)))$
126	10 125	syl	$⊢ A \in V \to (ran F \in fBas (S) \leftrightarrow (ran F \subseteq 𝒫 S \land (ran F \neq \emptyset \land \emptyset \notin ran F \land \forall a \in ran F \forall b \in ran F ran F \cap 𝒫 (a \cap b) \neq \emptyset)))$
127	16 124 126	mpbir2and	$⊢ A \in V \to ran F \in fBas (S)$
128	3 127	eqeltrid	$⊢ A \in V \to L \in fBas (S)$
129	4 5 128	3syl	$⊢ φ \to L \in fBas (S)$

Metamath Proof Explorer

Theorem tsmsfbas

Proof