Metamath Proof Explorer


Theorem salgensscntex

Description: This counterexample shows that the sigma-algebra generated by a set is not the smallest sigma-algebra containing the set, if we consider also sigma-algebras with a larger base set. (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypotheses salgensscntex.a 𝐴 = ( 0 [,] 2 )
salgensscntex.s 𝑆 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑥 ≼ ω ∨ ( 𝐴𝑥 ) ≼ ω ) }
salgensscntex.x 𝑋 = ran ( 𝑦 ∈ ( 0 [,] 1 ) ↦ { 𝑦 } )
salgensscntex.g 𝐺 = ( SalGen ‘ 𝑋 )
Assertion salgensscntex ( 𝑋𝑆𝑆 ∈ SAlg ∧ ¬ 𝐺𝑆 )

Proof

Step Hyp Ref Expression
1 salgensscntex.a 𝐴 = ( 0 [,] 2 )
2 salgensscntex.s 𝑆 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑥 ≼ ω ∨ ( 𝐴𝑥 ) ≼ ω ) }
3 salgensscntex.x 𝑋 = ran ( 𝑦 ∈ ( 0 [,] 1 ) ↦ { 𝑦 } )
4 salgensscntex.g 𝐺 = ( SalGen ‘ 𝑋 )
5 0re 0 ∈ ℝ
6 2re 2 ∈ ℝ
7 5 6 pm3.2i ( 0 ∈ ℝ ∧ 2 ∈ ℝ )
8 5 leidi 0 ≤ 0
9 1le2 1 ≤ 2
10 8 9 pm3.2i ( 0 ≤ 0 ∧ 1 ≤ 2 )
11 iccss ( ( ( 0 ∈ ℝ ∧ 2 ∈ ℝ ) ∧ ( 0 ≤ 0 ∧ 1 ≤ 2 ) ) → ( 0 [,] 1 ) ⊆ ( 0 [,] 2 ) )
12 7 10 11 mp2an ( 0 [,] 1 ) ⊆ ( 0 [,] 2 )
13 id ( 𝑦 ∈ ( 0 [,] 1 ) → 𝑦 ∈ ( 0 [,] 1 ) )
14 12 13 sselid ( 𝑦 ∈ ( 0 [,] 1 ) → 𝑦 ∈ ( 0 [,] 2 ) )
15 14 1 eleqtrrdi ( 𝑦 ∈ ( 0 [,] 1 ) → 𝑦𝐴 )
16 snelpwi ( 𝑦𝐴 → { 𝑦 } ∈ 𝒫 𝐴 )
17 15 16 syl ( 𝑦 ∈ ( 0 [,] 1 ) → { 𝑦 } ∈ 𝒫 𝐴 )
18 snfi { 𝑦 } ∈ Fin
19 fict ( { 𝑦 } ∈ Fin → { 𝑦 } ≼ ω )
20 18 19 ax-mp { 𝑦 } ≼ ω
21 orc ( { 𝑦 } ≼ ω → ( { 𝑦 } ≼ ω ∨ ( 𝐴 ∖ { 𝑦 } ) ≼ ω ) )
22 20 21 ax-mp ( { 𝑦 } ≼ ω ∨ ( 𝐴 ∖ { 𝑦 } ) ≼ ω )
23 22 a1i ( 𝑦 ∈ ( 0 [,] 1 ) → ( { 𝑦 } ≼ ω ∨ ( 𝐴 ∖ { 𝑦 } ) ≼ ω ) )
24 17 23 jca ( 𝑦 ∈ ( 0 [,] 1 ) → ( { 𝑦 } ∈ 𝒫 𝐴 ∧ ( { 𝑦 } ≼ ω ∨ ( 𝐴 ∖ { 𝑦 } ) ≼ ω ) ) )
25 breq1 ( 𝑥 = { 𝑦 } → ( 𝑥 ≼ ω ↔ { 𝑦 } ≼ ω ) )
26 difeq2 ( 𝑥 = { 𝑦 } → ( 𝐴𝑥 ) = ( 𝐴 ∖ { 𝑦 } ) )
27 26 breq1d ( 𝑥 = { 𝑦 } → ( ( 𝐴𝑥 ) ≼ ω ↔ ( 𝐴 ∖ { 𝑦 } ) ≼ ω ) )
28 25 27 orbi12d ( 𝑥 = { 𝑦 } → ( ( 𝑥 ≼ ω ∨ ( 𝐴𝑥 ) ≼ ω ) ↔ ( { 𝑦 } ≼ ω ∨ ( 𝐴 ∖ { 𝑦 } ) ≼ ω ) ) )
29 28 2 elrab2 ( { 𝑦 } ∈ 𝑆 ↔ ( { 𝑦 } ∈ 𝒫 𝐴 ∧ ( { 𝑦 } ≼ ω ∨ ( 𝐴 ∖ { 𝑦 } ) ≼ ω ) ) )
30 24 29 sylibr ( 𝑦 ∈ ( 0 [,] 1 ) → { 𝑦 } ∈ 𝑆 )
31 30 rgen 𝑦 ∈ ( 0 [,] 1 ) { 𝑦 } ∈ 𝑆
32 eqid ( 𝑦 ∈ ( 0 [,] 1 ) ↦ { 𝑦 } ) = ( 𝑦 ∈ ( 0 [,] 1 ) ↦ { 𝑦 } )
33 32 rnmptss ( ∀ 𝑦 ∈ ( 0 [,] 1 ) { 𝑦 } ∈ 𝑆 → ran ( 𝑦 ∈ ( 0 [,] 1 ) ↦ { 𝑦 } ) ⊆ 𝑆 )
34 31 33 ax-mp ran ( 𝑦 ∈ ( 0 [,] 1 ) ↦ { 𝑦 } ) ⊆ 𝑆
35 3 34 eqsstri 𝑋𝑆
36 ovex ( 0 [,] 2 ) ∈ V
37 1 36 eqeltri 𝐴 ∈ V
38 37 a1i ( ⊤ → 𝐴 ∈ V )
39 38 2 salexct ( ⊤ → 𝑆 ∈ SAlg )
40 39 mptru 𝑆 ∈ SAlg
41 ovex ( 0 [,] 1 ) ∈ V
42 41 mptex ( 𝑦 ∈ ( 0 [,] 1 ) ↦ { 𝑦 } ) ∈ V
43 42 rnex ran ( 𝑦 ∈ ( 0 [,] 1 ) ↦ { 𝑦 } ) ∈ V
44 3 43 eqeltri 𝑋 ∈ V
45 44 a1i ( ⊤ → 𝑋 ∈ V )
46 3 unieqi 𝑋 = ran ( 𝑦 ∈ ( 0 [,] 1 ) ↦ { 𝑦 } )
47 snex { 𝑦 } ∈ V
48 47 rgenw 𝑦 ∈ ( 0 [,] 1 ) { 𝑦 } ∈ V
49 dfiun3g ( ∀ 𝑦 ∈ ( 0 [,] 1 ) { 𝑦 } ∈ V → 𝑦 ∈ ( 0 [,] 1 ) { 𝑦 } = ran ( 𝑦 ∈ ( 0 [,] 1 ) ↦ { 𝑦 } ) )
50 48 49 ax-mp 𝑦 ∈ ( 0 [,] 1 ) { 𝑦 } = ran ( 𝑦 ∈ ( 0 [,] 1 ) ↦ { 𝑦 } )
51 50 eqcomi ran ( 𝑦 ∈ ( 0 [,] 1 ) ↦ { 𝑦 } ) = 𝑦 ∈ ( 0 [,] 1 ) { 𝑦 }
52 iunid 𝑦 ∈ ( 0 [,] 1 ) { 𝑦 } = ( 0 [,] 1 )
53 46 51 52 3eqtrri ( 0 [,] 1 ) = 𝑋
54 45 4 53 unisalgen ( ⊤ → ( 0 [,] 1 ) ∈ 𝐺 )
55 54 mptru ( 0 [,] 1 ) ∈ 𝐺
56 eqid ( 0 [,] 1 ) = ( 0 [,] 1 )
57 1 2 56 salexct2 ¬ ( 0 [,] 1 ) ∈ 𝑆
58 nelss ( ( ( 0 [,] 1 ) ∈ 𝐺 ∧ ¬ ( 0 [,] 1 ) ∈ 𝑆 ) → ¬ 𝐺𝑆 )
59 55 57 58 mp2an ¬ 𝐺𝑆
60 35 40 59 3pm3.2i ( 𝑋𝑆𝑆 ∈ SAlg ∧ ¬ 𝐺𝑆 )