Metamath Proof Explorer

Theorem salexct

Description: An example of nontrivial sigma-algebra: the collection of all subsets which either are countable or have countable complement. (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypotheses salexct.a 
|- ( ph -> A e. V )
salexct.b 
|- S = { x e. ~P A | ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) }
Assertion salexct 
|- ( ph -> S e. SAlg )

Proof

Step Hyp Ref Expression
1 salexct.a 
 |-  ( ph -> A e. V )
2 salexct.b 
 |-  S = { x e. ~P A | ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) }
3 1 pwexd 
 |-  ( ph -> ~P A e. _V )
4 rabexg 
 |-  ( ~P A e. _V -> { x e. ~P A | ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) } e. _V )
5 3 4 syl 
 |-  ( ph -> { x e. ~P A | ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) } e. _V )
6 2 5 eqeltrid 
 |-  ( ph -> S e. _V )
7 0elpw 
 |-  (/) e. ~P A
8 7 a1i 
 |-  ( ph -> (/) e. ~P A )
9 0fin 
 |-  (/) e. Fin
10 fict 
 |-  ( (/) e. Fin -> (/) ~<_ _om )
11 9 10 ax-mp 
 |-  (/) ~<_ _om
12 11 orci 
 |-  ( (/) ~<_ _om \/ ( A \ (/) ) ~<_ _om )
13 12 a1i 
 |-  ( ph -> ( (/) ~<_ _om \/ ( A \ (/) ) ~<_ _om ) )
14 8 13 jca 
 |-  ( ph -> ( (/) e. ~P A /\ ( (/) ~<_ _om \/ ( A \ (/) ) ~<_ _om ) ) )
15 breq1 
 |-  ( x = (/) -> ( x ~<_ _om <-> (/) ~<_ _om ) )
16 difeq2 
 |-  ( x = (/) -> ( A \ x ) = ( A \ (/) ) )
17 16 breq1d 
 |-  ( x = (/) -> ( ( A \ x ) ~<_ _om <-> ( A \ (/) ) ~<_ _om ) )
18 15 17 orbi12d 
 |-  ( x = (/) -> ( ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) <-> ( (/) ~<_ _om \/ ( A \ (/) ) ~<_ _om ) ) )
19 18 2 elrab2 
 |-  ( (/) e. S <-> ( (/) e. ~P A /\ ( (/) ~<_ _om \/ ( A \ (/) ) ~<_ _om ) ) )
20 14 19 sylibr 
 |-  ( ph -> (/) e. S )
21 snidg 
 |-  ( y e. A -> y e. { y } )
22 snelpwi 
 |-  ( y e. A -> { y } e. ~P A )
23 snfi 
 |-  { y } e. Fin
24 fict 
 |-  ( { y } e. Fin -> { y } ~<_ _om )
25 23 24 ax-mp 
 |-  { y } ~<_ _om
26 25 orci 
 |-  ( { y } ~<_ _om \/ ( A \ { y } ) ~<_ _om )
27 26 a1i 
 |-  ( y e. A -> ( { y } ~<_ _om \/ ( A \ { y } ) ~<_ _om ) )
