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 e. ~P A | ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) }
salexct3.x 
|- X = ran ( y e. ( 0 [,] 1 ) |-> { y } )
Assertion salexct3 
|- ( S e. SAlg /\ X C_ S /\ -. U. X e. S )

Proof

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