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 simpr 
 |-  ( ( S e. ~P ~P O /\ x e. ( ( ~P S i^i Fin ) \ { (/) } ) ) -> x e. ( ( ~P S i^i Fin ) \ { (/) } ) )
7 eldifsn 
 |-  ( x e. ( ( ~P S i^i Fin ) \ { (/) } ) <-> ( x e. ( ~P S i^i Fin ) /\ x =/= (/) ) )
8 6 7 sylib 
 |-  ( ( S e. ~P ~P O /\ x e. ( ( ~P S i^i Fin ) \ { (/) } ) ) -> ( x e. ( ~P S i^i Fin ) /\ x =/= (/) ) )
9 8 simpld 
 |-  ( ( S e. ~P ~P O /\ x e. ( ( ~P S i^i Fin ) \ { (/) } ) ) -> x e. ( ~P S i^i Fin ) )
10 9 elin1d 
 |-  ( ( S e. ~P ~P O /\ x e. ( ( ~P S i^i Fin ) \ { (/) } ) ) -> x e. ~P S )
11 10 elpwid 
 |-  ( ( S e. ~P ~P O /\ x e. ( ( ~P S i^i Fin ) \ { (/) } ) ) -> x C_ S )
12 8 simprd 
 |-  ( ( S e. ~P ~P O /\ x e. ( ( ~P S i^i Fin ) \ { (/) } ) ) -> x =/= (/) )
13 9 elin2d 
 |-  ( ( S e. ~P ~P O /\ x e. ( ( ~P S i^i Fin ) \ { (/) } ) ) -> x e. Fin )
14 elfir 
 |-  ( ( S e. _V /\ ( x C_ S /\ x =/= (/) /\ x e. Fin ) ) -> |^| x e. ( fi ` S ) )
15 5 11 12 13 14 syl13anc 
 |-  ( ( S e. ~P ~P O /\ x e. ( ( ~P S i^i Fin ) \ { (/) } ) ) -> |^| x e. ( fi ` S ) )
16 elfi2 
 |-  ( S e. ~P ~P O -> ( y e. ( fi ` S ) <-> E. x e. ( ( ~P S i^i Fin ) \ { (/) } ) y = |^| x ) )
17 16 biimpa 
 |-  ( ( S e. ~P ~P O /\ y e. ( fi ` S ) ) -> E. x e. ( ( ~P S i^i Fin ) \ { (/) } ) y = |^| x )
18 simpr 
 |-  ( ( S e. ~P ~P O /\ y = |^| x ) -> y = |^| x )
19 18 eleq1d 
 |-  ( ( S e. ~P ~P O /\ y = |^| x ) -> ( y e. S <-> |^| x e. S ) )
20 15 17 19 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 ) )
21 3 20 bitrid 
 |-  ( S e. ~P ~P O -> ( ( fi ` S ) C_ S <-> A. x e. ( ( ~P S i^i Fin ) \ { (/) } ) |^| x e. S ) )
22 21 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 ) )
23 2 22 bitri 
 |-  ( S e. P <-> ( S e. ~P ~P O /\ A. x e. ( ( ~P S i^i Fin ) \ { (/) } ) |^| x e. S ) )