28 22 27 jca 
 |-  ( y e. A -> ( { 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. A -> { y } e. S )
35 elunii 
 |-  ( ( y e. { y } /\ { y } e. S ) -> y e. U. S )
36 21 34 35 syl2anc 
 |-  ( y e. A -> y e. U. S )
37 36 rgen 
 |-  A. y e. A y e. U. S
38 dfss3 
 |-  ( A C_ U. S <-> A. y e. A y e. U. S )
39 37 38 mpbir 
 |-  A C_ U. S
40 ssrab2 
 |-  { x e. ~P A | ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) } C_ ~P A
41 2 40 eqsstri 
 |-  S C_ ~P A
42 41 unissi 
 |-  U. S C_ U. ~P A
43 unipw 
 |-  U. ~P A = A
44 42 43 sseqtri 
 |-  U. S C_ A
45 39 44 eqssi 
 |-  A = U. S
46 difssd 
 |-  ( ph -> ( A \ x ) C_ A )
47 1 46 ssexd 
 |-  ( ph -> ( A \ x ) e. _V )
48 elpwg 
 |-  ( ( A \ x ) e. _V -> ( ( A \ x ) e. ~P A <-> ( A \ x ) C_ A ) )
49 47 48 syl 
 |-  ( ph -> ( ( A \ x ) e. ~P A <-> ( A \ x ) C_ A ) )
50 46 49 mpbird 
 |-  ( ph -> ( A \ x ) e. ~P A )
51 50 ad2antrr 
 |-  ( ( ( ph /\ x e. S ) /\ x ~<_ _om ) -> ( A \ x ) e. ~P A )
52 41 sseli 
 |-  ( x e. S -> x e. ~P A )
53 elpwi 
 |-  ( x e. ~P A -> x C_ A )
54 52 53 syl 
 |-  ( x e. S -> x C_ A )
55 dfss4 
 |-  ( x C_ A <-> ( A \ ( A \ x ) ) = x )
56 54 55 sylib 
 |-  ( x e. S -> ( A \ ( A \ x ) ) = x )
57 56 ad2antlr 
 |-  ( ( ( ph /\ x e. S ) /\ x ~<_ _om ) -> ( A \ ( A \ x ) ) = x )
58 simpr 
 |-  ( ( ( ph /\ x e. S ) /\ x ~<_ _om ) -> x ~<_ _om )
59 57 58 eqbrtrd 
 |-  ( ( ( ph /\ x e. S ) /\ x ~<_ _om ) -> ( A \ ( A \ x ) ) ~<_ _om )
60 olc 
 |-  ( ( A \ ( A \ x ) ) ~<_ _om -> ( ( A \ x ) ~<_ _om \/ ( A \ ( A \ x ) ) ~<_ _om ) )
61 59 60 syl 
 |-  ( ( ( ph /\ x e. S ) /\ x ~<_ _om ) -> ( ( A \ x ) ~<_ _om \/ ( A \ ( A \ x ) ) ~<_ _om ) )
62 51 61 jca 
 |-  ( ( ( ph /\ x e. S ) /\ x ~<_ _om ) -> ( ( A \ x ) e. ~P A /\ ( ( A \ x ) ~<_ _om \/ ( A \ ( A \ x ) ) ~<_ _om ) ) )
63 breq1 
 |-  ( y = ( A \ x ) -> ( y ~<_ _om <-> ( A \ x ) ~<_ _om ) )
64 difeq2 
 |-  ( y = ( A \ x ) -> ( A \ y ) = ( A \ ( A \ x ) ) )
65 64 breq1d 
 |-  ( y = ( A \ x ) -> ( ( A \ y ) ~<_ _om <-> ( A \ ( A \ x ) ) ~<_ _om ) )
66 63 65 orbi12d 
 |-  ( y = ( A \ x ) -> ( ( y ~<_ _om \/ ( A \ y ) ~<_ _om ) <-> ( ( A \ x ) ~<_ _om \/ ( A \ ( A \ x ) ) ~<_ _om ) ) )
67 breq1 
 |-  ( x = y -> ( x ~<_ _om <-> y ~<_ _om ) )
68 difeq2 
 |-  ( x = y -> ( A \ x ) = ( A \ y ) )
69 68 breq1d 
 |-  ( x = y -> ( ( A \ x ) ~<_ _om <-> ( A \ y ) ~<_ _om ) )
70 67 69 orbi12d 
 |-  ( x = y -> ( ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) <-> ( y ~<_ _om \/ ( A \ y ) ~<_ _om ) ) )
71 70 cbvrabv 
 |-  { x e. ~P A | ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) } = { y e. ~P A | ( y ~<_ _om \/ ( A \ y ) ~<_ _om ) }
72 2 71 eqtri 
 |-  S = { y e. ~P A | ( y ~<_ _om \/ ( A \ y ) ~<_ _om ) }
73 66 72 elrab2 
 |-  ( ( A \ x ) e. S <-> ( ( A \ x ) e. ~P A /\ ( ( A \ x ) ~<_ _om \/ ( A \ ( A \ x ) ) ~<_ _om ) ) )
74 62 73 sylibr 
 |-  ( ( ( ph /\ x e. S ) /\ x ~<_ _om ) -> ( A \ x ) e. S )
75 50 ad2antrr 
 |-  ( ( ( ph /\ x e. S ) /\ -. x ~<_ _om ) -> ( A \ x ) e. ~P A )
76 2 rabeq2i 
 |-  ( x e. S <-> ( x e. ~P A /\ ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) ) )
77 76 biimpi 
 |-  ( x e. S -> ( x e. ~P A /\ ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) ) )
78 77 simprd 
 |-  ( x e. S -> ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) )
79 78 adantl 
 |-  ( ( ph /\ x e. S ) -> ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) )
80 79 adantr 
 |-  ( ( ( ph /\ x e. S ) /\ -. x ~<_ _om ) -> ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) )
81 simpr 
 |-  ( ( ( ph /\ x e. S ) /\ -. x ~<_ _om ) -> -. x ~<_ _om )
82 pm2.53 
 |-  ( ( x ~<_ _om \/ ( A \ x ) ~<_ _om ) -> ( -. x ~<_ _om -> ( A \ x ) ~<_ _om ) )
83 80 81 82 sylc 
 |-  ( ( ( ph /\ x e. S ) /\ -. x ~<_ _om ) -> ( A \ x ) ~<_ _om )
