Theorem salexct3

Description: An example of a sigma-algebra that's not closed under uncountable union. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	salexct3.a	⊢ 𝐴 = ( 0 [,] 2 )
	salexct3.s	⊢ 𝑆 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑥 ≼ ω ∨ ( 𝐴 ∖ 𝑥 ) ≼ ω ) }
	salexct3.x	⊢ 𝑋 = ran ( 𝑦 ∈ ( 0 [,] 1 ) ↦ { 𝑦 } )
Assertion	salexct3	⊢ ( 𝑆 ∈ SAlg ∧ 𝑋 ⊆ 𝑆 ∧ ¬ ∪ 𝑋 ∈ 𝑆 )

Proof

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