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 = 0 2
salexct3.s S = x 𝒫 A | x ω A x ω
salexct3.x X = ran y 0 1 y
Assertion salexct3 S SAlg X S ¬ X S

Proof

Step Hyp Ref Expression
1 salexct3.a A = 0 2
2 salexct3.s S = x 𝒫 A | x ω A x ω
3 salexct3.x X = ran y 0 1 y
4 ovex 0 2 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 0 1 0 2
16 11 14 15 mp2an 0 1 0 2
17 id y 0 1 y 0 1
18 16 17 sseldi y 0 1 y 0 2
19 18 1 eleqtrrdi y 0 1 y A
20 snelpwi y A y 𝒫 A
21 19 20 syl y 0 1 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 0 1 y ω A y ω
28 21 27 jca y 0 1 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 0 1 y S
35 34 rgen y 0 1 y S
36 eqid y 0 1 y = y 0 1 y
37 36 rnmptss y 0 1 y S ran y 0 1 y S
38 35 37 ax-mp ran y 0 1 y S
39 3 38 eqsstri X S
40 3 unieqi X = ran y 0 1 y
41 snex y V
42 41 rgenw y 0 1 y V
43 dfiun3g y 0 1 y V y 0 1 y = ran y 0 1 y
44 42 43 ax-mp y 0 1 y = ran y 0 1 y
45 44 eqcomi ran y 0 1 y = y 0 1 y
46 iunid y 0 1 y = 0 1
47 40 45 46 3eqtrri 0 1 = X
48 47 eqcomi X = 0 1
49 1 2 48 salexct2 ¬ X S
50 8 39 49 3pm3.2i S SAlg X S ¬ X S