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 φ A V
salexct.b S = x 𝒫 A | x ω A x ω
Assertion salexct φ S SAlg

Proof

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