84 orc 
 |-  ( ( A \ x ) ~<_ _om -> ( ( A \ x ) ~<_ _om \/ ( A \ ( A \ x ) ) ~<_ _om ) )
85 83 84 syl 
 |-  ( ( ( ph /\ x e. S ) /\ -. x ~<_ _om ) -> ( ( A \ x ) ~<_ _om \/ ( A \ ( A \ x ) ) ~<_ _om ) )
86 75 85 jca 
 |-  ( ( ( ph /\ x e. S ) /\ -. x ~<_ _om ) -> ( ( A \ x ) e. ~P A /\ ( ( A \ x ) ~<_ _om \/ ( A \ ( A \ x ) ) ~<_ _om ) ) )
87 86 73 sylibr 
 |-  ( ( ( ph /\ x e. S ) /\ -. x ~<_ _om ) -> ( A \ x ) e. S )
88 74 87 pm2.61dan 
 |-  ( ( ph /\ x e. S ) -> ( A \ x ) e. S )
89 elpwi 
 |-  ( x e. ~P S -> x C_ S )
90 89 adantr 
 |-  ( ( x e. ~P S /\ y e. x ) -> x C_ S )
91 simpr 
 |-  ( ( x e. ~P S /\ y e. x ) -> y e. x )
92 90 91 sseldd 
 |-  ( ( x e. ~P S /\ y e. x ) -> y e. S )
93 41 sseli 
 |-  ( y e. S -> y e. ~P A )
94 elpwi 
 |-  ( y e. ~P A -> y C_ A )
95 93 94 syl 
 |-  ( y e. S -> y C_ A )
96 92 95 syl 
 |-  ( ( x e. ~P S /\ y e. x ) -> y C_ A )
97 96 ralrimiva 
 |-  ( x e. ~P S -> A. y e. x y C_ A )
98 unissb 
 |-  ( U. x C_ A <-> A. y e. x y C_ A )
99 97 98 sylibr 
 |-  ( x e. ~P S -> U. x C_ A )
100 vuniex 
 |-  U. x e. _V
101 100 elpw 
 |-  ( U. x e. ~P A <-> U. x C_ A )
102 99 101 sylibr 
 |-  ( x e. ~P S -> U. x e. ~P A )
103 102 adantr 
 |-  ( ( x e. ~P S /\ x ~<_ _om ) -> U. x e. ~P A )
104 id 
 |-  ( ( x ~<_ _om /\ A. y e. x y ~<_ _om ) -> ( x ~<_ _om /\ A. y e. x y ~<_ _om ) )
105 104 adantll 
 |-  ( ( ( x e. ~P S /\ x ~<_ _om ) /\ A. y e. x y ~<_ _om ) -> ( x ~<_ _om /\ A. y e. x y ~<_ _om ) )
106 unictb 
 |-  ( ( x ~<_ _om /\ A. y e. x y ~<_ _om ) -> U. x ~<_ _om )
107 orc 
 |-  ( U. x ~<_ _om -> ( U. x ~<_ _om \/ ( A \ U. x ) ~<_ _om ) )
108 105 106 107 3syl 
 |-  ( ( ( x e. ~P S /\ x ~<_ _om ) /\ A. y e. x y ~<_ _om ) -> ( U. x ~<_ _om \/ ( A \ U. x ) ~<_ _om ) )
109 rexnal 
 |-  ( E. y e. x -. y ~<_ _om <-> -. A. y e. x y ~<_ _om )
110 109 bicomi 
 |-  ( -. A. y e. x y ~<_ _om <-> E. y e. x -. y ~<_ _om )
111 110 biimpi 
 |-  ( -. A. y e. x y ~<_ _om -> E. y e. x -. y ~<_ _om )
112 111 adantl 
 |-  ( ( x e. ~P S /\ -. A. y e. x y ~<_ _om ) -> E. y e. x -. y ~<_ _om )
113 nfv 
 |-  F/ y x e. ~P S
114 nfra1 
 |-  F/ y A. y e. x y ~<_ _om
115 114 nfn 
 |-  F/ y -. A. y e. x y ~<_ _om
116 113 115 nfan 
 |-  F/ y ( x e. ~P S /\ -. A. y e. x y ~<_ _om )
117 nfv 
 |-  F/ y ( A \ U. x ) ~<_ _om
118 elssuni 
 |-  ( y e. x -> y C_ U. x )
119 118 3ad2ant2 
 |-  ( ( x e. ~P S /\ y e. x /\ -. y ~<_ _om ) -> y C_ U. x )
120 119 sscond 
 |-  ( ( x e. ~P S /\ y e. x /\ -. y ~<_ _om ) -> ( A \ U. x ) C_ ( A \ y ) )
121 92 3adant3 
 |-  ( ( x e. ~P S /\ y e. x /\ -. y ~<_ _om ) -> y e. S )
