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

Theorem salexct 40870
Description: An example of non trivial 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 (𝜑𝐴𝑉)
3 pwexg 4880 . . . . 5 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
42, 3syl 17 . . . 4 (𝜑 → 𝒫 𝐴 ∈ V)
5 rabexg 4844 . . . 4 (𝒫 𝐴 ∈ V → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} ∈ V)
64, 5syl 17 . . 3 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} ∈ V)
71, 6syl5eqel 2734 . 2 (𝜑𝑆 ∈ V)
8 0elpw 4864 . . . . 5 ∅ ∈ 𝒫 𝐴
98a1i 11 . . . 4 (𝜑 → ∅ ∈ 𝒫 𝐴)
10 0fin 8229 . . . . . . 7 ∅ ∈ Fin
11 fict 8588 . . . . . . 7 (∅ ∈ Fin → ∅ ≼ ω)
1210, 11ax-mp 5 . . . . . 6 ∅ ≼ ω
1312orci 404 . . . . 5 (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)
1413a1i 11 . . . 4 (𝜑 → (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω))
159, 14jca 553 . . 3 (𝜑 → (∅ ∈ 𝒫 𝐴 ∧ (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)))
16 breq1 4688 . . . . 5 (𝑥 = ∅ → (𝑥 ≼ ω ↔ ∅ ≼ ω))
17 difeq2 3755 . . . . . 6 (𝑥 = ∅ → (𝐴𝑥) = (𝐴 ∖ ∅))
1817breq1d 4695 . . . . 5 (𝑥 = ∅ → ((𝐴𝑥) ≼ ω ↔ (𝐴 ∖ ∅) ≼ ω))
1916, 18orbi12d 746 . . . 4 (𝑥 = ∅ → ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) ↔ (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)))
2019, 1elrab2 3399 . . 3 (∅ ∈ 𝑆 ↔ (∅ ∈ 𝒫 𝐴 ∧ (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)))
2115, 20sylibr 224 . 2 (𝜑 → ∅ ∈ 𝑆)
22 snidg 4239 . . . . . 6 (𝑦𝐴𝑦 ∈ {𝑦})
23 snelpwi 4942 . . . . . . . 8 (𝑦𝐴 → {𝑦} ∈ 𝒫 𝐴)
24 snfi 8079 . . . . . . . . . . 11 {𝑦} ∈ Fin
25 fict 8588 . . . . . . . . . . 11 ({𝑦} ∈ Fin → {𝑦} ≼ ω)
2624, 25ax-mp 5 . . . . . . . . . 10 {𝑦} ≼ ω
2726orci 404 . . . . . . . . 9 ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)
2827a1i 11 . . . . . . . 8 (𝑦𝐴 → ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))
2923, 28jca 553 . . . . . . 7 (𝑦𝐴 → ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
30 breq1 4688 . . . . . . . . 9 (𝑥 = {𝑦} → (𝑥 ≼ ω ↔ {𝑦} ≼ ω))
31 difeq2 3755 . . . . . . . . . 10 (𝑥 = {𝑦} → (𝐴𝑥) = (𝐴 ∖ {𝑦}))
3231breq1d 4695 . . . . . . . . 9 (𝑥 = {𝑦} → ((𝐴𝑥) ≼ ω ↔ (𝐴 ∖ {𝑦}) ≼ ω))
3330, 32orbi12d 746 . . . . . . . 8 (𝑥 = {𝑦} → ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) ↔ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
3433, 1elrab2 3399 . . . . . . 7 ({𝑦} ∈ 𝑆 ↔ ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
3529, 34sylibr 224 . . . . . 6 (𝑦𝐴 → {𝑦} ∈ 𝑆)
36 elunii 4473 . . . . . 6 ((𝑦 ∈ {𝑦} ∧ {𝑦} ∈ 𝑆) → 𝑦 𝑆)
3722, 35, 36syl2anc 694 . . . . 5 (𝑦𝐴𝑦 𝑆)
3837rgen 2951 . . . 4 𝑦𝐴 𝑦 𝑆
39 dfss3 3625 . . . 4 (𝐴 𝑆 ↔ ∀𝑦𝐴 𝑦 𝑆)
4038, 39mpbir 221 . . 3 𝐴 𝑆
41 ssrab2 3720 . . . . . 6 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} ⊆ 𝒫 𝐴
421, 41eqsstri 3668 . . . . 5 𝑆 ⊆ 𝒫 𝐴
4342unissi 4493 . . . 4 𝑆 𝒫 𝐴
44 unipw 4948 . . . 4 𝒫 𝐴 = 𝐴
4543, 44sseqtri 3670 . . 3 𝑆𝐴
4640, 45eqssi 3652 . 2 𝐴 = 𝑆
47 difssd 3771 . . . . . . 7 (𝜑 → (𝐴𝑥) ⊆ 𝐴)
482, 47ssexd 4838 . . . . . . . 8 (𝜑 → (𝐴𝑥) ∈ V)
49 elpwg 4199 . . . . . . . 8 ((𝐴𝑥) ∈ V → ((𝐴𝑥) ∈ 𝒫 𝐴 ↔ (𝐴𝑥) ⊆ 𝐴))
5048, 49syl 17 . . . . . . 7 (𝜑 → ((𝐴𝑥) ∈ 𝒫 𝐴 ↔ (𝐴𝑥) ⊆ 𝐴))
5147, 50mpbird 247 . . . . . 6 (𝜑 → (𝐴𝑥) ∈ 𝒫 𝐴)
5251ad2antrr 762 . . . . 5 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝒫 𝐴)
5342sseli 3632 . . . . . . . . . 10 (𝑥𝑆𝑥 ∈ 𝒫 𝐴)
54 elpwi 4201 . . . . . . . . . 10 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
5553, 54syl 17 . . . . . . . . 9 (𝑥𝑆𝑥𝐴)
56 dfss4 3891 . . . . . . . . 9 (𝑥𝐴 ↔ (𝐴 ∖ (𝐴𝑥)) = 𝑥)
5755, 56sylib 208 . . . . . . . 8 (𝑥𝑆 → (𝐴 ∖ (𝐴𝑥)) = 𝑥)
5857ad2antlr 763 . . . . . . 7 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ (𝐴𝑥)) = 𝑥)
59 simpr 476 . . . . . . 7 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → 𝑥 ≼ ω)
6058, 59eqbrtrd 4707 . . . . . 6 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ (𝐴𝑥)) ≼ ω)
61 olc 398 . . . . . 6 ((𝐴 ∖ (𝐴𝑥)) ≼ ω → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
6260, 61syl 17 . . . . 5 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
6352, 62jca 553 . . . 4 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → ((𝐴𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
64 breq1 4688 . . . . . 6 (𝑦 = (𝐴𝑥) → (𝑦 ≼ ω ↔ (𝐴𝑥) ≼ ω))
65 difeq2 3755 . . . . . . 7 (𝑦 = (𝐴𝑥) → (𝐴𝑦) = (𝐴 ∖ (𝐴𝑥)))
6665breq1d 4695 . . . . . 6 (𝑦 = (𝐴𝑥) → ((𝐴𝑦) ≼ ω ↔ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
6764, 66orbi12d 746 . . . . 5 (𝑦 = (𝐴𝑥) → ((𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω) ↔ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
68 breq1 4688 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 ≼ ω ↔ 𝑦 ≼ ω))
69 difeq2 3755 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐴𝑥) = (𝐴𝑦))
7069breq1d 4695 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐴𝑥) ≼ ω ↔ (𝐴𝑦) ≼ ω))
7168, 70orbi12d 746 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) ↔ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)))
7271cbvrabv 3230 . . . . . 6 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} = {𝑦 ∈ 𝒫 𝐴 ∣ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)}
731, 72eqtri 2673 . . . . 5 𝑆 = {𝑦 ∈ 𝒫 𝐴 ∣ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)}
7467, 73elrab2 3399 . . . 4 ((𝐴𝑥) ∈ 𝑆 ↔ ((𝐴𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
7563, 74sylibr 224 . . 3 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝑆)
7651ad2antrr 762 . . . . 5 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝒫 𝐴)
771rabeq2i 3228 . . . . . . . . . . 11 (𝑥𝑆 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)))
7877biimpi 206 . . . . . . . . . 10 (𝑥𝑆 → (𝑥 ∈ 𝒫 𝐴 ∧ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)))
7978simprd 478 . . . . . . . . 9 (𝑥𝑆 → (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω))
8079adantl 481 . . . . . . . 8 ((𝜑𝑥𝑆) → (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω))
8180adantr 480 . . . . . . 7 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω))
82 simpr 476 . . . . . . 7 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → ¬ 𝑥 ≼ ω)
83 pm2.53 387 . . . . . . 7 ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) → (¬ 𝑥 ≼ ω → (𝐴𝑥) ≼ ω))
8481, 82, 83sylc 65 . . . . . 6 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴𝑥) ≼ ω)
85 orc 399 . . . . . 6 ((𝐴𝑥) ≼ ω → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
8684, 85syl 17 . . . . 5 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
8776, 86jca 553 . . . 4 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → ((𝐴𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
8887, 74sylibr 224 . . 3 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝑆)
8975, 88pm2.61dan 849 . 2 ((𝜑𝑥𝑆) → (𝐴𝑥) ∈ 𝑆)
90 elpwi 4201 . . . . . . . . . . . 12 (𝑥 ∈ 𝒫 𝑆𝑥𝑆)
9190adantr 480 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑥𝑆)
92 simpr 476 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑦𝑥)
9391, 92sseldd 3637 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑦𝑆)
9442sseli 3632 . . . . . . . . . . 11 (𝑦𝑆𝑦 ∈ 𝒫 𝐴)
95 elpwi 4201 . . . . . . . . . . 11 (𝑦 ∈ 𝒫 𝐴𝑦𝐴)
9694, 95syl 17 . . . . . . . . . 10 (𝑦𝑆𝑦𝐴)
9793, 96syl 17 . . . . . . . . 9 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑦𝐴)
9897ralrimiva 2995 . . . . . . . 8 (𝑥 ∈ 𝒫 𝑆 → ∀𝑦𝑥 𝑦𝐴)
99 unissb 4501 . . . . . . . 8 ( 𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
10098, 99sylibr 224 . . . . . . 7 (𝑥 ∈ 𝒫 𝑆 𝑥𝐴)
101 vuniex 6996 . . . . . . . 8 𝑥 ∈ V
102101elpw 4197 . . . . . . 7 ( 𝑥 ∈ 𝒫 𝐴 𝑥𝐴)
103100, 102sylibr 224 . . . . . 6 (𝑥 ∈ 𝒫 𝑆 𝑥 ∈ 𝒫 𝐴)
104103adantr 480 . . . . 5 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → 𝑥 ∈ 𝒫 𝐴)
105 id 22 . . . . . . . 8 ((𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω) → (𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω))
106105adantll 750 . . . . . . 7 (((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) ∧ ∀𝑦𝑥 𝑦 ≼ ω) → (𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω))
107 unictb 9435 . . . . . . 7 ((𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω) → 𝑥 ≼ ω)
108 orc 399 . . . . . . 7 ( 𝑥 ≼ ω → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
109106, 107, 1083syl 18 . . . . . 6 (((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) ∧ ∀𝑦𝑥 𝑦 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
110 rexnal 3024 . . . . . . . . . . . 12 (∃𝑦𝑥 ¬ 𝑦 ≼ ω ↔ ¬ ∀𝑦𝑥 𝑦 ≼ ω)
111110bicomi 214 . . . . . . . . . . 11 (¬ ∀𝑦𝑥 𝑦 ≼ ω ↔ ∃𝑦𝑥 ¬ 𝑦 ≼ ω)
112111biimpi 206 . . . . . . . . . 10 (¬ ∀𝑦𝑥 𝑦 ≼ ω → ∃𝑦𝑥 ¬ 𝑦 ≼ ω)
113112adantl 481 . . . . . . . . 9 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → ∃𝑦𝑥 ¬ 𝑦 ≼ ω)
114 nfv 1883 . . . . . . . . . . 11 𝑦 𝑥 ∈ 𝒫 𝑆
115 nfra1 2970 . . . . . . . . . . . 12 𝑦𝑦𝑥 𝑦 ≼ ω
116115nfn 1824 . . . . . . . . . . 11 𝑦 ¬ ∀𝑦𝑥 𝑦 ≼ ω
117114, 116nfan 1868 . . . . . . . . . 10 𝑦(𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω)
118 nfv 1883 . . . . . . . . . 10 𝑦(𝐴 𝑥) ≼ ω
119 elssuni 4499 . . . . . . . . . . . . . . 15 (𝑦𝑥𝑦 𝑥)
1201193ad2ant2 1103 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → 𝑦 𝑥)
121120sscond 3780 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴 𝑥) ⊆ (𝐴𝑦))
122933adant3 1101 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → 𝑦𝑆)
123 simp3 1083 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → ¬ 𝑦 ≼ ω)
12473rabeq2i 3228 . . . . . . . . . . . . . . . . . 18 (𝑦𝑆 ↔ (𝑦 ∈ 𝒫 𝐴 ∧ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)))
125124biimpi 206 . . . . . . . . . . . . . . . . 17 (𝑦𝑆 → (𝑦 ∈ 𝒫 𝐴 ∧ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)))
126125simprd 478 . . . . . . . . . . . . . . . 16 (𝑦𝑆 → (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω))
127126adantr 480 . . . . . . . . . . . . . . 15 ((𝑦𝑆 ∧ ¬ 𝑦 ≼ ω) → (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω))
128 simpr 476 . . . . . . . . . . . . . . 15 ((𝑦𝑆 ∧ ¬ 𝑦 ≼ ω) → ¬ 𝑦 ≼ ω)
129 pm2.53 387 . . . . . . . . . . . . . . 15 ((𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω) → (¬ 𝑦 ≼ ω → (𝐴𝑦) ≼ ω))
130127, 128, 129sylc 65 . . . . . . . . . . . . . 14 ((𝑦𝑆 ∧ ¬ 𝑦 ≼ ω) → (𝐴𝑦) ≼ ω)
131122, 123, 130syl2anc 694 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴𝑦) ≼ ω)
132 ssct 8082 . . . . . . . . . . . . 13 (((𝐴 𝑥) ⊆ (𝐴𝑦) ∧ (𝐴𝑦) ≼ ω) → (𝐴 𝑥) ≼ ω)
133121, 131, 132syl2anc 694 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴 𝑥) ≼ ω)
1341333exp 1283 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝑆 → (𝑦𝑥 → (¬ 𝑦 ≼ ω → (𝐴 𝑥) ≼ ω)))
135134adantr 480 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → (𝑦𝑥 → (¬ 𝑦 ≼ ω → (𝐴 𝑥) ≼ ω)))
136117, 118, 135rexlimd 3055 . . . . . . . . 9 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → (∃𝑦𝑥 ¬ 𝑦 ≼ ω → (𝐴 𝑥) ≼ ω))
137113, 136mpd 15 . . . . . . . 8 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → (𝐴 𝑥) ≼ ω)
138 olc 398 . . . . . . . 8 ((𝐴 𝑥) ≼ ω → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
139137, 138syl 17 . . . . . . 7 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
140139adantlr 751 . . . . . 6 (((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
141109, 140pm2.61dan 849 . . . . 5 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
142104, 141jca 553 . . . 4 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω)))
143 breq1 4688 . . . . . 6 (𝑦 = 𝑥 → (𝑦 ≼ ω ↔ 𝑥 ≼ ω))
144 difeq2 3755 . . . . . . 7 (𝑦 = 𝑥 → (𝐴𝑦) = (𝐴 𝑥))
145144breq1d 4695 . . . . . 6 (𝑦 = 𝑥 → ((𝐴𝑦) ≼ ω ↔ (𝐴 𝑥) ≼ ω))
146143, 145orbi12d 746 . . . . 5 (𝑦 = 𝑥 → ((𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω) ↔ ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω)))
147146, 73elrab2 3399 . . . 4 ( 𝑥𝑆 ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω)))
148142, 147sylibr 224 . . 3 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → 𝑥𝑆)
1491483adant1 1099 . 2 ((𝜑𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → 𝑥𝑆)
1507, 21, 46, 89, 149issald 40869 1 (𝜑𝑆 ∈ SAlg)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054   = wceq 1523  wcel 2030  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  cdif 3604  wss 3607  c0 3948  𝒫 cpw 4191  {csn 4210   cuni 4468   class class class wbr 4685  ωcom 7107  cdom 7995  Fincfn 7997  SAlgcsalg 40846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cc 9295
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-oi 8456  df-card 8803  df-acn 8806  df-salg 40847
This theorem is referenced by:  salexct3  40878  salgencntex  40879  salgensscntex  40880
  Copyright terms: Public domain W3C validator