Metamath Proof Explorer

Theorem inelpisys

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

Ref Expression
Hypothesis ispisys.p ⊢ P = s ∈ 𝒫 𝒫 O | fi ⁡ s ⊆ s
Assertion inelpisys ⊢ S ∈ P ∧ A ∈ S ∧ B ∈ S → A ∩ B ∈ S

Proof

Step Hyp Ref Expression
1 ispisys.p ⊢ P = s ∈ 𝒫 𝒫 O | fi ⁡ s ⊆ s
2 intprg ⊢ A ∈ S ∧ B ∈ S → ⋂ A B = A ∩ B
3 2 3adant1 ⊢ S ∈ P ∧ A ∈ S ∧ B ∈ S → ⋂ A B = A ∩ B
4 inteq ⊢ x = A B → ⋂ x = ⋂ A B
5 eqidd ⊢ x = A B → S = S
6 4 5 eleq12d ⊢ x = A B → ⋂ x ∈ S ↔ ⋂ A B ∈ S
7 1 ispisys2 ⊢ S ∈ P ↔ S ∈ 𝒫 𝒫 O ∧ ∀ x ∈ 𝒫 S ∩ Fin ∖ ∅ ⋂ x ∈ S
8 7 simprbi ⊢ S ∈ P → ∀ x ∈ 𝒫 S ∩ Fin ∖ ∅ ⋂ x ∈ S
9 8 3ad2ant1 ⊢ S ∈ P ∧ A ∈ S ∧ B ∈ S → ∀ x ∈ 𝒫 S ∩ Fin ∖ ∅ ⋂ x ∈ S
10 prssi ⊢ A ∈ S ∧ B ∈ S → A B ⊆ S
11 prex ⊢ A B ∈ V
12 11 elpw ⊢ A B ∈ 𝒫 S ↔ A B ⊆ S
13 10 12 sylibr ⊢ A ∈ S ∧ B ∈ S → A B ∈ 𝒫 S
14 13 3adant1 ⊢ S ∈ P ∧ A ∈ S ∧ B ∈ S → A B ∈ 𝒫 S
15 prfi ⊢ A B ∈ Fin
16 15 a1i ⊢ S ∈ P ∧ A ∈ S ∧ B ∈ S → A B ∈ Fin
17 14 16 elind ⊢ S ∈ P ∧ A ∈ S ∧ B ∈ S → A B ∈ 𝒫 S ∩ Fin
18 prnzg ⊢ A ∈ S → A B ≠ ∅
19 18 3ad2ant2 ⊢ S ∈ P ∧ A ∈ S ∧ B ∈ S → A B ≠ ∅
20 19 neneqd ⊢ S ∈ P ∧ A ∈ S ∧ B ∈ S → ¬ A B = ∅
21 elsni ⊢ A B ∈ ∅ → A B = ∅
22 21 con3i ⊢ ¬ A B = ∅ → ¬ A B ∈ ∅
23 20 22 syl ⊢ S ∈ P ∧ A ∈ S ∧ B ∈ S → ¬ A B ∈ ∅
24 17 23 eldifd ⊢ S ∈ P ∧ A ∈ S ∧ B ∈ S → A B ∈ 𝒫 S ∩ Fin ∖ ∅
25 6 9 24 rspcdva ⊢ S ∈ P ∧ A ∈ S ∧ B ∈ S → ⋂ A B ∈ S
26 3 25 eqeltrrd ⊢ S ∈ P ∧ A ∈ S ∧ B ∈ S → A ∩ B ∈ S