Metamath Proof Explorer

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 ⊢A=02
salexct3.s ⊢S=x∈𝒫A|x≼ω∨A∖x≼ω
salexct3.x ⊢X=ran⁡y∈01⟼y
Assertion salexct3 ⊢S∈SAlg∧X⊆S∧¬⋃X∈S

Proof

Step Hyp Ref Expression
1 salexct3.a ⊢A=02
2 salexct3.s ⊢S=x∈𝒫A|x≼ω∨A∖x≼ω
3 salexct3.x ⊢X=ran⁡y∈01⟼y
4 ovex ⊢02∈V
5 1 4 eqeltri ⊢A∈V
6 5 a1i ⊢⊤→A∈V
7 6 2 salexct ⊢⊤→S∈SAlg
8 7 mptru ⊢S∈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→01⊆02
16 11 14 15 mp2an ⊢01⊆02
17 id ⊢y∈01→y∈01
18 16 17 sselid ⊢y∈01→y∈02
19 18 1 eleqtrrdi ⊢y∈01→y∈A
20 snelpwi ⊢y∈A→y∈𝒫A
21 19 20 syl ⊢y∈01→y∈𝒫A
22 snfi ⊢y∈Fin
23 fict ⊢y∈Fin→y≼ω
24 22 23 ax-mp ⊢y≼ω
25 orc ⊢y≼ω→y≼ω∨A∖y≼ω
26 24 25 ax-mp ⊢y≼ω∨A∖y≼ω
27 26 a1i ⊢y∈01→y≼ω∨A∖y≼ω
28 21 27 jca ⊢y∈01→y∈𝒫A∧y≼ω∨A∖y≼ω
29 breq1 ⊢x=y→x≼ω↔y≼ω
30 difeq2 ⊢x=y→A∖x=A∖y
31 30 breq1d ⊢x=y→A∖x≼ω↔A∖y≼ω
32 29 31 orbi12d ⊢x=y→x≼ω∨A∖x≼ω↔y≼ω∨A∖y≼ω
33 32 2 elrab2 ⊢y∈S↔y∈𝒫A∧y≼ω∨A∖y≼ω
34 28 33 sylibr ⊢y∈01→y∈S
35 34 rgen ⊢∀y∈01y∈S
36 eqid ⊢y∈01⟼y=y∈01⟼y
37 36 rnmptss ⊢∀y∈01y∈S→ran⁡y∈01⟼y⊆S
38 35 37 ax-mp ⊢ran⁡y∈01⟼y⊆S
39 3 38 eqsstri ⊢X⊆S
40 3 unieqi ⊢⋃X=⋃ran⁡y∈01⟼y
41 vsnex ⊢y∈V
42 41 rgenw ⊢∀y∈01y∈V
43 dfiun3g ⊢∀y∈01y∈V→⋃y∈01y=⋃ran⁡y∈01⟼y
44 42 43 ax-mp ⊢⋃y∈01y=⋃ran⁡y∈01⟼y
45 44 eqcomi ⊢⋃ran⁡y∈01⟼y=⋃y∈01y
46 iunid ⊢⋃y∈01y=01
47 40 45 46 3eqtrri ⊢01=⋃X
48 47 eqcomi ⊢⋃X=01
49 1 2 48 salexct2 ⊢¬⋃X∈S
50 8 39 49 3pm3.2i ⊢S∈SAlg∧X⊆S∧¬⋃X∈S