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 e. ~P A | ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) }
salgencntex.b 
|- B = ( 0 [,] 1 )
salgencntex.t 
|- T = ~P B
salgencntex.c 
|- C = ( S i^i T )
salgencntex.z 
|- Z = |^| { s e. SAlg | C C_ s }
Assertion salgencntex 
|- -. Z e. SAlg

Proof

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