Metamath Proof Explorer

Theorem 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 e. ~P ~P O | ( fi ` s ) C_ s }
Assertion ispisys2 
|- ( S e. P <-> ( S e. ~P ~P O /\ A. x e. ( ( ~P S i^i Fin ) \ { (/) } ) |^| x e. S ) )

Proof

Step Hyp Ref Expression
1 ispisys.p 
 |-  P = { s e. ~P ~P O | ( fi ` s ) C_ s }
2 1 ispisys 
 |-  ( S e. P <-> ( S e. ~P ~P O /\ ( fi ` S ) C_ S ) )
3 dfss3 
 |-  ( ( fi ` S ) C_ S <-> A. y e. ( fi ` S ) y e. S )
4 elex 
 |-  ( S e. ~P ~P O -> S e. _V )
5 4 adantr 
 |-  ( ( S e. ~P ~P O /\ x e. ( ( ~P S i^i Fin ) \ { (/) } ) ) -> S e. _V )
6 eldifsn 
 |-  ( x e. ( ( ~P S i^i Fin ) \ { (/) } ) <-> ( x e. ( ~P S i^i Fin ) /\ x =/= (/) ) )
7 6 bilani 
 |-  ( ( S e. ~P ~P O /\ x e. ( ( ~P S i^i Fin ) \ { (/) } ) ) -> ( x e. ( ~P S i^i Fin ) /\ x =/= (/) ) )
8 7 simpld 
 |-  ( ( S e. ~P ~P O /\ x e. ( ( ~P S i^i Fin ) \ { (/) } ) ) -> x e. ( ~P S i^i Fin ) )
9 8 elin1d 
 |-  ( ( S e. ~P ~P O /\ x e. ( ( ~P S i^i Fin ) \ { (/) } ) ) -> x e. ~P S )
10 9 elpwid 
 |-  ( ( S e. ~P ~P O /\ x e. ( ( ~P S i^i Fin ) \ { (/) } ) ) -> x C_ S )
11 7 simprd 
 |-  ( ( S e. ~P ~P O /\ x e. ( ( ~P S i^i Fin ) \ { (/) } ) ) -> x =/= (/) )
12 8 elin2d 
 |-  ( ( S e. ~P ~P O /\ x e. ( ( ~P S i^i Fin ) \ { (/) } ) ) -> x e. Fin )
13 elfir 
 |-  ( ( S e. _V /\ ( x C_ S /\ x =/= (/) /\ x e. Fin ) ) -> |^| x e. ( fi ` S ) )
14 5 10 11 12 13 syl13anc 
 |-  ( ( S e. ~P ~P O /\ x e. ( ( ~P S i^i Fin ) \ { (/) } ) ) -> |^| x e. ( fi ` S ) )
15 elfi2 
 |-  ( S e. ~P ~P O -> ( y e. ( fi ` S ) <-> E. x e. ( ( ~P S i^i Fin ) \ { (/) } ) y = |^| x ) )
16 15 biimpa 
 |-  ( ( S e. ~P ~P O /\ y e. ( fi ` S ) ) -> E. x e. ( ( ~P S i^i Fin ) \ { (/) } ) y = |^| x )
17 simpr 
 |-  ( ( S e. ~P ~P O /\ y = |^| x ) -> y = |^| x )
18 17 eleq1d 
 |-  ( ( S e. ~P ~P O /\ y = |^| x ) -> ( y e. S <-> |^| x e. S ) )
19 14 16 18 ralxfrd 
 |-  ( S e. ~P ~P O -> ( A. y e. ( fi ` S ) y e. S <-> A. x e. ( ( ~P S i^i Fin ) \ { (/) } ) |^| x e. S ) )
20 3 19 bitrid 
 |-  ( S e. ~P ~P O -> ( ( fi ` S ) C_ S <-> A. x e. ( ( ~P S i^i Fin ) \ { (/) } ) |^| x e. S ) )
21 20 pm5.32i 
 |-  ( ( S e. ~P ~P O /\ ( fi ` S ) C_ S ) <-> ( S e. ~P ~P O /\ A. x e. ( ( ~P S i^i Fin ) \ { (/) } ) |^| x e. S ) )
22 2 21 bitri 
 |-  ( S e. P <-> ( S e. ~P ~P O /\ A. x e. ( ( ~P S i^i Fin ) \ { (/) } ) |^| x e. S ) )