Metamath Proof Explorer


Theorem salgencntex

Description: This counterexample shows that df-salgen needs to require that all containing sigma-algebra have the same base set. Otherwise, the intersection could lead to a set that is not a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypotheses salgencntex.a A = 0 2
salgencntex.s S = x 𝒫 A | x ω A x ω
salgencntex.b B = 0 1
salgencntex.t T = 𝒫 B
salgencntex.c C = S T
salgencntex.z Z = s SAlg | C s
Assertion salgencntex ¬ Z SAlg

Proof

Step Hyp Ref Expression
1 salgencntex.a A = 0 2
2 salgencntex.s S = x 𝒫 A | x ω A x ω
3 salgencntex.b B = 0 1
4 salgencntex.t T = 𝒫 B
5 salgencntex.c C = S T
6 salgencntex.z Z = s SAlg | C s
7 saluni Z SAlg Z Z
8 ovex 0 1 V
9 3 8 eqeltri B V
10 pwsal B V 𝒫 B SAlg
11 9 10 ax-mp 𝒫 B SAlg
12 4 11 eqeltri T SAlg
13 inss2 S T T
14 5 13 eqsstri C T
15 12 14 pm3.2i T SAlg C T
16 sseq2 s = T C s C T
17 16 elrab T s SAlg | C s T SAlg C T
18 15 17 mpbir T s SAlg | C s
19 intss1 T s SAlg | C s s SAlg | C s T
20 18 19 ax-mp s SAlg | C s T
21 6 20 eqsstri Z T
22 21 unissi Z T
23 4 unieqi T = 𝒫 B
24 unipw 𝒫 B = B
25 23 24 eqtri T = B
26 22 25 sseqtri Z B
27 sseq2 s = t C s C t
28 27 elrab t s SAlg | C s t SAlg C t
29 28 biimpi t s SAlg | C s t SAlg C t
30 29 simprd t s SAlg | C s C t
31 30 adantl y B t s SAlg | C s C t
32 0red y B 0
33 2re 2
34 33 a1i y B 2
35 unitssre 0 1
36 id y B y B
37 36 3 eleqtrdi y B y 0 1
38 35 37 sseldi y B y
39 32 rexrd y B 0 *
40 1xr 1 *
41 40 a1i y B 1 *
42 iccgelb 0 * 1 * y 0 1 0 y
43 39 41 37 42 syl3anc y B 0 y
44 1re 1
45 44 a1i y B 1
46 iccleub 0 * 1 * y 0 1 y 1
47 39 41 37 46 syl3anc y B y 1
48 1le2 1 2
49 48 a1i y B 1 2
50 38 45 34 47 49 letrd y B y 2
51 32 34 38 43 50 eliccd y B y 0 2
52 51 1 eleqtrrdi y B y A
53 snelpwi y A y 𝒫 A
54 52 53 syl y B y 𝒫 A
55 snfi y Fin
56 fict y Fin y ω
57 55 56 ax-mp y ω
58 57 a1i y B y ω
59 orc y ω y ω A y ω
60 58 59 syl y B y ω A y ω
61 54 60 jca y B y 𝒫 A y ω A y ω
62 breq1 x = y x ω y ω
63 difeq2 x = y A x = A y
64 63 breq1d x = y A x ω A y ω
65 62 64 orbi12d x = y x ω A x ω y ω A y ω
66 65 2 elrab2 y S y 𝒫 A y ω A y ω
67 61 66 sylibr y B y S
68 snelpwi y B y 𝒫 B
69 68 4 eleqtrrdi y B y T
70 67 69 elind y B y S T
71 5 eqcomi S T = C
72 71 a1i y B S T = C
73 70 72 eleqtrd y B y C
74 73 adantr y B t s SAlg | C s y C
75 31 74 sseldd y B t s SAlg | C s y t
76 75 ralrimiva y B t s SAlg | C s y t
77 snex y V
78 77 elint2 y s SAlg | C s t s SAlg | C s y t
79 76 78 sylibr y B y s SAlg | C s
80 79 6 eleqtrrdi y B y Z
81 snidg y B y y
82 eleq2 w = y y w y y
83 82 rspcev y Z y y w Z y w
84 80 81 83 syl2anc y B w Z y w
85 eluni2 y Z w Z y w
86 84 85 sylibr y B y Z
87 86 rgen y B y Z
88 dfss3 B Z y B y Z
89 87 88 mpbir B Z
90 26 89 eqssi Z = B
91 ovex 0 2 V
92 1 91 eqeltri A V
93 92 a1i A V
94 93 2 salexct S SAlg
95 94 mptru S SAlg
96 inss1 S T S
97 5 96 eqsstri C S
98 95 97 pm3.2i S SAlg C S
99 sseq2 s = S C s C S
100 99 elrab S s SAlg | C s S SAlg C S
101 98 100 mpbir S s SAlg | C s
102 intss1 S s SAlg | C s s SAlg | C s S
103 101 102 ax-mp s SAlg | C s S
104 6 103 eqsstri Z S
105 104 sseli B Z B S
106 1 2 3 salexct2 ¬ B S
107 106 a1i B Z ¬ B S
108 105 107 pm2.65i ¬ B Z
109 90 108 eqneltri ¬ Z Z
110 109 a1i Z SAlg ¬ Z Z
111 7 110 pm2.65i ¬ Z SAlg