Theorem inelpisys

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

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

Proof

Step	Hyp	Ref	Expression
1		ispisys.p	⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
2		intprg	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) )
3	2	3adant1	⊢ ( ( 𝑆 ∈ 𝑃 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) )
4		inteq	⊢ ( 𝑥 = { 𝐴 , 𝐵 } → ∩ 𝑥 = ∩ { 𝐴 , 𝐵 } )
5	4	eleq1d	⊢ ( 𝑥 = { 𝐴 , 𝐵 } → ( ∩ 𝑥 ∈ 𝑆 ↔ ∩ { 𝐴 , 𝐵 } ∈ 𝑆 ) )
6	1	ispisys2	⊢ ( 𝑆 ∈ 𝑃 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∀ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑆 ) )
7	6	simprbi	⊢ ( 𝑆 ∈ 𝑃 → ∀ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑆 )
8	7	3ad2ant1	⊢ ( ( 𝑆 ∈ 𝑃 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ∀ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑆 )
9		prelpwi	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → { 𝐴 , 𝐵 } ∈ 𝒫 𝑆 )
10	9	3adant1	⊢ ( ( 𝑆 ∈ 𝑃 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → { 𝐴 , 𝐵 } ∈ 𝒫 𝑆 )
11		prfi	⊢ { 𝐴 , 𝐵 } ∈ Fin
12	11	a1i	⊢ ( ( 𝑆 ∈ 𝑃 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → { 𝐴 , 𝐵 } ∈ Fin )
13	10 12	elind	⊢ ( ( 𝑆 ∈ 𝑃 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → { 𝐴 , 𝐵 } ∈ ( 𝒫 𝑆 ∩ Fin ) )
14		prnzg	⊢ ( 𝐴 ∈ 𝑆 → { 𝐴 , 𝐵 } ≠ ∅ )
15	14	3ad2ant2	⊢ ( ( 𝑆 ∈ 𝑃 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → { 𝐴 , 𝐵 } ≠ ∅ )
16	15	neneqd	⊢ ( ( 𝑆 ∈ 𝑃 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ¬ { 𝐴 , 𝐵 } = ∅ )
17		elsni	⊢ ( { 𝐴 , 𝐵 } ∈ { ∅ } → { 𝐴 , 𝐵 } = ∅ )
18	16 17	nsyl	⊢ ( ( 𝑆 ∈ 𝑃 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ¬ { 𝐴 , 𝐵 } ∈ { ∅ } )
19	13 18	eldifd	⊢ ( ( 𝑆 ∈ 𝑃 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → { 𝐴 , 𝐵 } ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) )
20	5 8 19	rspcdva	⊢ ( ( 𝑆 ∈ 𝑃 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ∩ { 𝐴 , 𝐵 } ∈ 𝑆 )
21	3 20	eqeltrrd	⊢ ( ( 𝑆 ∈ 𝑃 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝑆 )