Theorem ispisys

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

	Ref	Expression
Hypothesis	ispisys.p	⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
Assertion	ispisys	⊢ ( 𝑆 ∈ 𝑃 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝑆 ) ⊆ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		ispisys.p	⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
2		fveq2	⊢ ( 𝑠 = 𝑆 → ( fi ‘ 𝑠 ) = ( fi ‘ 𝑆 ) )
3		id	⊢ ( 𝑠 = 𝑆 → 𝑠 = 𝑆 )
4	2 3	sseq12d	⊢ ( 𝑠 = 𝑆 → ( ( fi ‘ 𝑠 ) ⊆ 𝑠 ↔ ( fi ‘ 𝑆 ) ⊆ 𝑆 ) )
5	4 1	elrab2	⊢ ( 𝑆 ∈ 𝑃 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝑆 ) ⊆ 𝑆 ) )