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		simpr	$⊢ (S \in 𝒫 𝒫 O \land x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})) \to x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})$
7		eldifsn	$⊢ x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\}) \leftrightarrow (x \in (𝒫 S \cap Fin) \land x \neq \emptyset)$
8	6 7	sylib	$⊢ (S \in 𝒫 𝒫 O \land x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})) \to (x \in (𝒫 S \cap Fin) \land x \neq \emptyset)$
9	8	simpld	$⊢ (S \in 𝒫 𝒫 O \land x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})) \to x \in (𝒫 S \cap Fin)$
10	9	elin1d	$⊢ (S \in 𝒫 𝒫 O \land x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})) \to x \in 𝒫 S$
11	10	elpwid	$⊢ (S \in 𝒫 𝒫 O \land x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})) \to x \subseteq S$
12	8	simprd	$⊢ (S \in 𝒫 𝒫 O \land x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})) \to x \neq \emptyset$
13	9	elin2d	$⊢ (S \in 𝒫 𝒫 O \land x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})) \to x \in Fin$
14		elfir	$⊢ (S \in V \land (x \subseteq S \land x \neq \emptyset \land x \in Fin)) \to ⋂ x \in fi (S)$
15	5 11 12 13 14	syl13anc	$⊢ (S \in 𝒫 𝒫 O \land x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\})) \to ⋂ x \in fi (S)$
16		elfi2	$⊢ S \in 𝒫 𝒫 O \to (y \in fi (S) \leftrightarrow \exists x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\}) y = ⋂ x)$
17	16	biimpa	$⊢ (S \in 𝒫 𝒫 O \land y \in fi (S)) \to \exists x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\}) y = ⋂ x$
18		simpr	$⊢ (S \in 𝒫 𝒫 O \land y = ⋂ x) \to y = ⋂ x$
19	18	eleq1d	$⊢ (S \in 𝒫 𝒫 O \land y = ⋂ x) \to (y \in S \leftrightarrow ⋂ x \in S)$
20	15 17 19	ralxfrd	$⊢ S \in 𝒫 𝒫 O \to (\forall y \in fi (S) y \in S \leftrightarrow \forall x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\}) ⋂ x \in S)$
21	3 20	syl5bb	$⊢ S \in 𝒫 𝒫 O \to (fi (S) \subseteq S \leftrightarrow \forall x \in ((𝒫 S \cap Fin) ∖ \{\emptyset\}) ⋂ x \in S)$
22	21	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)$
23	2 22	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