Metamath Proof Explorer

Theorem salexct2

Description: An example of a subset that does not belong to a nontrivial sigma-algebra, see salexct . (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypotheses salexct2.1 
|- A = ( 0 [,] 2 )
salexct2.2 
|- S = { x e. ~P A | ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) }
salexct2.3 
|- B = ( 0 [,] 1 )
Assertion salexct2 
|- -. B e. S

Proof

Step Hyp Ref Expression
1 salexct2.1 
 |-  A = ( 0 [,] 2 )
2 salexct2.2 
 |-  S = { x e. ~P A | ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) }
3 salexct2.3 
 |-  B = ( 0 [,] 1 )
4 0xr 
 |-  0 e. RR*
5 4 a1i 
 |-  ( T. -> 0 e. RR* )
6 1xr 
 |-  1 e. RR*
7 6 a1i 
 |-  ( T. -> 1 e. RR* )
8 0lt1 
 |-  0 < 1
9 8 a1i 
 |-  ( T. -> 0 < 1 )
10 5 7 9 3 iccnct 
 |-  ( T. -> -. B ~<_ _om )
11 10 mptru 
 |-  -. B ~<_ _om
12 2re 
 |-  2 e. RR
13 12 rexri 
 |-  2 e. RR*
14 13 a1i 
 |-  ( T. -> 2 e. RR* )
15 1lt2 
 |-  1 < 2
16 15 a1i 
 |-  ( T. -> 1 < 2 )
17 eqid 
 |-  ( 1 (,] 2 ) = ( 1 (,] 2 )
18 7 14 16 17 iocnct 
 |-  ( T. -> -. ( 1 (,] 2 ) ~<_ _om )
19 18 mptru 
 |-  -. ( 1 (,] 2 ) ~<_ _om
20 1 3 difeq12i 
 |-  ( A \ B ) = ( ( 0 [,] 2 ) \ ( 0 [,] 1 ) )
21 5 7 9 xrltled 
 |-  ( T. -> 0 <_ 1 )
22 5 7 14 21 iccdificc 
 |-  ( T. -> ( ( 0 [,] 2 ) \ ( 0 [,] 1 ) ) = ( 1 (,] 2 ) )
23 22 mptru 
 |-  ( ( 0 [,] 2 ) \ ( 0 [,] 1 ) ) = ( 1 (,] 2 )
24 20 23 eqtri 
 |-  ( A \ B ) = ( 1 (,] 2 )
25 24 breq1i 
 |-  ( ( A \ B ) ~<_ _om <-> ( 1 (,] 2 ) ~<_ _om )
26 19 25 mtbir 
 |-  -. ( A \ B ) ~<_ _om
27 11 26 pm3.2i 
 |-  ( -. B ~<_ _om /\ -. ( A \ B ) ~<_ _om )
28 ioran 
 |-  ( -. ( B ~<_ _om \/ ( A \ B ) ~<_ _om ) <-> ( -. B ~<_ _om /\ -. ( A \ B ) ~<_ _om ) )
29 27 28 mpbir 
 |-  -. ( B ~<_ _om \/ ( A \ B ) ~<_ _om )
30 29 intnan 
 |-  -. ( B e. ~P A /\ ( B ~<_ _om \/ ( A \ B ) ~<_ _om ) )
31 breq1 
 |-  ( x = B -> ( x ~<_ _om <-> B ~<_ _om ) )
32 difeq2 
 |-  ( x = B -> ( A \ x ) = ( A \ B ) )
33 32 breq1d 
 |-  ( x = B -> ( ( A \ x ) ~<_ _om <-> ( A \ B ) ~<_ _om ) )
34 31 33 orbi12d 
 |-  ( x = B -> ( ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) <-> ( B ~<_ _om \/ ( A \ B ) ~<_ _om ) ) )
35 34 2 elrab2 
 |-  ( B e. S <-> ( B e. ~P A /\ ( B ~<_ _om \/ ( A \ B ) ~<_ _om ) ) )
36 30 35 mtbir 
 |-  -. B e. S