dffi2

Description: The set of finite intersections is the smallest set that contains A and is closed under pairwise intersection. (Contributed by Mario Carneiro, 24-Nov-2013)

		Ref	Expression
	Assertion	dffi2	$⊢ A \in V \to fi (A) = ⋂ \{z \| (A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z)\}$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in V \to A \in V$
2		vex	$⊢ t \in V$
3		elfi	$⊢ (t \in V \land A \in V) \to (t \in fi (A) \leftrightarrow \exists x \in (𝒫 A \cap Fin) t = ⋂ x)$
4	2 3	mpan	$⊢ A \in V \to (t \in fi (A) \leftrightarrow \exists x \in (𝒫 A \cap Fin) t = ⋂ x)$
5	4	biimpd	$⊢ A \in V \to (t \in fi (A) \to \exists x \in (𝒫 A \cap Fin) t = ⋂ x)$
6		df-rex	$⊢ \exists x \in (𝒫 A \cap Fin) t = ⋂ x \leftrightarrow \exists x (x \in (𝒫 A \cap Fin) \land t = ⋂ x)$
7		fiint	$⊢ \forall x \in z \forall y \in z x \cap y \in z \leftrightarrow \forall x ((x \subseteq z \land x \neq \emptyset \land x \in Fin) \to ⋂ x \in z)$
8		elinel1	$⊢ x \in (𝒫 A \cap Fin) \to x \in 𝒫 A$
9	8	elpwid	$⊢ x \in (𝒫 A \cap Fin) \to x \subseteq A$
10	9	3ad2ant2	$⊢ (A \subseteq z \land x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to x \subseteq A$
11		simp1	$⊢ (A \subseteq z \land x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to A \subseteq z$
12	10 11	sstrd	$⊢ (A \subseteq z \land x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to x \subseteq z$
13		eqvisset	$⊢ t = ⋂ x \to ⋂ x \in V$
14		intex	$⊢ x \neq \emptyset \leftrightarrow ⋂ x \in V$
15	13 14	sylibr	$⊢ t = ⋂ x \to x \neq \emptyset$
16	15	3ad2ant3	$⊢ (A \subseteq z \land x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to x \neq \emptyset$
17		elinel2	$⊢ x \in (𝒫 A \cap Fin) \to x \in Fin$
18	17	3ad2ant2	$⊢ (A \subseteq z \land x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to x \in Fin$
19	12 16 18	3jca	$⊢ (A \subseteq z \land x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to (x \subseteq z \land x \neq \emptyset \land x \in Fin)$
20	19	3expib	$⊢ A \subseteq z \to ((x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to (x \subseteq z \land x \neq \emptyset \land x \in Fin))$
21		pm2.27	$⊢ (x \subseteq z \land x \neq \emptyset \land x \in Fin) \to (((x \subseteq z \land x \neq \emptyset \land x \in Fin) \to ⋂ x \in z) \to ⋂ x \in z)$
22	20 21	syl6	$⊢ A \subseteq z \to ((x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to (((x \subseteq z \land x \neq \emptyset \land x \in Fin) \to ⋂ x \in z) \to ⋂ x \in z))$
23		eleq1	$⊢ t = ⋂ x \to (t \in z \leftrightarrow ⋂ x \in z)$
24	23	biimprd	$⊢ t = ⋂ x \to (⋂ x \in z \to t \in z)$
25	24	adantl	$⊢ (x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to (⋂ x \in z \to t \in z)$
26	25	a1i	$⊢ A \subseteq z \to ((x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to (⋂ x \in z \to t \in z))$
27	22 26	syldd	$⊢ A \subseteq z \to ((x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to (((x \subseteq z \land x \neq \emptyset \land x \in Fin) \to ⋂ x \in z) \to t \in z))$
28	27	com23	$⊢ A \subseteq z \to (((x \subseteq z \land x \neq \emptyset \land x \in Fin) \to ⋂ x \in z) \to ((x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to t \in z))$
29	28	alimdv	$⊢ A \subseteq z \to (\forall x ((x \subseteq z \land x \neq \emptyset \land x \in Fin) \to ⋂ x \in z) \to \forall x ((x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to t \in z))$
30	7 29	syl5bi	$⊢ A \subseteq z \to (\forall x \in z \forall y \in z x \cap y \in z \to \forall x ((x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to t \in z))$
31	30	imp	$⊢ (A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z) \to \forall x ((x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to t \in z)$
32		19.23v	$⊢ \forall x ((x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to t \in z) \leftrightarrow (\exists x (x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to t \in z)$
33	31 32	sylib	$⊢ (A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z) \to (\exists x (x \in (𝒫 A \cap Fin) \land t = ⋂ x) \to t \in z)$
34	6 33	syl5bi	$⊢ (A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z) \to (\exists x \in (𝒫 A \cap Fin) t = ⋂ x \to t \in z)$
35	5 34	sylan9	$⊢ (A \in V \land (A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z)) \to (t \in fi (A) \to t \in z)$
36	35	ssrdv	$⊢ (A \in V \land (A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z)) \to fi (A) \subseteq z$
37	36	ex	$⊢ A \in V \to ((A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z) \to fi (A) \subseteq z)$
38	37	alrimiv	$⊢ A \in V \to \forall z ((A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z) \to fi (A) \subseteq z)$
39		ssintab	$⊢ fi (A) \subseteq ⋂ \{z \| (A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z)\} \leftrightarrow \forall z ((A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z) \to fi (A) \subseteq z)$
40	38 39	sylibr	$⊢ A \in V \to fi (A) \subseteq ⋂ \{z \| (A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z)\}$
41		ssfii	$⊢ A \in V \to A \subseteq fi (A)$
42		fiin	$⊢ (x \in fi (A) \land y \in fi (A)) \to x \cap y \in fi (A)$
43	42	rgen2	$⊢ \forall x \in fi (A) \forall y \in fi (A) x \cap y \in fi (A)$
44		fvex	$⊢ fi (A) \in V$
45		sseq2	$⊢ z = fi (A) \to (A \subseteq z \leftrightarrow A \subseteq fi (A))$
46		eleq2	$⊢ z = fi (A) \to (x \cap y \in z \leftrightarrow x \cap y \in fi (A))$
47	46	raleqbi1dv	$⊢ z = fi (A) \to (\forall y \in z x \cap y \in z \leftrightarrow \forall y \in fi (A) x \cap y \in fi (A))$
48	47	raleqbi1dv	$⊢ z = fi (A) \to (\forall x \in z \forall y \in z x \cap y \in z \leftrightarrow \forall x \in fi (A) \forall y \in fi (A) x \cap y \in fi (A))$
49	45 48	anbi12d	$⊢ z = fi (A) \to ((A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z) \leftrightarrow (A \subseteq fi (A) \land \forall x \in fi (A) \forall y \in fi (A) x \cap y \in fi (A)))$
50	44 49	elab	$⊢ fi (A) \in \{z \| (A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z)\} \leftrightarrow (A \subseteq fi (A) \land \forall x \in fi (A) \forall y \in fi (A) x \cap y \in fi (A))$
51	41 43 50	sylanblrc	$⊢ A \in V \to fi (A) \in \{z \| (A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z)\}$
52		intss1	$⊢ fi (A) \in \{z \| (A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z)\} \to ⋂ \{z \| (A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z)\} \subseteq fi (A)$
53	51 52	syl	$⊢ A \in V \to ⋂ \{z \| (A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z)\} \subseteq fi (A)$
54	40 53	eqssd	$⊢ A \in V \to fi (A) = ⋂ \{z \| (A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z)\}$
55	1 54	syl	$⊢ A \in V \to fi (A) = ⋂ \{z \| (A \subseteq z \land \forall x \in z \forall y \in z x \cap y \in z)\}$

Metamath Proof Explorer

Theorem dffi2

Proof