122 simp3 
 |-  ( ( x e. ~P S /\ y e. x /\ -. y ~<_ _om ) -> -. y ~<_ _om )
123 72 rabeq2i 
 |-  ( y e. S <-> ( y e. ~P A /\ ( y ~<_ _om \/ ( A \ y ) ~<_ _om ) ) )
124 123 biimpi 
 |-  ( y e. S -> ( y e. ~P A /\ ( y ~<_ _om \/ ( A \ y ) ~<_ _om ) ) )
125 124 simprd 
 |-  ( y e. S -> ( y ~<_ _om \/ ( A \ y ) ~<_ _om ) )
126 125 adantr 
 |-  ( ( y e. S /\ -. y ~<_ _om ) -> ( y ~<_ _om \/ ( A \ y ) ~<_ _om ) )
127 simpr 
 |-  ( ( y e. S /\ -. y ~<_ _om ) -> -. y ~<_ _om )
128 pm2.53 
 |-  ( ( y ~<_ _om \/ ( A \ y ) ~<_ _om ) -> ( -. y ~<_ _om -> ( A \ y ) ~<_ _om ) )
129 126 127 128 sylc 
 |-  ( ( y e. S /\ -. y ~<_ _om ) -> ( A \ y ) ~<_ _om )
130 121 122 129 syl2anc 
 |-  ( ( x e. ~P S /\ y e. x /\ -. y ~<_ _om ) -> ( A \ y ) ~<_ _om )
131 ssct 
 |-  ( ( ( A \ U. x ) C_ ( A \ y ) /\ ( A \ y ) ~<_ _om ) -> ( A \ U. x ) ~<_ _om )
132 120 130 131 syl2anc 
 |-  ( ( x e. ~P S /\ y e. x /\ -. y ~<_ _om ) -> ( A \ U. x ) ~<_ _om )
133 132 3exp 
 |-  ( x e. ~P S -> ( y e. x -> ( -. y ~<_ _om -> ( A \ U. x ) ~<_ _om ) ) )
134 133 adantr 
 |-  ( ( x e. ~P S /\ -. A. y e. x y ~<_ _om ) -> ( y e. x -> ( -. y ~<_ _om -> ( A \ U. x ) ~<_ _om ) ) )
135 116 117 134 rexlimd 
 |-  ( ( x e. ~P S /\ -. A. y e. x y ~<_ _om ) -> ( E. y e. x -. y ~<_ _om -> ( A \ U. x ) ~<_ _om ) )
136 112 135 mpd 
 |-  ( ( x e. ~P S /\ -. A. y e. x y ~<_ _om ) -> ( A \ U. x ) ~<_ _om )
137 olc 
 |-  ( ( A \ U. x ) ~<_ _om -> ( U. x ~<_ _om \/ ( A \ U. x ) ~<_ _om ) )
138 136 137 syl 
 |-  ( ( x e. ~P S /\ -. A. y e. x y ~<_ _om ) -> ( U. x ~<_ _om \/ ( A \ U. x ) ~<_ _om ) )
139 138 adantlr 
 |-  ( ( ( x e. ~P S /\ x ~<_ _om ) /\ -. A. y e. x y ~<_ _om ) -> ( U. x ~<_ _om \/ ( A \ U. x ) ~<_ _om ) )
140 108 139 pm2.61dan 
 |-  ( ( x e. ~P S /\ x ~<_ _om ) -> ( U. x ~<_ _om \/ ( A \ U. x ) ~<_ _om ) )
141 103 140 jca 
 |-  ( ( x e. ~P S /\ x ~<_ _om ) -> ( U. x e. ~P A /\ ( U. x ~<_ _om \/ ( A \ U. x ) ~<_ _om ) ) )
142 breq1 
 |-  ( y = U. x -> ( y ~<_ _om <-> U. x ~<_ _om ) )
143 difeq2 
 |-  ( y = U. x -> ( A \ y ) = ( A \ U. x ) )
144 143 breq1d 
 |-  ( y = U. x -> ( ( A \ y ) ~<_ _om <-> ( A \ U. x ) ~<_ _om ) )
145 142 144 orbi12d 
 |-  ( y = U. x -> ( ( y ~<_ _om \/ ( A \ y ) ~<_ _om ) <-> ( U. x ~<_ _om \/ ( A \ U. x ) ~<_ _om ) ) )
146 145 72 elrab2 
 |-  ( U. x e. S <-> ( U. x e. ~P A /\ ( U. x ~<_ _om \/ ( A \ U. x ) ~<_ _om ) ) )
147 141 146 sylibr 
 |-  ( ( x e. ~P S /\ x ~<_ _om ) -> U. x e. S )
148 147 3adant1 
 |-  ( ( ph /\ x e. ~P S /\ x ~<_ _om ) -> U. x e. S )
149 6 20 45 88 148 issald 
 |-  ( ph -> S e. SAlg )