Metamath Proof Explorer

Theorem salgensscntex

Description: This counterexample shows that the sigma-algebra generated by a set is not the smallest sigma-algebra containing the set, if we consider also sigma-algebras with a larger base set. (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypotheses salgensscntex.a 
|- A = ( 0 [,] 2 )
salgensscntex.s 
|- S = { x e. ~P A | ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) }
salgensscntex.x 
|- X = ran ( y e. ( 0 [,] 1 ) |-> { y } )
salgensscntex.g 
|- G = ( SalGen ` X )
Assertion salgensscntex 
|- ( X C_ S /\ S e. SAlg /\ -. G C_ S )

Proof

Step Hyp Ref Expression
1 salgensscntex.a 
 |-  A = ( 0 [,] 2 )
2 salgensscntex.s 
 |-  S = { x e. ~P A | ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) }
3 salgensscntex.x 
 |-  X = ran ( y e. ( 0 [,] 1 ) |-> { y } )
4 salgensscntex.g 
 |-  G = ( SalGen ` X )
5 0re 
 |-  0 e. RR
6 2re 
 |-  2 e. RR
7 5 6 pm3.2i 
 |-  ( 0 e. RR /\ 2 e. RR )
8 5 leidi 
 |-  0 <_ 0
9 1le2 
 |-  1 <_ 2
10 8 9 pm3.2i 
 |-  ( 0 <_ 0 /\ 1 <_ 2 )
11 iccss 
 |-  ( ( ( 0 e. RR /\ 2 e. RR ) /\ ( 0 <_ 0 /\ 1 <_ 2 ) ) -> ( 0 [,] 1 ) C_ ( 0 [,] 2 ) )
12 7 10 11 mp2an 
 |-  ( 0 [,] 1 ) C_ ( 0 [,] 2 )
13 id 
 |-  ( y e. ( 0 [,] 1 ) -> y e. ( 0 [,] 1 ) )
14 12 13 sseldi 
 |-  ( y e. ( 0 [,] 1 ) -> y e. ( 0 [,] 2 ) )
15 14 1 eleqtrrdi 
 |-  ( y e. ( 0 [,] 1 ) -> y e. A )
16 snelpwi 
 |-  ( y e. A -> { y } e. ~P A )
17 15 16 syl 
 |-  ( y e. ( 0 [,] 1 ) -> { y } e. ~P A )
18 snfi 
 |-  { y } e. Fin
19 fict 
 |-  ( { y } e. Fin -> { y } ~<_ _om )
20 18 19 ax-mp 
 |-  { y } ~<_ _om
21 orc 
 |-  ( { y } ~<_ _om -> ( { y } ~<_ _om \/ ( A \ { y } ) ~<_ _om ) )
22 20 21 ax-mp 
 |-  ( { y } ~<_ _om \/ ( A \ { y } ) ~<_ _om )
23 22 a1i 
 |-  ( y e. ( 0 [,] 1 ) -> ( { y } ~<_ _om \/ ( A \ { y } ) ~<_ _om ) )
24 17 23 jca 
 |-  ( y e. ( 0 [,] 1 ) -> ( { y } e. ~P A /\ ( { y } ~<_ _om \/ ( A \ { y } ) ~<_ _om ) ) )
25 breq1 
 |-  ( x = { y } -> ( x ~<_ _om <-> { y } ~<_ _om ) )
26 difeq2 
 |-  ( x = { y } -> ( A \ x ) = ( A \ { y } ) )
27 26 breq1d 
 |-  ( x = { y } -> ( ( A \ x ) ~<_ _om <-> ( A \ { y } ) ~<_ _om ) )
28 25 27 orbi12d 
 |-  ( x = { y } -> ( ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) <-> ( { y } ~<_ _om \/ ( A \ { y } ) ~<_ _om ) ) )
29 28 2 elrab2 
 |-  ( { y } e. S <-> ( { y } e. ~P A /\ ( { y } ~<_ _om \/ ( A \ { y } ) ~<_ _om ) ) )
30 24 29 sylibr 
 |-  ( y e. ( 0 [,] 1 ) -> { y } e. S )
31 30 rgen 
 |-  A. y e. ( 0 [,] 1 ) { y } e. S
32 eqid 
 |-  ( y e. ( 0 [,] 1 ) |-> { y } ) = ( y e. ( 0 [,] 1 ) |-> { y } )
33 32 rnmptss 
 |-  ( A. y e. ( 0 [,] 1 ) { y } e. S -> ran ( y e. ( 0 [,] 1 ) |-> { y } ) C_ S )
34 31 33 ax-mp 
 |-  ran ( y e. ( 0 [,] 1 ) |-> { y } ) C_ S
35 3 34 eqsstri 
 |-  X C_ S
36 ovex 
 |-  ( 0 [,] 2 ) e. _V
37 1 36 eqeltri 
 |-  A e. _V
38 37 a1i 
 |-  ( T. -> A e. _V )
39 38 2 salexct 
 |-  ( T. -> S e. SAlg )
40 39 mptru 
 |-  S e. SAlg
41 ovex 
 |-  ( 0 [,] 1 ) e. _V
42 41 mptex 
 |-  ( y e. ( 0 [,] 1 ) |-> { y } ) e. _V
43 42 rnex 
 |-  ran ( y e. ( 0 [,] 1 ) |-> { y } ) e. _V
44 3 43 eqeltri 
 |-  X e. _V
45 44 a1i 
 |-  ( T. -> X e. _V )
46 3 unieqi 
 |-  U. X = U. ran ( y e. ( 0 [,] 1 ) |-> { y } )
47 snex 
 |-  { y } e. _V
48 47 rgenw 
 |-  A. y e. ( 0 [,] 1 ) { y } e. _V
49 dfiun3g 
 |-  ( A. y e. ( 0 [,] 1 ) { y } e. _V -> U_ y e. ( 0 [,] 1 ) { y } = U. ran ( y e. ( 0 [,] 1 ) |-> { y } ) )
50 48 49 ax-mp 
 |-  U_ y e. ( 0 [,] 1 ) { y } = U. ran ( y e. ( 0 [,] 1 ) |-> { y } )
51 50 eqcomi 
 |-  U. ran ( y e. ( 0 [,] 1 ) |-> { y } ) = U_ y e. ( 0 [,] 1 ) { y }
52 iunid 
 |-  U_ y e. ( 0 [,] 1 ) { y } = ( 0 [,] 1 )
53 46 51 52 3eqtrri 
 |-  ( 0 [,] 1 ) = U. X
54 45 4 53 unisalgen 
 |-  ( T. -> ( 0 [,] 1 ) e. G )
55 54 mptru 
 |-  ( 0 [,] 1 ) e. G
56 eqid 
 |-  ( 0 [,] 1 ) = ( 0 [,] 1 )
57 1 2 56 salexct2 
 |-  -. ( 0 [,] 1 ) e. S
58 nelss 
 |-  ( ( ( 0 [,] 1 ) e. G /\ -. ( 0 [,] 1 ) e. S ) -> -. G C_ S )
59 55 57 58 mp2an 
 |-  -. G C_ S
60 35 40 59 3pm3.2i 
 |-  ( X C_ S /\ S e. SAlg /\ -. G C_ S )