Theorem ispisys

Description: The property of being a pi-system. (Contributed by Thierry Arnoux, 10-Jun-2020)

	Ref	Expression
Hypothesis	ispisys.p	$$⊢P=\left\{s\in 𝒫𝒫O|\mathrm{fi}\left(s\right)\subseteq s\right\}$$
Assertion	ispisys	$$⊢S\in P\leftrightarrow \left(S\in 𝒫𝒫O\wedge \mathrm{fi}\left(S\right)\subseteq S\right)$$

Proof

Step	Hyp	Ref	Expression
1		ispisys.p	$$⊢P=\left\{s\in 𝒫𝒫O|\mathrm{fi}\left(s\right)\subseteq s\right\}$$
2		fveq2	$$⊢s=S\to \mathrm{fi}\left(s\right)=\mathrm{fi}\left(S\right)$$
3		id	$$⊢s=S\to s=S$$
4	2 3	sseq12d	$$⊢s=S\to \left(\mathrm{fi}\left(s\right)\subseteq s\leftrightarrow \mathrm{fi}\left(S\right)\subseteq S\right)$$
5	4 1	elrab2	$$⊢S\in P\leftrightarrow \left(S\in 𝒫𝒫O\wedge \mathrm{fi}\left(S\right)\subseteq S\right)$$