ispisys2

Description: The property of being a pi-system, expanded version. Pi-systems are closed under finite intersections. (Contributed by Thierry Arnoux, 13-Jun-2020)

		Ref	Expression
	Hypothesis	ispisys.p	$⊢ P = \{s \in 𝒫 𝒫 O \| fi (s) \subseteq s\}$
	Assertion	ispisys2	$⊢ S \in P \leftrightarrow (S \in 𝒫 𝒫 O \land \forall x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\}) ⋂ x \in S)$

Proof

Step	Hyp	Ref	Expression
1		ispisys.p	$⊢ P = \{s \in 𝒫 𝒫 O \| fi (s) \subseteq s\}$
2	1	ispisys	$⊢ S \in P \leftrightarrow (S \in 𝒫 𝒫 O \land fi (S) \subseteq S)$
3		dfss3	$⊢ fi (S) \subseteq S \leftrightarrow \forall y \in fi (S) y \in S$
4		elex	$⊢ S \in 𝒫 𝒫 O \to S \in V$
5	4	adantr	$⊢ (S \in 𝒫 𝒫 O \land x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})) \to S \in V$
6		eldifsn	$⊢ x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\}) \leftrightarrow (x \in (𝒫 S \cap Fin) \land x \neq \emptyset)$
7	6	bilani	$⊢ (S \in 𝒫 𝒫 O \land x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})) \to (x \in (𝒫 S \cap Fin) \land x \neq \emptyset)$
8	7	simpld	$⊢ (S \in 𝒫 𝒫 O \land x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})) \to x \in (𝒫 S \cap Fin)$
9	8	elin1d	$⊢ (S \in 𝒫 𝒫 O \land x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})) \to x \in 𝒫 S$
10	9	elpwid	$⊢ (S \in 𝒫 𝒫 O \land x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})) \to x \subseteq S$
11	7	simprd	$⊢ (S \in 𝒫 𝒫 O \land x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})) \to x \neq \emptyset$
12	8	elin2d	$⊢ (S \in 𝒫 𝒫 O \land x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})) \to x \in Fin$
13		elfir	$⊢ (S \in V \land (x \subseteq S \land x \neq \emptyset \land x \in Fin)) \to ⋂ x \in fi (S)$
14	5 10 11 12 13	syl13anc	$⊢ (S \in 𝒫 𝒫 O \land x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})) \to ⋂ x \in fi (S)$
15		elfi2	$⊢ S \in 𝒫 𝒫 O \to (y \in fi (S) \leftrightarrow \exists x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\}) y = ⋂ x)$
16	15	biimpa	$⊢ (S \in 𝒫 𝒫 O \land y \in fi (S)) \to \exists x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\}) y = ⋂ x$
17		simpr	$⊢ (S \in 𝒫 𝒫 O \land y = ⋂ x) \to y = ⋂ x$
18	17	eleq1d	$⊢ (S \in 𝒫 𝒫 O \land y = ⋂ x) \to (y \in S \leftrightarrow ⋂ x \in S)$
19	14 16 18	ralxfrd	$⊢ S \in 𝒫 𝒫 O \to (\forall y \in fi (S) y \in S \leftrightarrow \forall x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\}) ⋂ x \in S)$
20	3 19	bitrid	$⊢ S \in 𝒫 𝒫 O \to (fi (S) \subseteq S \leftrightarrow \forall x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\}) ⋂ x \in S)$
21	20	pm5.32i	$⊢ (S \in 𝒫 𝒫 O \land fi (S) \subseteq S) \leftrightarrow (S \in 𝒫 𝒫 O \land \forall x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\}) ⋂ x \in S)$
22	2 21	bitri	$⊢ S \in P \leftrightarrow (S \in 𝒫 𝒫 O \land \forall x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\}) ⋂ x \in S)$

Metamath Proof Explorer

Theorem ispisys2

Proof