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 ⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
Assertion ispisys2 ( 𝑆 ∈ 𝑃 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∀ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 ispisys.p ⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
2 1 ispisys ⊢ ( 𝑆 ∈ 𝑃 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝑆 ) ⊆ 𝑆 ) )
3 dfss3 ⊢ ( ( fi ‘ 𝑆 ) ⊆ 𝑆 ↔ ∀ 𝑦 ∈ ( fi ‘ 𝑆 ) 𝑦 ∈ 𝑆 )
4 elex ⊢ ( 𝑆 ∈ 𝒫 𝒫 𝑂 → 𝑆 ∈ V )
5 4 adantr ⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ) → 𝑆 ∈ V )
6 simpr ⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) )
7 eldifsn ⊢ ( 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ↔ ( 𝑥 ∈ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑥 ≠ ∅ ) )
8 6 7 sylib ⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ) → ( 𝑥 ∈ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑥 ≠ ∅ ) )
9 8 simpld ⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ∈ ( 𝒫 𝑆 ∩ Fin ) )
10 9 elin1d ⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ∈ 𝒫 𝑆 )
11 10 elpwid ⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ⊆ 𝑆 )
12 8 simprd ⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ≠ ∅ )
13 9 elin2d ⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ) → 𝑥 ∈ Fin )
14 elfir ⊢ ( ( 𝑆 ∈ V ∧ ( 𝑥 ⊆ 𝑆 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) ) → ∩ 𝑥 ∈ ( fi ‘ 𝑆 ) )
15 5 11 12 13 14 syl13anc ⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ) → ∩ 𝑥 ∈ ( fi ‘ 𝑆 ) )
16 elfi2 ⊢ ( 𝑆 ∈ 𝒫 𝒫 𝑂 → ( 𝑦 ∈ ( fi ‘ 𝑆 ) ↔ ∃ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) 𝑦 = ∩ 𝑥 ) )
17 16 biimpa ⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑦 ∈ ( fi ‘ 𝑆 ) ) → ∃ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) 𝑦 = ∩ 𝑥 )
18 simpr ⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑦 = ∩ 𝑥 ) → 𝑦 = ∩ 𝑥 )
19 18 eleq1d ⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ 𝑦 = ∩ 𝑥 ) → ( 𝑦 ∈ 𝑆 ↔ ∩ 𝑥 ∈ 𝑆 ) )
20 15 17 19 ralxfrd ⊢ ( 𝑆 ∈ 𝒫 𝒫 𝑂 → ( ∀ 𝑦 ∈ ( fi ‘ 𝑆 ) 𝑦 ∈ 𝑆 ↔ ∀ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑆 ) )
21 3 20 syl5bb ⊢ ( 𝑆 ∈ 𝒫 𝒫 𝑂 → ( ( fi ‘ 𝑆 ) ⊆ 𝑆 ↔ ∀ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑆 ) )
22 21 pm5.32i ⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝑆 ) ⊆ 𝑆 ) ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∀ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑆 ) )
23 2 22 bitri ⊢ ( 𝑆 ∈ 𝑃 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∀ 𝑥 ∈ ( ( 𝒫 𝑆 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑆 ) )