Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  salexct Structured version   Visualization version   GIF version

Theorem salexct 43340
 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.)
Hypotheses
Ref Expression
salexct.a (𝜑𝐴𝑉)
salexct.b 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)}
Assertion
Ref Expression
salexct (𝜑𝑆 ∈ SAlg)
Distinct variable groups:   𝑥,𝐴   𝑥,𝑆   𝜑,𝑥
Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem salexct
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 salexct.b . . 3 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)}
2 salexct.a . . . . 5 (𝜑𝐴𝑉)
32pwexd 5248 . . . 4 (𝜑 → 𝒫 𝐴 ∈ V)
4 rabexg 5201 . . . 4 (𝒫 𝐴 ∈ V → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} ∈ V)
53, 4syl 17 . . 3 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} ∈ V)
61, 5eqeltrid 2856 . 2 (𝜑𝑆 ∈ V)
7 0elpw 5224 . . . . 5 ∅ ∈ 𝒫 𝐴
87a1i 11 . . . 4 (𝜑 → ∅ ∈ 𝒫 𝐴)
9 0fin 8740 . . . . . . 7 ∅ ∈ Fin
10 fict 9149 . . . . . . 7 (∅ ∈ Fin → ∅ ≼ ω)
119, 10ax-mp 5 . . . . . 6 ∅ ≼ ω
1211orci 862 . . . . 5 (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)
1312a1i 11 . . . 4 (𝜑 → (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω))
148, 13jca 515 . . 3 (𝜑 → (∅ ∈ 𝒫 𝐴 ∧ (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)))
15 breq1 5035 . . . . 5 (𝑥 = ∅ → (𝑥 ≼ ω ↔ ∅ ≼ ω))
16 difeq2 4022 . . . . . 6 (𝑥 = ∅ → (𝐴𝑥) = (𝐴 ∖ ∅))
1716breq1d 5042 . . . . 5 (𝑥 = ∅ → ((𝐴𝑥) ≼ ω ↔ (𝐴 ∖ ∅) ≼ ω))
1815, 17orbi12d 916 . . . 4 (𝑥 = ∅ → ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) ↔ (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)))
1918, 1elrab2 3605 . . 3 (∅ ∈ 𝑆 ↔ (∅ ∈ 𝒫 𝐴 ∧ (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)))
2014, 19sylibr 237 . 2 (𝜑 → ∅ ∈ 𝑆)
21 snidg 4556 . . . . . 6 (𝑦𝐴𝑦 ∈ {𝑦})
22 snelpwi 5305 . . . . . . . 8 (𝑦𝐴 → {𝑦} ∈ 𝒫 𝐴)
23 snfi 8614 . . . . . . . . . . 11 {𝑦} ∈ Fin
24 fict 9149 . . . . . . . . . . 11 ({𝑦} ∈ Fin → {𝑦} ≼ ω)
2523, 24ax-mp 5 . . . . . . . . . 10 {𝑦} ≼ ω
2625orci 862 . . . . . . . . 9 ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)
2726a1i 11 . . . . . . . 8 (𝑦𝐴 → ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))
2822, 27jca 515 . . . . . . 7 (𝑦𝐴 → ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
29 breq1 5035 . . . . . . . . 9 (𝑥 = {𝑦} → (𝑥 ≼ ω ↔ {𝑦} ≼ ω))
30 difeq2 4022 . . . . . . . . . 10 (𝑥 = {𝑦} → (𝐴𝑥) = (𝐴 ∖ {𝑦}))
3130breq1d 5042 . . . . . . . . 9 (𝑥 = {𝑦} → ((𝐴𝑥) ≼ ω ↔ (𝐴 ∖ {𝑦}) ≼ ω))
3229, 31orbi12d 916 . . . . . . . 8 (𝑥 = {𝑦} → ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) ↔ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
3332, 1elrab2 3605 . . . . . . 7 ({𝑦} ∈ 𝑆 ↔ ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
3428, 33sylibr 237 . . . . . 6 (𝑦𝐴 → {𝑦} ∈ 𝑆)
35 elunii 4803 . . . . . 6 ((𝑦 ∈ {𝑦} ∧ {𝑦} ∈ 𝑆) → 𝑦 𝑆)
3621, 34, 35syl2anc 587 . . . . 5 (𝑦𝐴𝑦 𝑆)
3736rgen 3080 . . . 4 𝑦𝐴 𝑦 𝑆
38 dfss3 3880 . . . 4 (𝐴 𝑆 ↔ ∀𝑦𝐴 𝑦 𝑆)
3937, 38mpbir 234 . . 3 𝐴 𝑆
40 ssrab2 3984 . . . . . 6 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} ⊆ 𝒫 𝐴
411, 40eqsstri 3926 . . . . 5 𝑆 ⊆ 𝒫 𝐴
4241unissi 4807 . . . 4 𝑆 𝒫 𝐴
43 unipw 5311 . . . 4 𝒫 𝐴 = 𝐴
4442, 43sseqtri 3928 . . 3 𝑆𝐴
4539, 44eqssi 3908 . 2 𝐴 = 𝑆
46 difssd 4038 . . . . . . 7 (𝜑 → (𝐴𝑥) ⊆ 𝐴)
472, 46ssexd 5194 . . . . . . . 8 (𝜑 → (𝐴𝑥) ∈ V)
48 elpwg 4497 . . . . . . . 8 ((𝐴𝑥) ∈ V → ((𝐴𝑥) ∈ 𝒫 𝐴 ↔ (𝐴𝑥) ⊆ 𝐴))
4947, 48syl 17 . . . . . . 7 (𝜑 → ((𝐴𝑥) ∈ 𝒫 𝐴 ↔ (𝐴𝑥) ⊆ 𝐴))
5046, 49mpbird 260 . . . . . 6 (𝜑 → (𝐴𝑥) ∈ 𝒫 𝐴)
5150ad2antrr 725 . . . . 5 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝒫 𝐴)
5241sseli 3888 . . . . . . . . . 10 (𝑥𝑆𝑥 ∈ 𝒫 𝐴)
53 elpwi 4503 . . . . . . . . . 10 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
5452, 53syl 17 . . . . . . . . 9 (𝑥𝑆𝑥𝐴)
55 dfss4 4163 . . . . . . . . 9 (𝑥𝐴 ↔ (𝐴 ∖ (𝐴𝑥)) = 𝑥)
5654, 55sylib 221 . . . . . . . 8 (𝑥𝑆 → (𝐴 ∖ (𝐴𝑥)) = 𝑥)
5756ad2antlr 726 . . . . . . 7 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ (𝐴𝑥)) = 𝑥)
58 simpr 488 . . . . . . 7 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → 𝑥 ≼ ω)
5957, 58eqbrtrd 5054 . . . . . 6 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ (𝐴𝑥)) ≼ ω)
60 olc 865 . . . . . 6 ((𝐴 ∖ (𝐴𝑥)) ≼ ω → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
6159, 60syl 17 . . . . 5 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
6251, 61jca 515 . . . 4 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → ((𝐴𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
63 breq1 5035 . . . . . 6 (𝑦 = (𝐴𝑥) → (𝑦 ≼ ω ↔ (𝐴𝑥) ≼ ω))
64 difeq2 4022 . . . . . . 7 (𝑦 = (𝐴𝑥) → (𝐴𝑦) = (𝐴 ∖ (𝐴𝑥)))
6564breq1d 5042 . . . . . 6 (𝑦 = (𝐴𝑥) → ((𝐴𝑦) ≼ ω ↔ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
6663, 65orbi12d 916 . . . . 5 (𝑦 = (𝐴𝑥) → ((𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω) ↔ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
67 breq1 5035 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 ≼ ω ↔ 𝑦 ≼ ω))
68 difeq2 4022 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐴𝑥) = (𝐴𝑦))
6968breq1d 5042 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐴𝑥) ≼ ω ↔ (𝐴𝑦) ≼ ω))
7067, 69orbi12d 916 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) ↔ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)))
7170cbvrabv 3404 . . . . . 6 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} = {𝑦 ∈ 𝒫 𝐴 ∣ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)}
721, 71eqtri 2781 . . . . 5 𝑆 = {𝑦 ∈ 𝒫 𝐴 ∣ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)}
7366, 72elrab2 3605 . . . 4 ((𝐴𝑥) ∈ 𝑆 ↔ ((𝐴𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
7462, 73sylibr 237 . . 3 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝑆)
7550ad2antrr 725 . . . . 5 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝒫 𝐴)
761rabeq2i 3400 . . . . . . . . . . 11 (𝑥𝑆 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)))
7776biimpi 219 . . . . . . . . . 10 (𝑥𝑆 → (𝑥 ∈ 𝒫 𝐴 ∧ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)))
7877simprd 499 . . . . . . . . 9 (𝑥𝑆 → (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω))
7978adantl 485 . . . . . . . 8 ((𝜑𝑥𝑆) → (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω))
8079adantr 484 . . . . . . 7 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω))
81 simpr 488 . . . . . . 7 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → ¬ 𝑥 ≼ ω)
82 pm2.53 848 . . . . . . 7 ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) → (¬ 𝑥 ≼ ω → (𝐴𝑥) ≼ ω))
8380, 81, 82sylc 65 . . . . . 6 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴𝑥) ≼ ω)
84 orc 864 . . . . . 6 ((𝐴𝑥) ≼ ω → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
8583, 84syl 17 . . . . 5 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
8675, 85jca 515 . . . 4 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → ((𝐴𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
8786, 73sylibr 237 . . 3 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝑆)
8874, 87pm2.61dan 812 . 2 ((𝜑𝑥𝑆) → (𝐴𝑥) ∈ 𝑆)
89 elpwi 4503 . . . . . . . . . . . 12 (𝑥 ∈ 𝒫 𝑆𝑥𝑆)
9089adantr 484 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑥𝑆)
91 simpr 488 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑦𝑥)
9290, 91sseldd 3893 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑦𝑆)
9341sseli 3888 . . . . . . . . . . 11 (𝑦𝑆𝑦 ∈ 𝒫 𝐴)
94 elpwi 4503 . . . . . . . . . . 11 (𝑦 ∈ 𝒫 𝐴𝑦𝐴)
9593, 94syl 17 . . . . . . . . . 10 (𝑦𝑆𝑦𝐴)
9692, 95syl 17 . . . . . . . . 9 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑦𝐴)
9796ralrimiva 3113 . . . . . . . 8 (𝑥 ∈ 𝒫 𝑆 → ∀𝑦𝑥 𝑦𝐴)
98 unissb 4832 . . . . . . . 8 ( 𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
9997, 98sylibr 237 . . . . . . 7 (𝑥 ∈ 𝒫 𝑆 𝑥𝐴)
100 vuniex 7463 . . . . . . . 8 𝑥 ∈ V
101100elpw 4498 . . . . . . 7 ( 𝑥 ∈ 𝒫 𝐴 𝑥𝐴)
10299, 101sylibr 237 . . . . . 6 (𝑥 ∈ 𝒫 𝑆 𝑥 ∈ 𝒫 𝐴)
103102adantr 484 . . . . 5 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → 𝑥 ∈ 𝒫 𝐴)
104 id 22 . . . . . . . 8 ((𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω) → (𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω))
105104adantll 713 . . . . . . 7 (((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) ∧ ∀𝑦𝑥 𝑦 ≼ ω) → (𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω))
106 unictb 10035 . . . . . . 7 ((𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω) → 𝑥 ≼ ω)
107 orc 864 . . . . . . 7 ( 𝑥 ≼ ω → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
108105, 106, 1073syl 18 . . . . . 6 (((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) ∧ ∀𝑦𝑥 𝑦 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
109 rexnal 3165 . . . . . . . . . . . 12 (∃𝑦𝑥 ¬ 𝑦 ≼ ω ↔ ¬ ∀𝑦𝑥 𝑦 ≼ ω)
110109bicomi 227 . . . . . . . . . . 11 (¬ ∀𝑦𝑥 𝑦 ≼ ω ↔ ∃𝑦𝑥 ¬ 𝑦 ≼ ω)
111110biimpi 219 . . . . . . . . . 10 (¬ ∀𝑦𝑥 𝑦 ≼ ω → ∃𝑦𝑥 ¬ 𝑦 ≼ ω)
112111adantl 485 . . . . . . . . 9 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → ∃𝑦𝑥 ¬ 𝑦 ≼ ω)
113 nfv 1915 . . . . . . . . . . 11 𝑦 𝑥 ∈ 𝒫 𝑆
114 nfra1 3147 . . . . . . . . . . . 12 𝑦𝑦𝑥 𝑦 ≼ ω
115114nfn 1858 . . . . . . . . . . 11 𝑦 ¬ ∀𝑦𝑥 𝑦 ≼ ω
116113, 115nfan 1900 . . . . . . . . . 10 𝑦(𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω)
117 nfv 1915 . . . . . . . . . 10 𝑦(𝐴 𝑥) ≼ ω
118 elssuni 4830 . . . . . . . . . . . . . . 15 (𝑦𝑥𝑦 𝑥)
1191183ad2ant2 1131 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → 𝑦 𝑥)
120119sscond 4047 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴 𝑥) ⊆ (𝐴𝑦))
121923adant3 1129 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → 𝑦𝑆)
122 simp3 1135 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → ¬ 𝑦 ≼ ω)
12372rabeq2i 3400 . . . . . . . . . . . . . . . . . 18 (𝑦𝑆 ↔ (𝑦 ∈ 𝒫 𝐴 ∧ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)))
124123biimpi 219 . . . . . . . . . . . . . . . . 17 (𝑦𝑆 → (𝑦 ∈ 𝒫 𝐴 ∧ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)))
125124simprd 499 . . . . . . . . . . . . . . . 16 (𝑦𝑆 → (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω))
126125adantr 484 . . . . . . . . . . . . . . 15 ((𝑦𝑆 ∧ ¬ 𝑦 ≼ ω) → (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω))
127 simpr 488 . . . . . . . . . . . . . . 15 ((𝑦𝑆 ∧ ¬ 𝑦 ≼ ω) → ¬ 𝑦 ≼ ω)
128 pm2.53 848 . . . . . . . . . . . . . . 15 ((𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω) → (¬ 𝑦 ≼ ω → (𝐴𝑦) ≼ ω))
129126, 127, 128sylc 65 . . . . . . . . . . . . . 14 ((𝑦𝑆 ∧ ¬ 𝑦 ≼ ω) → (𝐴𝑦) ≼ ω)
130121, 122, 129syl2anc 587 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴𝑦) ≼ ω)
131 ssct 8619 . . . . . . . . . . . . 13 (((𝐴 𝑥) ⊆ (𝐴𝑦) ∧ (𝐴𝑦) ≼ ω) → (𝐴 𝑥) ≼ ω)
132120, 130, 131syl2anc 587 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴 𝑥) ≼ ω)
1331323exp 1116 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝑆 → (𝑦𝑥 → (¬ 𝑦 ≼ ω → (𝐴 𝑥) ≼ ω)))
134133adantr 484 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → (𝑦𝑥 → (¬ 𝑦 ≼ ω → (𝐴 𝑥) ≼ ω)))
135116, 117, 134rexlimd 3241 . . . . . . . . 9 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → (∃𝑦𝑥 ¬ 𝑦 ≼ ω → (𝐴 𝑥) ≼ ω))
136112, 135mpd 15 . . . . . . . 8 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → (𝐴 𝑥) ≼ ω)
137 olc 865 . . . . . . . 8 ((𝐴 𝑥) ≼ ω → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
138136, 137syl 17 . . . . . . 7 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
139138adantlr 714 . . . . . 6 (((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
140108, 139pm2.61dan 812 . . . . 5 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
141103, 140jca 515 . . . 4 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω)))
142 breq1 5035 . . . . . 6 (𝑦 = 𝑥 → (𝑦 ≼ ω ↔ 𝑥 ≼ ω))
143 difeq2 4022 . . . . . . 7 (𝑦 = 𝑥 → (𝐴𝑦) = (𝐴 𝑥))
144143breq1d 5042 . . . . . 6 (𝑦 = 𝑥 → ((𝐴𝑦) ≼ ω ↔ (𝐴 𝑥) ≼ ω))
145142, 144orbi12d 916 . . . . 5 (𝑦 = 𝑥 → ((𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω) ↔ ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω)))
146145, 72elrab2 3605 . . . 4 ( 𝑥𝑆 ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω)))
147141, 146sylibr 237 . . 3 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → 𝑥𝑆)
1481473adant1 1127 . 2 ((𝜑𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → 𝑥𝑆)
1496, 20, 45, 88, 148issald 43339 1 (𝜑𝑆 ∈ SAlg)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071  {crab 3074  Vcvv 3409   ∖ cdif 3855   ⊆ wss 3858  ∅c0 4225  𝒫 cpw 4494  {csn 4522  ∪ cuni 4798   class class class wbr 5032  ωcom 7579   ≼ cdom 8525  Fincfn 8527  SAlgcsalg 43316 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-inf2 9137  ax-cc 9895 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-int 4839  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-se 5484  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-isom 6344  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7580  df-1st 7693  df-2nd 7694  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-er 8299  df-map 8418  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-oi 9007  df-card 9401  df-acn 9404  df-salg 43317 This theorem is referenced by:  salexct3  43348  salgencntex  43349  salgensscntex  43350
 Copyright terms: Public domain W3C validator