inelpisys

Description: Pi-systems are closed under pairwise intersections. (Contributed by Thierry Arnoux, 6-Jul-2020)

		Ref	Expression
	Hypothesis	ispisys.p	$⊢ P = \{s \in 𝒫 𝒫 O \| fi (s) \subseteq s\}$
	Assertion	inelpisys	$⊢ (S \in P \land A \in S \land B \in S) \to A \cap B \in S$

Proof

Step	Hyp	Ref	Expression
1		ispisys.p	$⊢ P = \{s \in 𝒫 𝒫 O \| fi (s) \subseteq s\}$
2		intprg	$⊢ (A \in S \land B \in S) \to ⋂ \{A, B\} = A \cap B$
3	2	3adant1	$⊢ (S \in P \land A \in S \land B \in S) \to ⋂ \{A, B\} = A \cap B$
4		inteq	$⊢ x = \{A, B\} \to ⋂ x = ⋂ \{A, B\}$
5	4	eleq1d	$⊢ x = \{A, B\} \to (⋂ x \in S \leftrightarrow ⋂ \{A, B\} \in S)$
6	1	ispisys2	$⊢ S \in P \leftrightarrow (S \in 𝒫 𝒫 O \land \forall x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\}) ⋂ x \in S)$
7	6	simprbi	$⊢ S \in P \to \forall x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\}) ⋂ x \in S$
8	7	3ad2ant1	$⊢ (S \in P \land A \in S \land B \in S) \to \forall x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\}) ⋂ x \in S$
9		prelpwi	$⊢ (A \in S \land B \in S) \to \{A, B\} \in 𝒫 S$
10	9	3adant1	$⊢ (S \in P \land A \in S \land B \in S) \to \{A, B\} \in 𝒫 S$
11		prfi	$⊢ \{A, B\} \in Fin$
12	11	a1i	$⊢ (S \in P \land A \in S \land B \in S) \to \{A, B\} \in Fin$
13	10 12	elind	$⊢ (S \in P \land A \in S \land B \in S) \to \{A, B\} \in (𝒫 S \cap Fin)$
14		prnzg	$⊢ A \in S \to \{A, B\} \neq \emptyset$
15	14	3ad2ant2	$⊢ (S \in P \land A \in S \land B \in S) \to \{A, B\} \neq \emptyset$
16	15	neneqd	$⊢ (S \in P \land A \in S \land B \in S) \to \neg \{A, B\} = \emptyset$
17		elsni	$⊢ \{A, B\} \in \{\emptyset\} \to \{A, B\} = \emptyset$
18	16 17	nsyl	$⊢ (S \in P \land A \in S \land B \in S) \to \neg \{A, B\} \in \{\emptyset\}$
19	13 18	eldifd	$⊢ (S \in P \land A \in S \land B \in S) \to \{A, B\} \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})$
20	5 8 19	rspcdva	$⊢ (S \in P \land A \in S \land B \in S) \to ⋂ \{A, B\} \in S$
21	3 20	eqeltrrd	$⊢ (S \in P \land A \in S \land B \in S) \to A \cap B \in S$

Metamath Proof Explorer

Theorem inelpisys

Proof