fiint

Description: Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite nonempty subcollection of A is in A ". This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use the left-hand version of this axiom and others the right-hand version, but as our proof here shows, their "intuitively obvious" equivalence can be non-trivial to establish formally. (Contributed by NM, 22-Sep-2002) Use a separate setvar for the right-hand side and avoid ax-pow . (Revised by BTernaryTau, 14-Jan-2025)

		Ref	Expression
	Assertion	fiint	$⊢ \forall x \in A \forall y \in A x \cap y \in A \leftrightarrow \forall z ((z \subseteq A \land z \neq \emptyset \land z \in Fin) \to ⋂ z \in A)$

Proof

Step	Hyp	Ref	Expression
1		isfi	$⊢ z \in Fin \leftrightarrow \exists w \in ω z \approx w$
2		nnfi	$⊢ w \in ω \to w \in Fin$
3		ensymfib	$⊢ w \in Fin \to (w \approx z \leftrightarrow z \approx w)$
4	2 3	syl	$⊢ w \in ω \to (w \approx z \leftrightarrow z \approx w)$
5		breq1	$⊢ w = \emptyset \to (w \approx z \leftrightarrow \emptyset \approx z)$
6	5	anbi2d	$⊢ w = \emptyset \to (((z \subseteq A \land z \neq \emptyset) \land w \approx z) \leftrightarrow ((z \subseteq A \land z \neq \emptyset) \land \emptyset \approx z))$
7	6	imbi1d	$⊢ w = \emptyset \to ((((z \subseteq A \land z \neq \emptyset) \land w \approx z) \to ⋂ z \in A) \leftrightarrow (((z \subseteq A \land z \neq \emptyset) \land \emptyset \approx z) \to ⋂ z \in A))$
8	7	albidv	$⊢ w = \emptyset \to (\forall z (((z \subseteq A \land z \neq \emptyset) \land w \approx z) \to ⋂ z \in A) \leftrightarrow \forall z (((z \subseteq A \land z \neq \emptyset) \land \emptyset \approx z) \to ⋂ z \in A))$
9		breq1	$⊢ w = t \to (w \approx z \leftrightarrow t \approx z)$
10	9	anbi2d	$⊢ w = t \to (((z \subseteq A \land z \neq \emptyset) \land w \approx z) \leftrightarrow ((z \subseteq A \land z \neq \emptyset) \land t \approx z))$
11	10	imbi1d	$⊢ w = t \to ((((z \subseteq A \land z \neq \emptyset) \land w \approx z) \to ⋂ z \in A) \leftrightarrow (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A))$
12	11	albidv	$⊢ w = t \to (\forall z (((z \subseteq A \land z \neq \emptyset) \land w \approx z) \to ⋂ z \in A) \leftrightarrow \forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A))$
13		breq1	$⊢ w = suc t \to (w \approx z \leftrightarrow suc t \approx z)$
14	13	anbi2d	$⊢ w = suc t \to (((z \subseteq A \land z \neq \emptyset) \land w \approx z) \leftrightarrow ((z \subseteq A \land z \neq \emptyset) \land suc t \approx z))$
15	14	imbi1d	$⊢ w = suc t \to ((((z \subseteq A \land z \neq \emptyset) \land w \approx z) \to ⋂ z \in A) \leftrightarrow (((z \subseteq A \land z \neq \emptyset) \land suc t \approx z) \to ⋂ z \in A))$
16	15	albidv	$⊢ w = suc t \to (\forall z (((z \subseteq A \land z \neq \emptyset) \land w \approx z) \to ⋂ z \in A) \leftrightarrow \forall z (((z \subseteq A \land z \neq \emptyset) \land suc t \approx z) \to ⋂ z \in A))$
17		en0r	$⊢ \emptyset \approx z \leftrightarrow z = \emptyset$
18	17	biimpi	$⊢ \emptyset \approx z \to z = \emptyset$
19	18	anim1i	$⊢ (\emptyset \approx z \land z \neq \emptyset) \to (z = \emptyset \land z \neq \emptyset)$
20	19	ancoms	$⊢ (z \neq \emptyset \land \emptyset \approx z) \to (z = \emptyset \land z \neq \emptyset)$
21	20	adantll	$⊢ ((z \subseteq A \land z \neq \emptyset) \land \emptyset \approx z) \to (z = \emptyset \land z \neq \emptyset)$
22		df-ne	$⊢ z \neq \emptyset \leftrightarrow \neg z = \emptyset$
23		pm3.24	$⊢ \neg (z = \emptyset \land \neg z = \emptyset)$
24	23	pm2.21i	$⊢ (z = \emptyset \land \neg z = \emptyset) \to ⋂ z \in A$
25	22 24	sylan2b	$⊢ (z = \emptyset \land z \neq \emptyset) \to ⋂ z \in A$
26	21 25	syl	$⊢ ((z \subseteq A \land z \neq \emptyset) \land \emptyset \approx z) \to ⋂ z \in A$
27	26	ax-gen	$⊢ \forall z (((z \subseteq A \land z \neq \emptyset) \land \emptyset \approx z) \to ⋂ z \in A)$
28	27	a1i	$⊢ \forall v \in A \forall u \in A v \cap u \in A \to \forall z (((z \subseteq A \land z \neq \emptyset) \land \emptyset \approx z) \to ⋂ z \in A)$
29		nfv	$⊢ Ⅎ z \forall v \in A \forall u \in A v \cap u \in A$
30		nfa1	$⊢ Ⅎ z \forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A)$
31		bren	$⊢ suc t \approx z \leftrightarrow \exists f f : suc t \underset{1-1 onto}{⟶} z$
32		ssel	$⊢ z \subseteq A \to (f (t) \in z \to f (t) \in A)$
33		f1of	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to f : suc t ⟶ z$
34		vex	$⊢ t \in V$
35	34	sucid	$⊢ t \in suc t$
36		ffvelcdm	$⊢ (f : suc t ⟶ z \land t \in suc t) \to f (t) \in z$
37	33 35 36	sylancl	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to f (t) \in z$
38	32 37	impel	$⊢ (z \subseteq A \land f : suc t \underset{1-1 onto}{⟶} z) \to f (t) \in A$
39	38	adantr	$⊢ ((z \subseteq A \land f : suc t \underset{1-1 onto}{⟶} z) \land (\forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \land \forall v \in A \forall u \in A v \cap u \in A)) \to f (t) \in A$
40		df-ne	$⊢ f [t] \neq \emptyset \leftrightarrow \neg f [t] = \emptyset$
41		imassrn	$⊢ f [t] \subseteq ran f$
42		dff1o2	$⊢ f : suc t \underset{1-1 onto}{⟶} z \leftrightarrow (f Fn suc t \land Fun f^{-1} \land ran f = z)$
43	42	simp3bi	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to ran f = z$
44	41 43	sseqtrid	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to f [t] \subseteq z$
45		sstr2	$⊢ f [t] \subseteq z \to (z \subseteq A \to f [t] \subseteq A)$
46	44 45	syl	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to (z \subseteq A \to f [t] \subseteq A)$
47	46	anim1d	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to ((z \subseteq A \land f [t] \neq \emptyset) \to (f [t] \subseteq A \land f [t] \neq \emptyset))$
48		f1of1	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to f : suc t \underset{1-1}{⟶} z$
49		sssucid	$⊢ t \subseteq suc t$
50		vex	$⊢ f \in V$
51		f1imaen3g	$⊢ (f : suc t \underset{1-1}{⟶} z \land t \subseteq suc t \land f \in V) \to t \approx f [t]$
52	49 50 51	mp3an23	$⊢ f : suc t \underset{1-1}{⟶} z \to t \approx f [t]$
53	48 52	syl	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to t \approx f [t]$
54	47 53	jctird	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to ((z \subseteq A \land f [t] \neq \emptyset) \to ((f [t] \subseteq A \land f [t] \neq \emptyset) \land t \approx f [t]))$
55	50	imaex	$⊢ f [t] \in V$
56		sseq1	$⊢ z = f [t] \to (z \subseteq A \leftrightarrow f [t] \subseteq A)$
57		neeq1	$⊢ z = f [t] \to (z \neq \emptyset \leftrightarrow f [t] \neq \emptyset)$
58	56 57	anbi12d	$⊢ z = f [t] \to ((z \subseteq A \land z \neq \emptyset) \leftrightarrow (f [t] \subseteq A \land f [t] \neq \emptyset))$
59		breq2	$⊢ z = f [t] \to (t \approx z \leftrightarrow t \approx f [t])$
60	58 59	anbi12d	$⊢ z = f [t] \to (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \leftrightarrow ((f [t] \subseteq A \land f [t] \neq \emptyset) \land t \approx f [t]))$
61		inteq	$⊢ z = f [t] \to ⋂ z = ⋂ f [t]$
62	61	eleq1d	$⊢ z = f [t] \to (⋂ z \in A \leftrightarrow ⋂ f [t] \in A)$
63	60 62	imbi12d	$⊢ z = f [t] \to ((((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \leftrightarrow (((f [t] \subseteq A \land f [t] \neq \emptyset) \land t \approx f [t]) \to ⋂ f [t] \in A))$
64	55 63	spcv	$⊢ \forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \to (((f [t] \subseteq A \land f [t] \neq \emptyset) \land t \approx f [t]) \to ⋂ f [t] \in A)$
65	54 64	sylan9	$⊢ (f : suc t \underset{1-1 onto}{⟶} z \land \forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A)) \to ((z \subseteq A \land f [t] \neq \emptyset) \to ⋂ f [t] \in A)$
66		ineq1	$⊢ v = ⋂ f [t] \to v \cap u = ⋂ f [t] \cap u$
67	66	eleq1d	$⊢ v = ⋂ f [t] \to (v \cap u \in A \leftrightarrow ⋂ f [t] \cap u \in A)$
68		ineq2	$⊢ u = f (t) \to ⋂ f [t] \cap u = ⋂ f [t] \cap f (t)$
69	68	eleq1d	$⊢ u = f (t) \to (⋂ f [t] \cap u \in A \leftrightarrow ⋂ f [t] \cap f (t) \in A)$
70	67 69	rspc2v	$⊢ (⋂ f [t] \in A \land f (t) \in A) \to (\forall v \in A \forall u \in A v \cap u \in A \to ⋂ f [t] \cap f (t) \in A)$
71	70	ex	$⊢ ⋂ f [t] \in A \to (f (t) \in A \to (\forall v \in A \forall u \in A v \cap u \in A \to ⋂ f [t] \cap f (t) \in A))$
72	65 71	syl6	$⊢ (f : suc t \underset{1-1 onto}{⟶} z \land \forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A)) \to ((z \subseteq A \land f [t] \neq \emptyset) \to (f (t) \in A \to (\forall v \in A \forall u \in A v \cap u \in A \to ⋂ f [t] \cap f (t) \in A)))$
73	72	com4r	$⊢ \forall v \in A \forall u \in A v \cap u \in A \to ((f : suc t \underset{1-1 onto}{⟶} z \land \forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A)) \to ((z \subseteq A \land f [t] \neq \emptyset) \to (f (t) \in A \to ⋂ f [t] \cap f (t) \in A)))$
74	73	exp5c	$⊢ \forall v \in A \forall u \in A v \cap u \in A \to (f : suc t \underset{1-1 onto}{⟶} z \to (\forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \to (z \subseteq A \to (f [t] \neq \emptyset \to (f (t) \in A \to ⋂ f [t] \cap f (t) \in A)))))$
75	74	com14	$⊢ z \subseteq A \to (f : suc t \underset{1-1 onto}{⟶} z \to (\forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \to (\forall v \in A \forall u \in A v \cap u \in A \to (f [t] \neq \emptyset \to (f (t) \in A \to ⋂ f [t] \cap f (t) \in A)))))$
76	75	imp43	$⊢ ((z \subseteq A \land f : suc t \underset{1-1 onto}{⟶} z) \land (\forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \land \forall v \in A \forall u \in A v \cap u \in A)) \to (f [t] \neq \emptyset \to (f (t) \in A \to ⋂ f [t] \cap f (t) \in A))$
77	40 76	biimtrrid	$⊢ ((z \subseteq A \land f : suc t \underset{1-1 onto}{⟶} z) \land (\forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \land \forall v \in A \forall u \in A v \cap u \in A)) \to (\neg f [t] = \emptyset \to (f (t) \in A \to ⋂ f [t] \cap f (t) \in A))$
78		inteq	$⊢ f [t] = \emptyset \to ⋂ f [t] = ⋂ \emptyset$
79		int0	$⊢ ⋂ \emptyset = V$
80	78 79	eqtrdi	$⊢ f [t] = \emptyset \to ⋂ f [t] = V$
81	80	ineq1d	$⊢ f [t] = \emptyset \to ⋂ f [t] \cap f (t) = V \cap f (t)$
82		ssv	$⊢ f (t) \subseteq V$
83		sseqin2	$⊢ f (t) \subseteq V \leftrightarrow V \cap f (t) = f (t)$
84	82 83	mpbi	$⊢ V \cap f (t) = f (t)$
85	81 84	eqtrdi	$⊢ f [t] = \emptyset \to ⋂ f [t] \cap f (t) = f (t)$
86	85	eleq1d	$⊢ f [t] = \emptyset \to (⋂ f [t] \cap f (t) \in A \leftrightarrow f (t) \in A)$
87	86	biimprd	$⊢ f [t] = \emptyset \to (f (t) \in A \to ⋂ f [t] \cap f (t) \in A)$
88	77 87	pm2.61d2	$⊢ ((z \subseteq A \land f : suc t \underset{1-1 onto}{⟶} z) \land (\forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \land \forall v \in A \forall u \in A v \cap u \in A)) \to (f (t) \in A \to ⋂ f [t] \cap f (t) \in A)$
89	39 88	mpd	$⊢ ((z \subseteq A \land f : suc t \underset{1-1 onto}{⟶} z) \land (\forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \land \forall v \in A \forall u \in A v \cap u \in A)) \to ⋂ f [t] \cap f (t) \in A$
90		fvex	$⊢ f (t) \in V$
91	90	intunsn	$⊢ ⋂ (f [t] \cup \{f (t)\}) = ⋂ f [t] \cap f (t)$
92		f1ofn	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to f Fn suc t$
93		fnsnfv	$⊢ (f Fn suc t \land t \in suc t) \to \{f (t)\} = f [\{t\}]$
94	92 35 93	sylancl	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to \{f (t)\} = f [\{t\}]$
95	94	uneq2d	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to f [t] \cup \{f (t)\} = f [t] \cup f [\{t\}]$
96		df-suc	$⊢ suc t = t \cup \{t\}$
97	96	imaeq2i	$⊢ f [suc t] = f [t \cup \{t\}]$
98		imaundi	$⊢ f [t \cup \{t\}] = f [t] \cup f [\{t\}]$
99	97 98	eqtr2i	$⊢ f [t] \cup f [\{t\}] = f [suc t]$
100	95 99	eqtrdi	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to f [t] \cup \{f (t)\} = f [suc t]$
101		f1ofo	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to f : suc t \underset{onto}{⟶} z$
102		foima	$⊢ f : suc t \underset{onto}{⟶} z \to f [suc t] = z$
103	101 102	syl	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to f [suc t] = z$
104	100 103	eqtrd	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to f [t] \cup \{f (t)\} = z$
105	104	inteqd	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to ⋂ (f [t] \cup \{f (t)\}) = ⋂ z$
106	91 105	eqtr3id	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to ⋂ f [t] \cap f (t) = ⋂ z$
107	106	eleq1d	$⊢ f : suc t \underset{1-1 onto}{⟶} z \to (⋂ f [t] \cap f (t) \in A \leftrightarrow ⋂ z \in A)$
108	107	ad2antlr	$⊢ ((z \subseteq A \land f : suc t \underset{1-1 onto}{⟶} z) \land (\forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \land \forall v \in A \forall u \in A v \cap u \in A)) \to (⋂ f [t] \cap f (t) \in A \leftrightarrow ⋂ z \in A)$
109	89 108	mpbid	$⊢ ((z \subseteq A \land f : suc t \underset{1-1 onto}{⟶} z) \land (\forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \land \forall v \in A \forall u \in A v \cap u \in A)) \to ⋂ z \in A$
110	109	exp43	$⊢ z \subseteq A \to (f : suc t \underset{1-1 onto}{⟶} z \to (\forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \to (\forall v \in A \forall u \in A v \cap u \in A \to ⋂ z \in A)))$
111	110	exlimdv	$⊢ z \subseteq A \to (\exists f f : suc t \underset{1-1 onto}{⟶} z \to (\forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \to (\forall v \in A \forall u \in A v \cap u \in A \to ⋂ z \in A)))$
112	31 111	biimtrid	$⊢ z \subseteq A \to (suc t \approx z \to (\forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \to (\forall v \in A \forall u \in A v \cap u \in A \to ⋂ z \in A)))$
113	112	imp	$⊢ (z \subseteq A \land suc t \approx z) \to (\forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \to (\forall v \in A \forall u \in A v \cap u \in A \to ⋂ z \in A))$
114	113	adantlr	$⊢ ((z \subseteq A \land z \neq \emptyset) \land suc t \approx z) \to (\forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \to (\forall v \in A \forall u \in A v \cap u \in A \to ⋂ z \in A))$
115	114	com13	$⊢ \forall v \in A \forall u \in A v \cap u \in A \to (\forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \to (((z \subseteq A \land z \neq \emptyset) \land suc t \approx z) \to ⋂ z \in A))$
116	29 30 115	alrimd	$⊢ \forall v \in A \forall u \in A v \cap u \in A \to (\forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \to \forall z (((z \subseteq A \land z \neq \emptyset) \land suc t \approx z) \to ⋂ z \in A))$
117	116	a1i	$⊢ t \in ω \to (\forall v \in A \forall u \in A v \cap u \in A \to (\forall z (((z \subseteq A \land z \neq \emptyset) \land t \approx z) \to ⋂ z \in A) \to \forall z (((z \subseteq A \land z \neq \emptyset) \land suc t \approx z) \to ⋂ z \in A)))$
118	8 12 16 28 117	finds2	$⊢ w \in ω \to (\forall v \in A \forall u \in A v \cap u \in A \to \forall z (((z \subseteq A \land z \neq \emptyset) \land w \approx z) \to ⋂ z \in A))$
119		sp	$⊢ \forall z (((z \subseteq A \land z \neq \emptyset) \land w \approx z) \to ⋂ z \in A) \to (((z \subseteq A \land z \neq \emptyset) \land w \approx z) \to ⋂ z \in A)$
120	118 119	syl6	$⊢ w \in ω \to (\forall v \in A \forall u \in A v \cap u \in A \to (((z \subseteq A \land z \neq \emptyset) \land w \approx z) \to ⋂ z \in A))$
121	120	exp4a	$⊢ w \in ω \to (\forall v \in A \forall u \in A v \cap u \in A \to ((z \subseteq A \land z \neq \emptyset) \to (w \approx z \to ⋂ z \in A)))$
122	121	com24	$⊢ w \in ω \to (w \approx z \to ((z \subseteq A \land z \neq \emptyset) \to (\forall v \in A \forall u \in A v \cap u \in A \to ⋂ z \in A)))$
123	4 122	sylbird	$⊢ w \in ω \to (z \approx w \to ((z \subseteq A \land z \neq \emptyset) \to (\forall v \in A \forall u \in A v \cap u \in A \to ⋂ z \in A)))$
124	123	rexlimiv	$⊢ \exists w \in ω z \approx w \to ((z \subseteq A \land z \neq \emptyset) \to (\forall v \in A \forall u \in A v \cap u \in A \to ⋂ z \in A))$
125	1 124	sylbi	$⊢ z \in Fin \to ((z \subseteq A \land z \neq \emptyset) \to (\forall v \in A \forall u \in A v \cap u \in A \to ⋂ z \in A))$
126	125	com13	$⊢ \forall v \in A \forall u \in A v \cap u \in A \to ((z \subseteq A \land z \neq \emptyset) \to (z \in Fin \to ⋂ z \in A))$
127	126	impd	$⊢ \forall v \in A \forall u \in A v \cap u \in A \to (((z \subseteq A \land z \neq \emptyset) \land z \in Fin) \to ⋂ z \in A)$
128	127	alrimiv	$⊢ \forall v \in A \forall u \in A v \cap u \in A \to \forall z (((z \subseteq A \land z \neq \emptyset) \land z \in Fin) \to ⋂ z \in A)$
129		zfpair2	$⊢ \{v, u\} \in V$
130		sseq1	$⊢ z = \{v, u\} \to (z \subseteq A \leftrightarrow \{v, u\} \subseteq A)$
131		neeq1	$⊢ z = \{v, u\} \to (z \neq \emptyset \leftrightarrow \{v, u\} \neq \emptyset)$
132	130 131	anbi12d	$⊢ z = \{v, u\} \to ((z \subseteq A \land z \neq \emptyset) \leftrightarrow (\{v, u\} \subseteq A \land \{v, u\} \neq \emptyset))$
133		eleq1	$⊢ z = \{v, u\} \to (z \in Fin \leftrightarrow \{v, u\} \in Fin)$
134	132 133	anbi12d	$⊢ z = \{v, u\} \to (((z \subseteq A \land z \neq \emptyset) \land z \in Fin) \leftrightarrow ((\{v, u\} \subseteq A \land \{v, u\} \neq \emptyset) \land \{v, u\} \in Fin))$
135		inteq	$⊢ z = \{v, u\} \to ⋂ z = ⋂ \{v, u\}$
136	135	eleq1d	$⊢ z = \{v, u\} \to (⋂ z \in A \leftrightarrow ⋂ \{v, u\} \in A)$
137	134 136	imbi12d	$⊢ z = \{v, u\} \to ((((z \subseteq A \land z \neq \emptyset) \land z \in Fin) \to ⋂ z \in A) \leftrightarrow (((\{v, u\} \subseteq A \land \{v, u\} \neq \emptyset) \land \{v, u\} \in Fin) \to ⋂ \{v, u\} \in A))$
138	129 137	spcv	$⊢ \forall z (((z \subseteq A \land z \neq \emptyset) \land z \in Fin) \to ⋂ z \in A) \to (((\{v, u\} \subseteq A \land \{v, u\} \neq \emptyset) \land \{v, u\} \in Fin) \to ⋂ \{v, u\} \in A)$
139		vex	$⊢ v \in V$
140		vex	$⊢ u \in V$
141	139 140	prss	$⊢ (v \in A \land u \in A) \leftrightarrow \{v, u\} \subseteq A$
142	139	prnz	$⊢ \{v, u\} \neq \emptyset$
143	142	biantru	$⊢ \{v, u\} \subseteq A \leftrightarrow (\{v, u\} \subseteq A \land \{v, u\} \neq \emptyset)$
144		prfi	$⊢ \{v, u\} \in Fin$
145	144	biantru	$⊢ (\{v, u\} \subseteq A \land \{v, u\} \neq \emptyset) \leftrightarrow ((\{v, u\} \subseteq A \land \{v, u\} \neq \emptyset) \land \{v, u\} \in Fin)$
146	141 143 145	3bitrri	$⊢ ((\{v, u\} \subseteq A \land \{v, u\} \neq \emptyset) \land \{v, u\} \in Fin) \leftrightarrow (v \in A \land u \in A)$
147	139 140	intpr	$⊢ ⋂ \{v, u\} = v \cap u$
148	147	eleq1i	$⊢ ⋂ \{v, u\} \in A \leftrightarrow v \cap u \in A$
149	138 146 148	3imtr3g	$⊢ \forall z (((z \subseteq A \land z \neq \emptyset) \land z \in Fin) \to ⋂ z \in A) \to ((v \in A \land u \in A) \to v \cap u \in A)$
150	149	ralrimivv	$⊢ \forall z (((z \subseteq A \land z \neq \emptyset) \land z \in Fin) \to ⋂ z \in A) \to \forall v \in A \forall u \in A v \cap u \in A$
151	128 150	impbii	$⊢ \forall v \in A \forall u \in A v \cap u \in A \leftrightarrow \forall z (((z \subseteq A \land z \neq \emptyset) \land z \in Fin) \to ⋂ z \in A)$
152		ineq1	$⊢ x = v \to x \cap y = v \cap y$
153	152	eleq1d	$⊢ x = v \to (x \cap y \in A \leftrightarrow v \cap y \in A)$
154		ineq2	$⊢ y = u \to v \cap y = v \cap u$
155	154	eleq1d	$⊢ y = u \to (v \cap y \in A \leftrightarrow v \cap u \in A)$
156	153 155	cbvral2vw	$⊢ \forall x \in A \forall y \in A x \cap y \in A \leftrightarrow \forall v \in A \forall u \in A v \cap u \in A$
157		df-3an	$⊢ (z \subseteq A \land z \neq \emptyset \land z \in Fin) \leftrightarrow ((z \subseteq A \land z \neq \emptyset) \land z \in Fin)$
158	157	imbi1i	$⊢ ((z \subseteq A \land z \neq \emptyset \land z \in Fin) \to ⋂ z \in A) \leftrightarrow (((z \subseteq A \land z \neq \emptyset) \land z \in Fin) \to ⋂ z \in A)$
159	158	albii	$⊢ \forall z ((z \subseteq A \land z \neq \emptyset \land z \in Fin) \to ⋂ z \in A) \leftrightarrow \forall z (((z \subseteq A \land z \neq \emptyset) \land z \in Fin) \to ⋂ z \in A)$
160	151 156 159	3bitr4i	$⊢ \forall x \in A \forall y \in A x \cap y \in A \leftrightarrow \forall z ((z \subseteq A \land z \neq \emptyset \land z \in Fin) \to ⋂ z \in A)$

Metamath Proof Explorer

Theorem fiint

Proof