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 44565
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 5334 . . . 4 (𝜑 → 𝒫 𝐴 ∈ V)
4 rabexg 5288 . . . 4 (𝒫 𝐴 ∈ V → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} ∈ V)
53, 4syl 17 . . 3 (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} ∈ V)
61, 5eqeltrid 2842 . 2 (𝜑𝑆 ∈ V)
7 0elpw 5311 . . . . 5 ∅ ∈ 𝒫 𝐴
87a1i 11 . . . 4 (𝜑 → ∅ ∈ 𝒫 𝐴)
9 0fin 9115 . . . . . . 7 ∅ ∈ Fin
10 fict 9589 . . . . . . 7 (∅ ∈ Fin → ∅ ≼ ω)
119, 10ax-mp 5 . . . . . 6 ∅ ≼ ω
1211orci 863 . . . . 5 (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)
1312a1i 11 . . . 4 (𝜑 → (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω))
148, 13jca 512 . . 3 (𝜑 → (∅ ∈ 𝒫 𝐴 ∧ (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)))
15 breq1 5108 . . . . 5 (𝑥 = ∅ → (𝑥 ≼ ω ↔ ∅ ≼ ω))
16 difeq2 4076 . . . . . 6 (𝑥 = ∅ → (𝐴𝑥) = (𝐴 ∖ ∅))
1716breq1d 5115 . . . . 5 (𝑥 = ∅ → ((𝐴𝑥) ≼ ω ↔ (𝐴 ∖ ∅) ≼ ω))
1815, 17orbi12d 917 . . . 4 (𝑥 = ∅ → ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) ↔ (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)))
1918, 1elrab2 3648 . . 3 (∅ ∈ 𝑆 ↔ (∅ ∈ 𝒫 𝐴 ∧ (∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼ ω)))
2014, 19sylibr 233 . 2 (𝜑 → ∅ ∈ 𝑆)
21 snidg 4620 . . . . . 6 (𝑦𝐴𝑦 ∈ {𝑦})
22 snelpwi 5400 . . . . . . . 8 (𝑦𝐴 → {𝑦} ∈ 𝒫 𝐴)
23 snfi 8988 . . . . . . . . . . 11 {𝑦} ∈ Fin
24 fict 9589 . . . . . . . . . . 11 ({𝑦} ∈ Fin → {𝑦} ≼ ω)
2523, 24ax-mp 5 . . . . . . . . . 10 {𝑦} ≼ ω
2625orci 863 . . . . . . . . 9 ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)
2726a1i 11 . . . . . . . 8 (𝑦𝐴 → ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))
2822, 27jca 512 . . . . . . 7 (𝑦𝐴 → ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
29 breq1 5108 . . . . . . . . 9 (𝑥 = {𝑦} → (𝑥 ≼ ω ↔ {𝑦} ≼ ω))
30 difeq2 4076 . . . . . . . . . 10 (𝑥 = {𝑦} → (𝐴𝑥) = (𝐴 ∖ {𝑦}))
3130breq1d 5115 . . . . . . . . 9 (𝑥 = {𝑦} → ((𝐴𝑥) ≼ ω ↔ (𝐴 ∖ {𝑦}) ≼ ω))
3229, 31orbi12d 917 . . . . . . . 8 (𝑥 = {𝑦} → ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) ↔ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
3332, 1elrab2 3648 . . . . . . 7 ({𝑦} ∈ 𝑆 ↔ ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)))
3428, 33sylibr 233 . . . . . 6 (𝑦𝐴 → {𝑦} ∈ 𝑆)
35 elunii 4870 . . . . . 6 ((𝑦 ∈ {𝑦} ∧ {𝑦} ∈ 𝑆) → 𝑦 𝑆)
3621, 34, 35syl2anc 584 . . . . 5 (𝑦𝐴𝑦 𝑆)
3736rgen 3066 . . . 4 𝑦𝐴 𝑦 𝑆
38 dfss3 3932 . . . 4 (𝐴 𝑆 ↔ ∀𝑦𝐴 𝑦 𝑆)
3937, 38mpbir 230 . . 3 𝐴 𝑆
40 ssrab2 4037 . . . . . 6 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} ⊆ 𝒫 𝐴
411, 40eqsstri 3978 . . . . 5 𝑆 ⊆ 𝒫 𝐴
4241unissi 4874 . . . 4 𝑆 𝒫 𝐴
43 unipw 5407 . . . 4 𝒫 𝐴 = 𝐴
4442, 43sseqtri 3980 . . 3 𝑆𝐴
4539, 44eqssi 3960 . 2 𝐴 = 𝑆
46 difssd 4092 . . . . . . 7 (𝜑 → (𝐴𝑥) ⊆ 𝐴)
472, 46ssexd 5281 . . . . . . . 8 (𝜑 → (𝐴𝑥) ∈ V)
48 elpwg 4563 . . . . . . . 8 ((𝐴𝑥) ∈ V → ((𝐴𝑥) ∈ 𝒫 𝐴 ↔ (𝐴𝑥) ⊆ 𝐴))
4947, 48syl 17 . . . . . . 7 (𝜑 → ((𝐴𝑥) ∈ 𝒫 𝐴 ↔ (𝐴𝑥) ⊆ 𝐴))
5046, 49mpbird 256 . . . . . 6 (𝜑 → (𝐴𝑥) ∈ 𝒫 𝐴)
5150ad2antrr 724 . . . . 5 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝒫 𝐴)
5241sseli 3940 . . . . . . . . . 10 (𝑥𝑆𝑥 ∈ 𝒫 𝐴)
53 elpwi 4567 . . . . . . . . . 10 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
5452, 53syl 17 . . . . . . . . 9 (𝑥𝑆𝑥𝐴)
55 dfss4 4218 . . . . . . . . 9 (𝑥𝐴 ↔ (𝐴 ∖ (𝐴𝑥)) = 𝑥)
5654, 55sylib 217 . . . . . . . 8 (𝑥𝑆 → (𝐴 ∖ (𝐴𝑥)) = 𝑥)
5756ad2antlr 725 . . . . . . 7 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ (𝐴𝑥)) = 𝑥)
58 simpr 485 . . . . . . 7 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → 𝑥 ≼ ω)
5957, 58eqbrtrd 5127 . . . . . 6 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ (𝐴𝑥)) ≼ ω)
60 olc 866 . . . . . 6 ((𝐴 ∖ (𝐴𝑥)) ≼ ω → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
6159, 60syl 17 . . . . 5 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
6251, 61jca 512 . . . 4 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → ((𝐴𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
63 breq1 5108 . . . . . 6 (𝑦 = (𝐴𝑥) → (𝑦 ≼ ω ↔ (𝐴𝑥) ≼ ω))
64 difeq2 4076 . . . . . . 7 (𝑦 = (𝐴𝑥) → (𝐴𝑦) = (𝐴 ∖ (𝐴𝑥)))
6564breq1d 5115 . . . . . 6 (𝑦 = (𝐴𝑥) → ((𝐴𝑦) ≼ ω ↔ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
6663, 65orbi12d 917 . . . . 5 (𝑦 = (𝐴𝑥) → ((𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω) ↔ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
67 breq1 5108 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 ≼ ω ↔ 𝑦 ≼ ω))
68 difeq2 4076 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐴𝑥) = (𝐴𝑦))
6968breq1d 5115 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐴𝑥) ≼ ω ↔ (𝐴𝑦) ≼ ω))
7067, 69orbi12d 917 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) ↔ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)))
7170cbvrabv 3417 . . . . . 6 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)} = {𝑦 ∈ 𝒫 𝐴 ∣ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)}
721, 71eqtri 2764 . . . . 5 𝑆 = {𝑦 ∈ 𝒫 𝐴 ∣ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)}
7366, 72elrab2 3648 . . . 4 ((𝐴𝑥) ∈ 𝑆 ↔ ((𝐴𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
7462, 73sylibr 233 . . 3 (((𝜑𝑥𝑆) ∧ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝑆)
7550ad2antrr 724 . . . . 5 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝒫 𝐴)
761reqabi 3429 . . . . . . . . . . 11 (𝑥𝑆 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)))
7776biimpi 215 . . . . . . . . . 10 (𝑥𝑆 → (𝑥 ∈ 𝒫 𝐴 ∧ (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω)))
7877simprd 496 . . . . . . . . 9 (𝑥𝑆 → (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω))
7978adantl 482 . . . . . . . 8 ((𝜑𝑥𝑆) → (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω))
8079adantr 481 . . . . . . 7 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω))
81 simpr 485 . . . . . . 7 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → ¬ 𝑥 ≼ ω)
82 pm2.53 849 . . . . . . 7 ((𝑥 ≼ ω ∨ (𝐴𝑥) ≼ ω) → (¬ 𝑥 ≼ ω → (𝐴𝑥) ≼ ω))
8380, 81, 82sylc 65 . . . . . 6 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴𝑥) ≼ ω)
84 orc 865 . . . . . 6 ((𝐴𝑥) ≼ ω → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
8583, 84syl 17 . . . . 5 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω))
8675, 85jca 512 . . . 4 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → ((𝐴𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴𝑥)) ≼ ω)))
8786, 73sylibr 233 . . 3 (((𝜑𝑥𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴𝑥) ∈ 𝑆)
8874, 87pm2.61dan 811 . 2 ((𝜑𝑥𝑆) → (𝐴𝑥) ∈ 𝑆)
89 elpwi 4567 . . . . . . . . . . . 12 (𝑥 ∈ 𝒫 𝑆𝑥𝑆)
9089adantr 481 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑥𝑆)
91 simpr 485 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑦𝑥)
9290, 91sseldd 3945 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑦𝑆)
9341sseli 3940 . . . . . . . . . . 11 (𝑦𝑆𝑦 ∈ 𝒫 𝐴)
94 elpwi 4567 . . . . . . . . . . 11 (𝑦 ∈ 𝒫 𝐴𝑦𝐴)
9593, 94syl 17 . . . . . . . . . 10 (𝑦𝑆𝑦𝐴)
9692, 95syl 17 . . . . . . . . 9 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥) → 𝑦𝐴)
9796ralrimiva 3143 . . . . . . . 8 (𝑥 ∈ 𝒫 𝑆 → ∀𝑦𝑥 𝑦𝐴)
98 unissb 4900 . . . . . . . 8 ( 𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
9997, 98sylibr 233 . . . . . . 7 (𝑥 ∈ 𝒫 𝑆 𝑥𝐴)
100 vuniex 7676 . . . . . . . 8 𝑥 ∈ V
101100elpw 4564 . . . . . . 7 ( 𝑥 ∈ 𝒫 𝐴 𝑥𝐴)
10299, 101sylibr 233 . . . . . 6 (𝑥 ∈ 𝒫 𝑆 𝑥 ∈ 𝒫 𝐴)
103102adantr 481 . . . . 5 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → 𝑥 ∈ 𝒫 𝐴)
104 id 22 . . . . . . . 8 ((𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω) → (𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω))
105104adantll 712 . . . . . . 7 (((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) ∧ ∀𝑦𝑥 𝑦 ≼ ω) → (𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω))
106 unictb 10511 . . . . . . 7 ((𝑥 ≼ ω ∧ ∀𝑦𝑥 𝑦 ≼ ω) → 𝑥 ≼ ω)
107 orc 865 . . . . . . 7 ( 𝑥 ≼ ω → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
108105, 106, 1073syl 18 . . . . . 6 (((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) ∧ ∀𝑦𝑥 𝑦 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
109 rexnal 3103 . . . . . . . . . . . 12 (∃𝑦𝑥 ¬ 𝑦 ≼ ω ↔ ¬ ∀𝑦𝑥 𝑦 ≼ ω)
110109bicomi 223 . . . . . . . . . . 11 (¬ ∀𝑦𝑥 𝑦 ≼ ω ↔ ∃𝑦𝑥 ¬ 𝑦 ≼ ω)
111110biimpi 215 . . . . . . . . . 10 (¬ ∀𝑦𝑥 𝑦 ≼ ω → ∃𝑦𝑥 ¬ 𝑦 ≼ ω)
112111adantl 482 . . . . . . . . 9 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → ∃𝑦𝑥 ¬ 𝑦 ≼ ω)
113 nfv 1917 . . . . . . . . . . 11 𝑦 𝑥 ∈ 𝒫 𝑆
114 nfra1 3267 . . . . . . . . . . . 12 𝑦𝑦𝑥 𝑦 ≼ ω
115114nfn 1860 . . . . . . . . . . 11 𝑦 ¬ ∀𝑦𝑥 𝑦 ≼ ω
116113, 115nfan 1902 . . . . . . . . . 10 𝑦(𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω)
117 nfv 1917 . . . . . . . . . 10 𝑦(𝐴 𝑥) ≼ ω
118 elssuni 4898 . . . . . . . . . . . . . . 15 (𝑦𝑥𝑦 𝑥)
1191183ad2ant2 1134 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → 𝑦 𝑥)
120119sscond 4101 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴 𝑥) ⊆ (𝐴𝑦))
121923adant3 1132 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → 𝑦𝑆)
122 simp3 1138 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → ¬ 𝑦 ≼ ω)
12372reqabi 3429 . . . . . . . . . . . . . . . . . 18 (𝑦𝑆 ↔ (𝑦 ∈ 𝒫 𝐴 ∧ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)))
124123biimpi 215 . . . . . . . . . . . . . . . . 17 (𝑦𝑆 → (𝑦 ∈ 𝒫 𝐴 ∧ (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω)))
125124simprd 496 . . . . . . . . . . . . . . . 16 (𝑦𝑆 → (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω))
126125adantr 481 . . . . . . . . . . . . . . 15 ((𝑦𝑆 ∧ ¬ 𝑦 ≼ ω) → (𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω))
127 simpr 485 . . . . . . . . . . . . . . 15 ((𝑦𝑆 ∧ ¬ 𝑦 ≼ ω) → ¬ 𝑦 ≼ ω)
128 pm2.53 849 . . . . . . . . . . . . . . 15 ((𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω) → (¬ 𝑦 ≼ ω → (𝐴𝑦) ≼ ω))
129126, 127, 128sylc 65 . . . . . . . . . . . . . 14 ((𝑦𝑆 ∧ ¬ 𝑦 ≼ ω) → (𝐴𝑦) ≼ ω)
130121, 122, 129syl2anc 584 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴𝑦) ≼ ω)
131 ssct 8995 . . . . . . . . . . . . 13 (((𝐴 𝑥) ⊆ (𝐴𝑦) ∧ (𝐴𝑦) ≼ ω) → (𝐴 𝑥) ≼ ω)
132120, 130, 131syl2anc 584 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 𝑆𝑦𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴 𝑥) ≼ ω)
1331323exp 1119 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝑆 → (𝑦𝑥 → (¬ 𝑦 ≼ ω → (𝐴 𝑥) ≼ ω)))
134133adantr 481 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → (𝑦𝑥 → (¬ 𝑦 ≼ ω → (𝐴 𝑥) ≼ ω)))
135116, 117, 134rexlimd 3249 . . . . . . . . 9 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → (∃𝑦𝑥 ¬ 𝑦 ≼ ω → (𝐴 𝑥) ≼ ω))
136112, 135mpd 15 . . . . . . . 8 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → (𝐴 𝑥) ≼ ω)
137 olc 866 . . . . . . . 8 ((𝐴 𝑥) ≼ ω → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
138136, 137syl 17 . . . . . . 7 ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
139138adantlr 713 . . . . . 6 (((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) ∧ ¬ ∀𝑦𝑥 𝑦 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
140108, 139pm2.61dan 811 . . . . 5 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω))
141103, 140jca 512 . . . 4 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω)))
142 breq1 5108 . . . . . 6 (𝑦 = 𝑥 → (𝑦 ≼ ω ↔ 𝑥 ≼ ω))
143 difeq2 4076 . . . . . . 7 (𝑦 = 𝑥 → (𝐴𝑦) = (𝐴 𝑥))
144143breq1d 5115 . . . . . 6 (𝑦 = 𝑥 → ((𝐴𝑦) ≼ ω ↔ (𝐴 𝑥) ≼ ω))
145142, 144orbi12d 917 . . . . 5 (𝑦 = 𝑥 → ((𝑦 ≼ ω ∨ (𝐴𝑦) ≼ ω) ↔ ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω)))
146145, 72elrab2 3648 . . . 4 ( 𝑥𝑆 ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝑥 ≼ ω ∨ (𝐴 𝑥) ≼ ω)))
147141, 146sylibr 233 . . 3 ((𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → 𝑥𝑆)
1481473adant1 1130 . 2 ((𝜑𝑥 ∈ 𝒫 𝑆𝑥 ≼ ω) → 𝑥𝑆)
1496, 20, 45, 88, 148issald 44564 1 (𝜑𝑆 ∈ SAlg)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  cdif 3907  wss 3910  c0 4282  𝒫 cpw 4560  {csn 4586   cuni 4865   class class class wbr 5105  ωcom 7802  cdom 8881  Fincfn 8883  SAlgcsalg 44539
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cc 10371
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-oi 9446  df-card 9875  df-acn 9878  df-salg 44540
This theorem is referenced by:  salexct3  44573  salgencntex  44574  salgensscntex  44575
  Copyright terms: Public domain W3C validator