fiinfi

Description: If two classes have the finite intersection property, then so does their intersection. (Contributed by RP, 1-Jan-2020)

	Ref	Expression
Hypotheses	fiinfi.a	$⊢ φ \to \forall x \in A \forall y \in A x \cap y \in A$
	fiinfi.b	$⊢ φ \to \forall x \in B \forall y \in B x \cap y \in B$
	fiinfi.c	$⊢ φ \to C = A \cap B$
Assertion	fiinfi	$⊢ φ \to \forall x \in C \forall y \in C x \cap y \in C$

Proof

Step	Hyp	Ref	Expression
1		fiinfi.a	$⊢ φ \to \forall x \in A \forall y \in A x \cap y \in A$
2		fiinfi.b	$⊢ φ \to \forall x \in B \forall y \in B x \cap y \in B$
3		fiinfi.c	$⊢ φ \to C = A \cap B$
4		elinel1	$⊢ x \in (A \cap B) \to x \in A$
5		elinel1	$⊢ y \in (A \cap B) \to y \in A$
6	5	imim1i	$⊢ (y \in A \to x \cap y \in A) \to (y \in (A \cap B) \to x \cap y \in A)$
7	6	ralimi2	$⊢ \forall y \in A x \cap y \in A \to \forall y \in (A \cap B) x \cap y \in A$
8	4 7	imim12i	$⊢ (x \in A \to \forall y \in A x \cap y \in A) \to (x \in (A \cap B) \to \forall y \in (A \cap B) x \cap y \in A)$
9	8	ralimi2	$⊢ \forall x \in A \forall y \in A x \cap y \in A \to \forall x \in (A \cap B) \forall y \in (A \cap B) x \cap y \in A$
10	1 9	syl	$⊢ φ \to \forall x \in (A \cap B) \forall y \in (A \cap B) x \cap y \in A$
11		elinel2	$⊢ x \in (A \cap B) \to x \in B$
12		elinel2	$⊢ y \in (A \cap B) \to y \in B$
13	12	imim1i	$⊢ (y \in B \to x \cap y \in B) \to (y \in (A \cap B) \to x \cap y \in B)$
14	13	ralimi2	$⊢ \forall y \in B x \cap y \in B \to \forall y \in (A \cap B) x \cap y \in B$
15	11 14	imim12i	$⊢ (x \in B \to \forall y \in B x \cap y \in B) \to (x \in (A \cap B) \to \forall y \in (A \cap B) x \cap y \in B)$
16	15	ralimi2	$⊢ \forall x \in B \forall y \in B x \cap y \in B \to \forall x \in (A \cap B) \forall y \in (A \cap B) x \cap y \in B$
17	2 16	syl	$⊢ φ \to \forall x \in (A \cap B) \forall y \in (A \cap B) x \cap y \in B$
18		r19.26-2	$⊢ \forall x \in (A \cap B) \forall y \in (A \cap B) (x \cap y \in A \land x \cap y \in B) \leftrightarrow (\forall x \in (A \cap B) \forall y \in (A \cap B) x \cap y \in A \land \forall x \in (A \cap B) \forall y \in (A \cap B) x \cap y \in B)$
19	10 17 18	sylanbrc	$⊢ φ \to \forall x \in (A \cap B) \forall y \in (A \cap B) (x \cap y \in A \land x \cap y \in B)$
20		elin	$⊢ x \cap y \in (A \cap B) \leftrightarrow (x \cap y \in A \land x \cap y \in B)$
21	20	2ralbii	$⊢ \forall x \in (A \cap B) \forall y \in (A \cap B) x \cap y \in (A \cap B) \leftrightarrow \forall x \in (A \cap B) \forall y \in (A \cap B) (x \cap y \in A \land x \cap y \in B)$
22	19 21	sylibr	$⊢ φ \to \forall x \in (A \cap B) \forall y \in (A \cap B) x \cap y \in (A \cap B)$
23	3	eleq2d	$⊢ φ \to (x \cap y \in C \leftrightarrow x \cap y \in (A \cap B))$
24	23	ralbidv	$⊢ φ \to (\forall y \in (A \cap B) x \cap y \in C \leftrightarrow \forall y \in (A \cap B) x \cap y \in (A \cap B))$
25	24	ralbidv	$⊢ φ \to (\forall x \in (A \cap B) \forall y \in (A \cap B) x \cap y \in C \leftrightarrow \forall x \in (A \cap B) \forall y \in (A \cap B) x \cap y \in (A \cap B))$
26	22 25	mpbird	$⊢ φ \to \forall x \in (A \cap B) \forall y \in (A \cap B) x \cap y \in C$
27	3	raleqdv	$⊢ φ \to (\forall y \in C x \cap y \in C \leftrightarrow \forall y \in (A \cap B) x \cap y \in C)$
28	27	ralbidv	$⊢ φ \to (\forall x \in (A \cap B) \forall y \in C x \cap y \in C \leftrightarrow \forall x \in (A \cap B) \forall y \in (A \cap B) x \cap y \in C)$
29	26 28	mpbird	$⊢ φ \to \forall x \in (A \cap B) \forall y \in C x \cap y \in C$
30	3	raleqdv	$⊢ φ \to (\forall x \in C \forall y \in C x \cap y \in C \leftrightarrow \forall x \in (A \cap B) \forall y \in C x \cap y \in C)$
31	29 30	mpbird	$⊢ φ \to \forall x \in C \forall y \in C x \cap y \in C$

Metamath Proof Explorer

Theorem fiinfi

Proof