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)

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

Proof

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

Metamath Proof Explorer

Theorem fiint

Proof