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 41031
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 5049 . . . 4 (𝜑 → 𝒫 𝐴 ∈ V)
4 rabexg 5006 . . . 4 (𝒫 𝐴 ∈ V → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} ∈ V)
53, 4syl 17 . . 3 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} ∈ V)
61, 5syl5eqel 2889 . 2 (𝜑𝑆 ∈ V)
7 0elpw 5026 . . . . 5 ∅ ∈ 𝒫 𝐴
87a1i 11 . . . 4 (𝜑 → ∅ ∈ 𝒫 𝐴)
9 0fin 8427 . . . . . . 7 ∅ ∈ Fin
10 fict 8797 . . . . . . 7 (∅ ∈ Fin → ∅ ≼ ω)
119, 10ax-mp 5 . . . . . 6 ∅ ≼ ω
1211orci 883 . . . . 5 (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)
1312a1i 11 . . . 4 (𝜑 → (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω))
148, 13jca 503 . . 3 (𝜑 → (∅ ∈ 𝒫 𝐴 ∧ (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)))
15 breq1 4847 . . . . 5 (𝑥 = ∅ → (𝑥 ≼ ω ↔ ∅ ≼ ω))
16 difeq2 3921 . . . . . 6 (𝑥 = ∅ → (𝐴𝑥) = (𝐴 ∖ ∅))
1716breq1d 4854 . . . . 5 (𝑥 = ∅ → ((𝐴𝑥) ≼ ω ↔ (𝐴 ∖ ∅) ≼ ω))
1815, 17orbi12d 933 . . . 4 (𝑥 = ∅ → ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) ↔ (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)))
1918, 1elrab2 3562 . . 3 (∅ ∈ 𝑆 ↔ (∅ ∈ 𝒫 𝐴 ∧ (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)))
2014, 19sylibr 225 . 2 (𝜑 → ∅ ∈ 𝑆)
21 snidg 4400 . . . . . 6 (𝑦𝐴𝑦 ∈ {𝑦})
22 snelpwi 5102 . . . . . . . 8 (𝑦𝐴 → {𝑦} ∈ 𝒫 𝐴)
23 snfi 8277 . . . . . . . . . . 11 {𝑦} ∈ Fin
24 fict 8797 . . . . . . . . . . 11 ({𝑦} ∈ Fin → {𝑦} ≼ ω)
2523, 24ax-mp 5 . . . . . . . . . 10 {𝑦} ≼ ω
2625orci 883 . . . . . . . . 9 ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)
2726a1i 11 . . . . . . . 8 (𝑦𝐴 → ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))
2822, 27jca 503 . . . . . . 7 (𝑦𝐴 → ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
29 breq1 4847 . . . . . . . . 9 (𝑥 = {𝑦} → (𝑥 ≼ ω ↔ {𝑦} ≼ ω))
30 difeq2 3921 . . . . . . . . . 10 (𝑥 = {𝑦} → (𝐴𝑥) = (𝐴 ∖ {𝑦}))
3130breq1d 4854 . . . . . . . . 9 (𝑥 = {𝑦} → ((𝐴𝑥) ≼ ω ↔ (𝐴 ∖ {𝑦}) ≼ ω))
3229, 31orbi12d 933 . . . . . . . 8 (𝑥 = {𝑦} → ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) ↔ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
3332, 1elrab2 3562 . . . . . . 7 ({𝑦} ∈ 𝑆 ↔ ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
3428, 33sylibr 225 . . . . . 6 (𝑦𝐴 → {𝑦} ∈ 𝑆)
35 elunii 4635 . . . . . 6 ((𝑦 ∈ {𝑦} ∧ {𝑦} ∈ 𝑆) → 𝑦 𝑆)
3621, 34, 35syl2anc 575 . . . . 5 (𝑦𝐴𝑦 𝑆)
3736rgen 3110 . . . 4 𝑦𝐴 𝑦 𝑆
38 dfss3 3787 . . . 4 (𝐴 𝑆 ↔ ∀𝑦𝐴 𝑦 𝑆)
3937, 38mpbir 222 . . 3 𝐴 𝑆
40 ssrab2 3884 . . . . . 6 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} ⊆ 𝒫 𝐴
411, 40eqsstri 3832 . . . . 5 𝑆 ⊆ 𝒫 𝐴
4241unissi 4655 . . . 4 𝑆 𝒫 𝐴
43 unipw 5108 . . . 4 𝒫 𝐴 = 𝐴
4442, 43sseqtri 3834 . . 3 𝑆𝐴
4539, 44eqssi 3814 . 2 𝐴 = 𝑆
46 difssd 3937 . . . . . . 7 (𝜑 → (𝐴𝑥) ⊆ 𝐴)
472, 46ssexd 5000 . . . . . . . 8 (𝜑 → (𝐴𝑥) ∈ V)
48 elpwg 4359 . . . . . . . 8 ((𝐴𝑥) ∈ V → ((𝐴𝑥) ∈ 𝒫 𝐴 ↔ (𝐴𝑥) ⊆ 𝐴))
4947, 48syl 17 . . . . . . 7 (𝜑 → ((𝐴𝑥) ∈ 𝒫 𝐴 ↔ (𝐴𝑥) ⊆ 𝐴))
5046, 49mpbird 248 . . . . . 6 (𝜑 → (𝐴𝑥) ∈ 𝒫 𝐴)
5150ad2antrr 708 . . . . 5 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝒫 𝐴)
5241sseli 3794 . . . . . . . . . 10 (𝑥𝑆𝑥 ∈ 𝒫 𝐴)
53 elpwi 4361 . . . . . . . . . 10 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
5452, 53syl 17 . . . . . . . . 9 (𝑥𝑆𝑥𝐴)
55 dfss4 4060 . . . . . . . . 9 (𝑥𝐴 ↔ (𝐴 ∖ (𝐴𝑥)) = 𝑥)
5654, 55sylib 209 . . . . . . . 8 (𝑥𝑆 → (𝐴 ∖ (𝐴𝑥)) = 𝑥)
5756ad2antlr 709 . . . . . . 7 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ (𝐴𝑥)) = 𝑥)
58 simpr 473 . . . . . . 7 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → 𝑥 ≼ ω)
5957, 58eqbrtrd 4866 . . . . . 6 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ (𝐴𝑥)) ≼ ω)
60 olc 886 . . . . . 6 ((𝐴 ∖ (𝐴𝑥)) ≼ ω → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
6159, 60syl 17 . . . . 5 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
6251, 61jca 503 . . . 4 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → ((𝐴𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
63 breq1 4847 . . . . . 6 (𝑦 = (𝐴𝑥) → (𝑦 ≼ ω ↔ (𝐴𝑥) ≼ ω))
64 difeq2 3921 . . . . . . 7 (𝑦 = (𝐴𝑥) → (𝐴𝑦) = (𝐴 ∖ (𝐴𝑥)))
6564breq1d 4854 . . . . . 6 (𝑦 = (𝐴𝑥) → ((𝐴𝑦) ≼ ω ↔ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
6663, 65orbi12d 933 . . . . 5 (𝑦 = (𝐴𝑥) → ((𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω) ↔ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
67 breq1 4847 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 ≼ ω ↔ 𝑦 ≼ ω))
68 difeq2 3921 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐴𝑥) = (𝐴𝑦))
6968breq1d 4854 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐴𝑥) ≼ ω ↔ (𝐴𝑦) ≼ ω))
7067, 69orbi12d 933 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) ↔ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)))
7170cbvrabv 3389 . . . . . 6 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} = {𝑦 ∈ 𝒫 𝐴 ∣ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)}
721, 71eqtri 2828 . . . . 5 𝑆 = {𝑦 ∈ 𝒫 𝐴 ∣ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)}
7366, 72elrab2 3562 . . . 4 ((𝐴𝑥) ∈ 𝑆 ↔ ((𝐴𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
7462, 73sylibr 225 . . 3 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝑆)
7550ad2antrr 708 . . . . 5 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝒫 𝐴)
761rabeq2i 3387 . . . . . . . . . . 11 (𝑥𝑆 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)))
7776biimpi 207 . . . . . . . . . 10 (𝑥𝑆 → (𝑥 ∈ 𝒫 𝐴 ∧ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)))
7877simprd 485 . . . . . . . . 9 (𝑥𝑆 → (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω))
7978adantl 469 . . . . . . . 8 ((𝜑𝑥𝑆) → (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω))
8079adantr 468 . . . . . . 7 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω))
81 simpr 473 . . . . . . 7 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → ¬ 𝑥 ≼ ω)
82 pm2.53 869 . . . . . . 7 ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) → (¬ 𝑥 ≼ ω → (𝐴𝑥) ≼ ω))
8380, 81, 82sylc 65 . . . . . 6 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴𝑥) ≼ ω)
84 orc 885 . . . . . 6 ((𝐴𝑥) ≼ ω → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
8583, 84syl 17 . . . . 5 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
8675, 85jca 503 . . . 4 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → ((𝐴𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
8786, 73sylibr 225 . . 3 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝑆)
8874, 87pm2.61dan 838 . 2 ((𝜑𝑥𝑆) → (𝐴𝑥) ∈ 𝑆)
89 elpwi 4361 . . . . . . . . . . . 12 (𝑥 ∈ 𝒫 𝑆𝑥𝑆)
9089adantr 468 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑥𝑆)
91 simpr 473 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑦𝑥)
9290, 91sseldd 3799 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑦𝑆)
9341sseli 3794 . . . . . . . . . . 11 (𝑦𝑆𝑦 ∈ 𝒫 𝐴)
94 elpwi 4361 . . . . . . . . . . 11 (𝑦 ∈ 𝒫 𝐴𝑦𝐴)
9593, 94syl 17 . . . . . . . . . 10 (𝑦𝑆𝑦𝐴)
9692, 95syl 17 . . . . . . . . 9 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑦𝐴)
9796ralrimiva 3154 . . . . . . . 8 (𝑥 ∈ 𝒫 𝑆 → ∀𝑦𝑥 𝑦𝐴)
98 unissb 4663 . . . . . . . 8 ( 𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
9997, 98sylibr 225 . . . . . . 7 (𝑥 ∈ 𝒫 𝑆 𝑥𝐴)
100 vuniex 7184 . . . . . . . 8 𝑥 ∈ V
101100elpw 4357 . . . . . . 7 ( 𝑥 ∈ 𝒫 𝐴 𝑥𝐴)
10299, 101sylibr 225 . . . . . 6 (𝑥 ∈ 𝒫 𝑆 𝑥 ∈ 𝒫 𝐴)
103102adantr 468 . . . . 5 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → 𝑥 ∈ 𝒫 𝐴)
104 id 22 . . . . . . . 8 ((𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω) → (𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω))
105104adantll 696 . . . . . . 7 (((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) ∧ ∀𝑦𝑥 𝑦 ≼ ω) → (𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω))
106 unictb 9682 . . . . . . 7 ((𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω) → 𝑥 ≼ ω)
107 orc 885 . . . . . . 7 ( 𝑥 ≼ ω → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
108105, 106, 1073syl 18 . . . . . 6 (((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) ∧ ∀𝑦𝑥 𝑦 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
109 rexnal 3182 . . . . . . . . . . . 12 (∃𝑦𝑥 ¬ 𝑦 ≼ ω ↔ ¬ ∀𝑦𝑥 𝑦 ≼ ω)
110109bicomi 215 . . . . . . . . . . 11 (¬ ∀𝑦𝑥 𝑦 ≼ ω ↔ ∃𝑦𝑥 ¬ 𝑦 ≼ ω)
111110biimpi 207 . . . . . . . . . 10 (¬ ∀𝑦𝑥 𝑦 ≼ ω → ∃𝑦𝑥 ¬ 𝑦 ≼ ω)
112111adantl 469 . . . . . . . . 9 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → ∃𝑦𝑥 ¬ 𝑦 ≼ ω)
113 nfv 2005 . . . . . . . . . . 11 𝑦 𝑥 ∈ 𝒫 𝑆
114 nfra1 3129 . . . . . . . . . . . 12 𝑦𝑦𝑥 𝑦 ≼ ω
115114nfn 1944 . . . . . . . . . . 11 𝑦 ¬ ∀𝑦𝑥 𝑦 ≼ ω
116113, 115nfan 1990 . . . . . . . . . 10 𝑦(𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω)
117 nfv 2005 . . . . . . . . . 10 𝑦(𝐴 𝑥) ≼ ω
118 elssuni 4661 . . . . . . . . . . . . . . 15 (𝑦𝑥𝑦 𝑥)
1191183ad2ant2 1157 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → 𝑦 𝑥)
120119sscond 3946 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴 𝑥) ⊆ (𝐴𝑦))
121923adant3 1155 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → 𝑦𝑆)
122 simp3 1161 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → ¬ 𝑦 ≼ ω)
12372rabeq2i 3387 . . . . . . . . . . . . . . . . . 18 (𝑦𝑆 ↔ (𝑦 ∈ 𝒫 𝐴 ∧ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)))
124123biimpi 207 . . . . . . . . . . . . . . . . 17 (𝑦𝑆 → (𝑦 ∈ 𝒫 𝐴 ∧ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)))
125124simprd 485 . . . . . . . . . . . . . . . 16 (𝑦𝑆 → (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω))
126125adantr 468 . . . . . . . . . . . . . . 15 ((𝑦𝑆 ∧ ¬ 𝑦 ≼ ω) → (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω))
127 simpr 473 . . . . . . . . . . . . . . 15 ((𝑦𝑆 ∧ ¬ 𝑦 ≼ ω) → ¬ 𝑦 ≼ ω)
128 pm2.53 869 . . . . . . . . . . . . . . 15 ((𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω) → (¬ 𝑦 ≼ ω → (𝐴𝑦) ≼ ω))
129126, 127, 128sylc 65 . . . . . . . . . . . . . 14 ((𝑦𝑆 ∧ ¬ 𝑦 ≼ ω) → (𝐴𝑦) ≼ ω)
130121, 122, 129syl2anc 575 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴𝑦) ≼ ω)
131 ssct 8280 . . . . . . . . . . . . 13 (((𝐴 𝑥) ⊆ (𝐴𝑦) ∧ (𝐴𝑦) ≼ ω) → (𝐴 𝑥) ≼ ω)
132120, 130, 131syl2anc 575 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴 𝑥) ≼ ω)
1331323exp 1141 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝑆 → (𝑦𝑥 → (¬ 𝑦 ≼ ω → (𝐴 𝑥) ≼ ω)))
134133adantr 468 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → (𝑦𝑥 → (¬ 𝑦 ≼ ω → (𝐴 𝑥) ≼ ω)))
135116, 117, 134rexlimd 3214 . . . . . . . . 9 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → (∃𝑦𝑥 ¬ 𝑦 ≼ ω → (𝐴 𝑥) ≼ ω))
136112, 135mpd 15 . . . . . . . 8 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → (𝐴 𝑥) ≼ ω)
137 olc 886 . . . . . . . 8 ((𝐴 𝑥) ≼ ω → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
138136, 137syl 17 . . . . . . 7 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
139138adantlr 697 . . . . . 6 (((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
140108, 139pm2.61dan 838 . . . . 5 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
141103, 140jca 503 . . . 4 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω)))
142 breq1 4847 . . . . . 6 (𝑦 = 𝑥 → (𝑦 ≼ ω ↔ 𝑥 ≼ ω))
143 difeq2 3921 . . . . . . 7 (𝑦 = 𝑥 → (𝐴𝑦) = (𝐴 𝑥))
144143breq1d 4854 . . . . . 6 (𝑦 = 𝑥 → ((𝐴𝑦) ≼ ω ↔ (𝐴 𝑥) ≼ ω))
145142, 144orbi12d 933 . . . . 5 (𝑦 = 𝑥 → ((𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω) ↔ ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω)))
146145, 72elrab2 3562 . . . 4 ( 𝑥𝑆 ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω)))
147141, 146sylibr 225 . . 3 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → 𝑥𝑆)
1481473adant1 1153 . 2 ((𝜑𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → 𝑥𝑆)
1496, 20, 45, 88, 148issald 41030 1 (𝜑𝑆 ∈ SAlg)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3a 1100   = wceq 1637  wcel 2156  wral 3096  wrex 3097  {crab 3100  Vcvv 3391  cdif 3766  wss 3769  c0 4116  𝒫 cpw 4351  {csn 4370   cuni 4630   class class class wbr 4844  ωcom 7295  cdom 8190  Fincfn 8192  SAlgcsalg 41007
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-inf2 8785  ax-cc 9542
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-isom 6110  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-om 7296  df-1st 7398  df-2nd 7399  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-oadd 7800  df-er 7979  df-map 8094  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-oi 8654  df-card 9048  df-acn 9051  df-salg 41008
This theorem is referenced by:  salexct3  41039  salgencntex  41040  salgensscntex  41041
  Copyright terms: Public domain W3C validator