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 46349
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 5379 . . . 4 (𝜑 → 𝒫 𝐴 ∈ V)
4 rabexg 5337 . . . 4 (𝒫 𝐴 ∈ V → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} ∈ V)
53, 4syl 17 . . 3 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} ∈ V)
61, 5eqeltrid 2845 . 2 (𝜑𝑆 ∈ V)
7 0elpw 5356 . . . . 5 ∅ ∈ 𝒫 𝐴
87a1i 11 . . . 4 (𝜑 → ∅ ∈ 𝒫 𝐴)
9 0fi 9082 . . . . . . 7 ∅ ∈ Fin
10 fict 9693 . . . . . . 7 (∅ ∈ Fin → ∅ ≼ ω)
119, 10ax-mp 5 . . . . . 6 ∅ ≼ ω
1211orci 866 . . . . 5 (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)
1312a1i 11 . . . 4 (𝜑 → (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω))
148, 13jca 511 . . 3 (𝜑 → (∅ ∈ 𝒫 𝐴 ∧ (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)))
15 breq1 5146 . . . . 5 (𝑥 = ∅ → (𝑥 ≼ ω ↔ ∅ ≼ ω))
16 difeq2 4120 . . . . . 6 (𝑥 = ∅ → (𝐴𝑥) = (𝐴 ∖ ∅))
1716breq1d 5153 . . . . 5 (𝑥 = ∅ → ((𝐴𝑥) ≼ ω ↔ (𝐴 ∖ ∅) ≼ ω))
1815, 17orbi12d 919 . . . 4 (𝑥 = ∅ → ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) ↔ (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)))
1918, 1elrab2 3695 . . 3 (∅ ∈ 𝑆 ↔ (∅ ∈ 𝒫 𝐴 ∧ (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)))
2014, 19sylibr 234 . 2 (𝜑 → ∅ ∈ 𝑆)
21 snidg 4660 . . . . . 6 (𝑦𝐴𝑦 ∈ {𝑦})
22 snelpwi 5448 . . . . . . . 8 (𝑦𝐴 → {𝑦} ∈ 𝒫 𝐴)
23 snfi 9083 . . . . . . . . . . 11 {𝑦} ∈ Fin
24 fict 9693 . . . . . . . . . . 11 ({𝑦} ∈ Fin → {𝑦} ≼ ω)
2523, 24ax-mp 5 . . . . . . . . . 10 {𝑦} ≼ ω
2625orci 866 . . . . . . . . 9 ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)
2726a1i 11 . . . . . . . 8 (𝑦𝐴 → ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))
2822, 27jca 511 . . . . . . 7 (𝑦𝐴 → ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
29 breq1 5146 . . . . . . . . 9 (𝑥 = {𝑦} → (𝑥 ≼ ω ↔ {𝑦} ≼ ω))
30 difeq2 4120 . . . . . . . . . 10 (𝑥 = {𝑦} → (𝐴𝑥) = (𝐴 ∖ {𝑦}))
3130breq1d 5153 . . . . . . . . 9 (𝑥 = {𝑦} → ((𝐴𝑥) ≼ ω ↔ (𝐴 ∖ {𝑦}) ≼ ω))
3229, 31orbi12d 919 . . . . . . . 8 (𝑥 = {𝑦} → ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) ↔ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
3332, 1elrab2 3695 . . . . . . 7 ({𝑦} ∈ 𝑆 ↔ ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
3428, 33sylibr 234 . . . . . 6 (𝑦𝐴 → {𝑦} ∈ 𝑆)
35 elunii 4912 . . . . . 6 ((𝑦 ∈ {𝑦} ∧ {𝑦} ∈ 𝑆) → 𝑦 𝑆)
3621, 34, 35syl2anc 584 . . . . 5 (𝑦𝐴𝑦 𝑆)
3736rgen 3063 . . . 4 𝑦𝐴 𝑦 𝑆
38 dfss3 3972 . . . 4 (𝐴 𝑆 ↔ ∀𝑦𝐴 𝑦 𝑆)
3937, 38mpbir 231 . . 3 𝐴 𝑆
40 ssrab2 4080 . . . . . 6 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} ⊆ 𝒫 𝐴
411, 40eqsstri 4030 . . . . 5 𝑆 ⊆ 𝒫 𝐴
4241unissi 4916 . . . 4 𝑆 𝒫 𝐴
43 unipw 5455 . . . 4 𝒫 𝐴 = 𝐴
4442, 43sseqtri 4032 . . 3 𝑆𝐴
4539, 44eqssi 4000 . 2 𝐴 = 𝑆
46 difssd 4137 . . . . . . 7 (𝜑 → (𝐴𝑥) ⊆ 𝐴)
472, 46ssexd 5324 . . . . . . . 8 (𝜑 → (𝐴𝑥) ∈ V)
48 elpwg 4603 . . . . . . . 8 ((𝐴𝑥) ∈ V → ((𝐴𝑥) ∈ 𝒫 𝐴 ↔ (𝐴𝑥) ⊆ 𝐴))
4947, 48syl 17 . . . . . . 7 (𝜑 → ((𝐴𝑥) ∈ 𝒫 𝐴 ↔ (𝐴𝑥) ⊆ 𝐴))
5046, 49mpbird 257 . . . . . 6 (𝜑 → (𝐴𝑥) ∈ 𝒫 𝐴)
5150ad2antrr 726 . . . . 5 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝒫 𝐴)
5241sseli 3979 . . . . . . . . . 10 (𝑥𝑆𝑥 ∈ 𝒫 𝐴)
53 elpwi 4607 . . . . . . . . . 10 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
5452, 53syl 17 . . . . . . . . 9 (𝑥𝑆𝑥𝐴)
55 dfss4 4269 . . . . . . . . 9 (𝑥𝐴 ↔ (𝐴 ∖ (𝐴𝑥)) = 𝑥)
5654, 55sylib 218 . . . . . . . 8 (𝑥𝑆 → (𝐴 ∖ (𝐴𝑥)) = 𝑥)
5756ad2antlr 727 . . . . . . 7 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ (𝐴𝑥)) = 𝑥)
58 simpr 484 . . . . . . 7 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → 𝑥 ≼ ω)
5957, 58eqbrtrd 5165 . . . . . 6 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ (𝐴𝑥)) ≼ ω)
60 olc 869 . . . . . 6 ((𝐴 ∖ (𝐴𝑥)) ≼ ω → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
6159, 60syl 17 . . . . 5 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
6251, 61jca 511 . . . 4 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → ((𝐴𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
63 breq1 5146 . . . . . 6 (𝑦 = (𝐴𝑥) → (𝑦 ≼ ω ↔ (𝐴𝑥) ≼ ω))
64 difeq2 4120 . . . . . . 7 (𝑦 = (𝐴𝑥) → (𝐴𝑦) = (𝐴 ∖ (𝐴𝑥)))
6564breq1d 5153 . . . . . 6 (𝑦 = (𝐴𝑥) → ((𝐴𝑦) ≼ ω ↔ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
6663, 65orbi12d 919 . . . . 5 (𝑦 = (𝐴𝑥) → ((𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω) ↔ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
67 breq1 5146 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 ≼ ω ↔ 𝑦 ≼ ω))
68 difeq2 4120 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐴𝑥) = (𝐴𝑦))
6968breq1d 5153 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐴𝑥) ≼ ω ↔ (𝐴𝑦) ≼ ω))
7067, 69orbi12d 919 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) ↔ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)))
7170cbvrabv 3447 . . . . . 6 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} = {𝑦 ∈ 𝒫 𝐴 ∣ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)}
721, 71eqtri 2765 . . . . 5 𝑆 = {𝑦 ∈ 𝒫 𝐴 ∣ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)}
7366, 72elrab2 3695 . . . 4 ((𝐴𝑥) ∈ 𝑆 ↔ ((𝐴𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
7462, 73sylibr 234 . . 3 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝑆)
7550ad2antrr 726 . . . . 5 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝒫 𝐴)
761reqabi 3460 . . . . . . . . . . 11 (𝑥𝑆 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)))
7776biimpi 216 . . . . . . . . . 10 (𝑥𝑆 → (𝑥 ∈ 𝒫 𝐴 ∧ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)))
7877simprd 495 . . . . . . . . 9 (𝑥𝑆 → (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω))
7978adantl 481 . . . . . . . 8 ((𝜑𝑥𝑆) → (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω))
8079adantr 480 . . . . . . 7 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω))
81 simpr 484 . . . . . . 7 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → ¬ 𝑥 ≼ ω)
82 pm2.53 852 . . . . . . 7 ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) → (¬ 𝑥 ≼ ω → (𝐴𝑥) ≼ ω))
8380, 81, 82sylc 65 . . . . . 6 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴𝑥) ≼ ω)
84 orc 868 . . . . . 6 ((𝐴𝑥) ≼ ω → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
8583, 84syl 17 . . . . 5 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
8675, 85jca 511 . . . 4 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → ((𝐴𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
8786, 73sylibr 234 . . 3 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝑆)
8874, 87pm2.61dan 813 . 2 ((𝜑𝑥𝑆) → (𝐴𝑥) ∈ 𝑆)
89 elpwi 4607 . . . . . . . . . . . 12 (𝑥 ∈ 𝒫 𝑆𝑥𝑆)
9089adantr 480 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑥𝑆)
91 simpr 484 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑦𝑥)
9290, 91sseldd 3984 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑦𝑆)
9341sseli 3979 . . . . . . . . . . 11 (𝑦𝑆𝑦 ∈ 𝒫 𝐴)
94 elpwi 4607 . . . . . . . . . . 11 (𝑦 ∈ 𝒫 𝐴𝑦𝐴)
9593, 94syl 17 . . . . . . . . . 10 (𝑦𝑆𝑦𝐴)
9692, 95syl 17 . . . . . . . . 9 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑦𝐴)
9796ralrimiva 3146 . . . . . . . 8 (𝑥 ∈ 𝒫 𝑆 → ∀𝑦𝑥 𝑦𝐴)
98 unissb 4939 . . . . . . . 8 ( 𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
9997, 98sylibr 234 . . . . . . 7 (𝑥 ∈ 𝒫 𝑆 𝑥𝐴)
100 vuniex 7759 . . . . . . . 8 𝑥 ∈ V
101100elpw 4604 . . . . . . 7 ( 𝑥 ∈ 𝒫 𝐴 𝑥𝐴)
10299, 101sylibr 234 . . . . . 6 (𝑥 ∈ 𝒫 𝑆 𝑥 ∈ 𝒫 𝐴)
103102adantr 480 . . . . 5 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → 𝑥 ∈ 𝒫 𝐴)
104 id 22 . . . . . . . 8 ((𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω) → (𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω))
105104adantll 714 . . . . . . 7 (((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) ∧ ∀𝑦𝑥 𝑦 ≼ ω) → (𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω))
106 unictb 10615 . . . . . . 7 ((𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω) → 𝑥 ≼ ω)
107 orc 868 . . . . . . 7 ( 𝑥 ≼ ω → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
108105, 106, 1073syl 18 . . . . . 6 (((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) ∧ ∀𝑦𝑥 𝑦 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
109 rexnal 3100 . . . . . . . . . . . 12 (∃𝑦𝑥 ¬ 𝑦 ≼ ω ↔ ¬ ∀𝑦𝑥 𝑦 ≼ ω)
110109bicomi 224 . . . . . . . . . . 11 (¬ ∀𝑦𝑥 𝑦 ≼ ω ↔ ∃𝑦𝑥 ¬ 𝑦 ≼ ω)
111110biimpi 216 . . . . . . . . . 10 (¬ ∀𝑦𝑥 𝑦 ≼ ω → ∃𝑦𝑥 ¬ 𝑦 ≼ ω)
112111adantl 481 . . . . . . . . 9 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → ∃𝑦𝑥 ¬ 𝑦 ≼ ω)
113 nfv 1914 . . . . . . . . . . 11 𝑦 𝑥 ∈ 𝒫 𝑆
114 nfra1 3284 . . . . . . . . . . . 12 𝑦𝑦𝑥 𝑦 ≼ ω
115114nfn 1857 . . . . . . . . . . 11 𝑦 ¬ ∀𝑦𝑥 𝑦 ≼ ω
116113, 115nfan 1899 . . . . . . . . . 10 𝑦(𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω)
117 nfv 1914 . . . . . . . . . 10 𝑦(𝐴 𝑥) ≼ ω
118 elssuni 4937 . . . . . . . . . . . . . . 15 (𝑦𝑥𝑦 𝑥)
1191183ad2ant2 1135 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → 𝑦 𝑥)
120119sscond 4146 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴 𝑥) ⊆ (𝐴𝑦))
121923adant3 1133 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → 𝑦𝑆)
122 simp3 1139 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → ¬ 𝑦 ≼ ω)
12372reqabi 3460 . . . . . . . . . . . . . . . . . 18 (𝑦𝑆 ↔ (𝑦 ∈ 𝒫 𝐴 ∧ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)))
124123biimpi 216 . . . . . . . . . . . . . . . . 17 (𝑦𝑆 → (𝑦 ∈ 𝒫 𝐴 ∧ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)))
125124simprd 495 . . . . . . . . . . . . . . . 16 (𝑦𝑆 → (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω))
126125adantr 480 . . . . . . . . . . . . . . 15 ((𝑦𝑆 ∧ ¬ 𝑦 ≼ ω) → (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω))
127 simpr 484 . . . . . . . . . . . . . . 15 ((𝑦𝑆 ∧ ¬ 𝑦 ≼ ω) → ¬ 𝑦 ≼ ω)
128 pm2.53 852 . . . . . . . . . . . . . . 15 ((𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω) → (¬ 𝑦 ≼ ω → (𝐴𝑦) ≼ ω))
129126, 127, 128sylc 65 . . . . . . . . . . . . . 14 ((𝑦𝑆 ∧ ¬ 𝑦 ≼ ω) → (𝐴𝑦) ≼ ω)
130121, 122, 129syl2anc 584 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴𝑦) ≼ ω)
131 ssct 9091 . . . . . . . . . . . . 13 (((𝐴 𝑥) ⊆ (𝐴𝑦) ∧ (𝐴𝑦) ≼ ω) → (𝐴 𝑥) ≼ ω)
132120, 130, 131syl2anc 584 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴 𝑥) ≼ ω)
1331323exp 1120 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝑆 → (𝑦𝑥 → (¬ 𝑦 ≼ ω → (𝐴 𝑥) ≼ ω)))
134133adantr 480 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → (𝑦𝑥 → (¬ 𝑦 ≼ ω → (𝐴 𝑥) ≼ ω)))
135116, 117, 134rexlimd 3266 . . . . . . . . 9 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → (∃𝑦𝑥 ¬ 𝑦 ≼ ω → (𝐴 𝑥) ≼ ω))
136112, 135mpd 15 . . . . . . . 8 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → (𝐴 𝑥) ≼ ω)
137 olc 869 . . . . . . . 8 ((𝐴 𝑥) ≼ ω → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
138136, 137syl 17 . . . . . . 7 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
139138adantlr 715 . . . . . 6 (((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
140108, 139pm2.61dan 813 . . . . 5 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
141103, 140jca 511 . . . 4 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω)))
142 breq1 5146 . . . . . 6 (𝑦 = 𝑥 → (𝑦 ≼ ω ↔ 𝑥 ≼ ω))
143 difeq2 4120 . . . . . . 7 (𝑦 = 𝑥 → (𝐴𝑦) = (𝐴 𝑥))
144143breq1d 5153 . . . . . 6 (𝑦 = 𝑥 → ((𝐴𝑦) ≼ ω ↔ (𝐴 𝑥) ≼ ω))
145142, 144orbi12d 919 . . . . 5 (𝑦 = 𝑥 → ((𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω) ↔ ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω)))
146145, 72elrab2 3695 . . . 4 ( 𝑥𝑆 ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω)))
147141, 146sylibr 234 . . 3 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → 𝑥𝑆)
1481473adant1 1131 . 2 ((𝜑𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → 𝑥𝑆)
1496, 20, 45, 88, 148issald 46348 1 (𝜑𝑆 ∈ SAlg)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  w3a 1087   = wceq 1540  wcel 2108  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  cdif 3948  wss 3951  c0 4333  𝒫 cpw 4600  {csn 4626   cuni 4907   class class class wbr 5143  ωcom 7887  cdom 8983  Fincfn 8985  SAlgcsalg 46323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cc 10475
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-oi 9550  df-card 9979  df-acn 9982  df-salg 46324
This theorem is referenced by:  salexct3  46357  salgencntex  46358  salgensscntex  46359
  Copyright terms: Public domain W3C validator