Metamath Proof Explorer

Theorem ispisys

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

Ref Expression
Hypothesis ispisys.p 
|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }
Assertion ispisys 
|- ( S e. P <-> ( S e. ~P ~P O /\ ( fi ` S ) C_ S ) )

Proof

Step Hyp Ref Expression
1 ispisys.p 
 |-  P = { s e. ~P ~P O | ( fi ` s ) C_ s }
2 fveq2 
 |-  ( s = S -> ( fi ` s ) = ( fi ` S ) )
3 id 
 |-  ( s = S -> s = S )
4 2 3 sseq12d 
 |-  ( s = S -> ( ( fi ` s ) C_ s <-> ( fi ` S ) C_ S ) )
5 4 1 elrab2 
 |-  ( S e. P <-> ( S e. ~P ~P O /\ ( fi ` S ) C_ S ) )