Metamath Proof Explorer

Theorem issalgend

Description: One side of dfsalgen2 . If a sigma-algebra on U. X includes X and it is included in all the sigma-algebras with such two properties, then it is the sigma-algebra generated by X . (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypotheses issalgend.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
issalgend.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
issalgend.u ⊢ ( 𝜑 → ∪ 𝑆 = ∪ 𝑋 )
issalgend.i ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
issalgend.a ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ SAlg ∧ ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) ) → 𝑆 ⊆ 𝑦 )
Assertion issalgend ( 𝜑 → ( SalGen ‘ 𝑋 ) = 𝑆 )

Proof

Step Hyp Ref Expression
1 issalgend.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 issalgend.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3 issalgend.u ⊢ ( 𝜑 → ∪ 𝑆 = ∪ 𝑋 )
4 issalgend.i ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
5 issalgend.a ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ SAlg ∧ ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) ) → 𝑆 ⊆ 𝑦 )
6 eqid ⊢ ( SalGen ‘ 𝑋 ) = ( SalGen ‘ 𝑋 )
7 1 6 2 4 3 salgenss ⊢ ( 𝜑 → ( SalGen ‘ 𝑋 ) ⊆ 𝑆 )
8 simpl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ) → 𝜑 )
9 elrabi ⊢ ( 𝑦 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } → 𝑦 ∈ SAlg )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ) → 𝑦 ∈ SAlg )
11 unieq ⊢ ( 𝑠 = 𝑦 → ∪ 𝑠 = ∪ 𝑦 )
12 11 eqeq1d ⊢ ( 𝑠 = 𝑦 → ( ∪ 𝑠 = ∪ 𝑋 ↔ ∪ 𝑦 = ∪ 𝑋 ) )
13 sseq2 ⊢ ( 𝑠 = 𝑦 → ( 𝑋 ⊆ 𝑠 ↔ 𝑋 ⊆ 𝑦 ) )
14 12 13 anbi12d ⊢ ( 𝑠 = 𝑦 → ( ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) ↔ ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) ) )
15 14 elrab ⊢ ( 𝑦 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ↔ ( 𝑦 ∈ SAlg ∧ ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) ) )
16 15 biimpi ⊢ ( 𝑦 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } → ( 𝑦 ∈ SAlg ∧ ( ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦 ) ) )
17 16 simprld ⊢ ( 𝑦 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } → ∪ 𝑦 = ∪ 𝑋 )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ) → ∪ 𝑦 = ∪ 𝑋 )
19 16 simprrd ⊢ ( 𝑦 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } → 𝑋 ⊆ 𝑦 )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ) → 𝑋 ⊆ 𝑦 )
21 8 10 18 20 5 syl13anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ) → 𝑆 ⊆ 𝑦 )
22 21 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } 𝑆 ⊆ 𝑦 )
23 ssint ⊢ ( 𝑆 ⊆ ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ↔ ∀ 𝑦 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } 𝑆 ⊆ 𝑦 )
24 22 23 sylibr ⊢ ( 𝜑 → 𝑆 ⊆ ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
25 salgenval ⊢ ( 𝑋 ∈ 𝑉 → ( SalGen ‘ 𝑋 ) = ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
26 1 25 syl ⊢ ( 𝜑 → ( SalGen ‘ 𝑋 ) = ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
27 24 26 sseqtrrd ⊢ ( 𝜑 → 𝑆 ⊆ ( SalGen ‘ 𝑋 ) )
28 7 27 eqssd ⊢ ( 𝜑 → ( SalGen ‘ 𝑋 ) = 𝑆 )