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	sseldi	⊢ ( 𝑦 ∈ ( 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 ∧ ¬ 𝐺 ⊆ 𝑆 )