Theorem inelpisys

Description: Pi-systems are closed under pairwise intersections. (Contributed by Thierry Arnoux, 6-Jul-2020)

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

Proof

Step	Hyp	Ref	Expression
1		ispisys.p	|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }
2		intprg	|- ( ( A e. S /\ B e. S ) -> |^| { A , B } = ( A i^i B ) )
3	2	3adant1	|- ( ( S e. P /\ A e. S /\ B e. S ) -> |^| { A , B } = ( A i^i B ) )
4		inteq	|- ( x = { A , B } -> |^| x = |^| { A , B } )
5	4	eleq1d	|- ( x = { A , B } -> ( |^| x e. S <-> |^| { A , B } e. S ) )
6	1	ispisys2	|- ( S e. P <-> ( S e. ~P ~P O /\ A. x e. ( ( ~P S i^i Fin ) \ { (/) } ) |^| x e. S ) )
7	6	simprbi	|- ( S e. P -> A. x e. ( ( ~P S i^i Fin ) \ { (/) } ) |^| x e. S )
8	7	3ad2ant1	|- ( ( S e. P /\ A e. S /\ B e. S ) -> A. x e. ( ( ~P S i^i Fin ) \ { (/) } ) |^| x e. S )
9		prelpwi	|- ( ( A e. S /\ B e. S ) -> { A , B } e. ~P S )
10	9	3adant1	|- ( ( S e. P /\ A e. S /\ B e. S ) -> { A , B } e. ~P S )
11		prfi	|- { A , B } e. Fin
12	11	a1i	|- ( ( S e. P /\ A e. S /\ B e. S ) -> { A , B } e. Fin )
13	10 12	elind	|- ( ( S e. P /\ A e. S /\ B e. S ) -> { A , B } e. ( ~P S i^i Fin ) )
14		prnzg	|- ( A e. S -> { A , B } =/= (/) )
15	14	3ad2ant2	|- ( ( S e. P /\ A e. S /\ B e. S ) -> { A , B } =/= (/) )
16	15	neneqd	|- ( ( S e. P /\ A e. S /\ B e. S ) -> -. { A , B } = (/) )
17		elsni	|- ( { A , B } e. { (/) } -> { A , B } = (/) )
18	16 17	nsyl	|- ( ( S e. P /\ A e. S /\ B e. S ) -> -. { A , B } e. { (/) } )
19	13 18	eldifd	|- ( ( S e. P /\ A e. S /\ B e. S ) -> { A , B } e. ( ( ~P S i^i Fin ) \ { (/) } ) )
20	5 8 19	rspcdva	|- ( ( S e. P /\ A e. S /\ B e. S ) -> |^| { A , B } e. S )
21	3 20	eqeltrrd	|- ( ( S e. P /\ A e. S /\ B e. S ) -> ( A i^i B ) e. S )