| Step | Hyp | Ref
| Expression |
| 1 | | salexct.b |
. . 3
⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)} |
| 2 | | salexct.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 3 | 2 | pwexd 5379 |
. . . 4
⊢ (𝜑 → 𝒫 𝐴 ∈ V) |
| 4 | | rabexg 5337 |
. . . 4
⊢
(𝒫 𝐴 ∈
V → {𝑥 ∈
𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)} ∈
V) |
| 5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)} ∈
V) |
| 6 | 1, 5 | eqeltrid 2845 |
. 2
⊢ (𝜑 → 𝑆 ∈ V) |
| 7 | | 0elpw 5356 |
. . . . 5
⊢ ∅
∈ 𝒫 𝐴 |
| 8 | 7 | a1i 11 |
. . . 4
⊢ (𝜑 → ∅ ∈ 𝒫
𝐴) |
| 9 | | 0fi 9082 |
. . . . . . 7
⊢ ∅
∈ Fin |
| 10 | | fict 9693 |
. . . . . . 7
⊢ (∅
∈ Fin → ∅ ≼ ω) |
| 11 | 9, 10 | ax-mp 5 |
. . . . . 6
⊢ ∅
≼ ω |
| 12 | 11 | orci 866 |
. . . . 5
⊢ (∅
≼ ω ∨ (𝐴
∖ ∅) ≼ ω) |
| 13 | 12 | a1i 11 |
. . . 4
⊢ (𝜑 → (∅ ≼ ω
∨ (𝐴 ∖ ∅)
≼ ω)) |
| 14 | 8, 13 | jca 511 |
. . 3
⊢ (𝜑 → (∅ ∈ 𝒫
𝐴 ∧ (∅ ≼
ω ∨ (𝐴 ∖
∅) ≼ ω))) |
| 15 | | breq1 5146 |
. . . . 5
⊢ (𝑥 = ∅ → (𝑥 ≼ ω ↔ ∅
≼ ω)) |
| 16 | | difeq2 4120 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐴 ∖ 𝑥) = (𝐴 ∖ ∅)) |
| 17 | 16 | breq1d 5153 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝐴 ∖ 𝑥) ≼ ω ↔ (𝐴 ∖ ∅) ≼
ω)) |
| 18 | 15, 17 | orbi12d 919 |
. . . 4
⊢ (𝑥 = ∅ → ((𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω) ↔ (∅ ≼
ω ∨ (𝐴 ∖
∅) ≼ ω))) |
| 19 | 18, 1 | elrab2 3695 |
. . 3
⊢ (∅
∈ 𝑆 ↔ (∅
∈ 𝒫 𝐴 ∧
(∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼
ω))) |
| 20 | 14, 19 | sylibr 234 |
. 2
⊢ (𝜑 → ∅ ∈ 𝑆) |
| 21 | | snidg 4660 |
. . . . . 6
⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ {𝑦}) |
| 22 | | snelpwi 5448 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝒫 𝐴) |
| 23 | | snfi 9083 |
. . . . . . . . . . 11
⊢ {𝑦} ∈ Fin |
| 24 | | fict 9693 |
. . . . . . . . . . 11
⊢ ({𝑦} ∈ Fin → {𝑦} ≼
ω) |
| 25 | 23, 24 | ax-mp 5 |
. . . . . . . . . 10
⊢ {𝑦} ≼
ω |
| 26 | 25 | orci 866 |
. . . . . . . . 9
⊢ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω) |
| 27 | 26 | a1i 11 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)) |
| 28 | 22, 27 | jca 511 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 → ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))) |
| 29 | | breq1 5146 |
. . . . . . . . 9
⊢ (𝑥 = {𝑦} → (𝑥 ≼ ω ↔ {𝑦} ≼ ω)) |
| 30 | | difeq2 4120 |
. . . . . . . . . 10
⊢ (𝑥 = {𝑦} → (𝐴 ∖ 𝑥) = (𝐴 ∖ {𝑦})) |
| 31 | 30 | breq1d 5153 |
. . . . . . . . 9
⊢ (𝑥 = {𝑦} → ((𝐴 ∖ 𝑥) ≼ ω ↔ (𝐴 ∖ {𝑦}) ≼ ω)) |
| 32 | 29, 31 | orbi12d 919 |
. . . . . . . 8
⊢ (𝑥 = {𝑦} → ((𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω) ↔ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))) |
| 33 | 32, 1 | elrab2 3695 |
. . . . . . 7
⊢ ({𝑦} ∈ 𝑆 ↔ ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))) |
| 34 | 28, 33 | sylibr 234 |
. . . . . 6
⊢ (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝑆) |
| 35 | | elunii 4912 |
. . . . . 6
⊢ ((𝑦 ∈ {𝑦} ∧ {𝑦} ∈ 𝑆) → 𝑦 ∈ ∪ 𝑆) |
| 36 | 21, 34, 35 | syl2anc 584 |
. . . . 5
⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ ∪ 𝑆) |
| 37 | 36 | rgen 3063 |
. . . 4
⊢
∀𝑦 ∈
𝐴 𝑦 ∈ ∪ 𝑆 |
| 38 | | dfss3 3972 |
. . . 4
⊢ (𝐴 ⊆ ∪ 𝑆
↔ ∀𝑦 ∈
𝐴 𝑦 ∈ ∪ 𝑆) |
| 39 | 37, 38 | mpbir 231 |
. . 3
⊢ 𝐴 ⊆ ∪ 𝑆 |
| 40 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)} ⊆ 𝒫 𝐴 |
| 41 | 1, 40 | eqsstri 4030 |
. . . . 5
⊢ 𝑆 ⊆ 𝒫 𝐴 |
| 42 | 41 | unissi 4916 |
. . . 4
⊢ ∪ 𝑆
⊆ ∪ 𝒫 𝐴 |
| 43 | | unipw 5455 |
. . . 4
⊢ ∪ 𝒫 𝐴 = 𝐴 |
| 44 | 42, 43 | sseqtri 4032 |
. . 3
⊢ ∪ 𝑆
⊆ 𝐴 |
| 45 | 39, 44 | eqssi 4000 |
. 2
⊢ 𝐴 = ∪
𝑆 |
| 46 | | difssd 4137 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∖ 𝑥) ⊆ 𝐴) |
| 47 | 2, 46 | ssexd 5324 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∖ 𝑥) ∈ V) |
| 48 | | elpwg 4603 |
. . . . . . . 8
⊢ ((𝐴 ∖ 𝑥) ∈ V → ((𝐴 ∖ 𝑥) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ 𝑥) ⊆ 𝐴)) |
| 49 | 47, 48 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 ∖ 𝑥) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ 𝑥) ⊆ 𝐴)) |
| 50 | 46, 49 | mpbird 257 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∖ 𝑥) ∈ 𝒫 𝐴) |
| 51 | 50 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ 𝑥) ∈ 𝒫 𝐴) |
| 52 | 41 | sseli 3979 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ 𝒫 𝐴) |
| 53 | | elpwi 4607 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴) |
| 54 | 52, 53 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 → 𝑥 ⊆ 𝐴) |
| 55 | | dfss4 4269 |
. . . . . . . . 9
⊢ (𝑥 ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ 𝑥)) = 𝑥) |
| 56 | 54, 55 | sylib 218 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑆 → (𝐴 ∖ (𝐴 ∖ 𝑥)) = 𝑥) |
| 57 | 56 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ (𝐴 ∖ 𝑥)) = 𝑥) |
| 58 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 ≼ ω) → 𝑥 ≼ ω) |
| 59 | 57, 58 | eqbrtrd 5165 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω) |
| 60 | | olc 869 |
. . . . . 6
⊢ ((𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω → ((𝐴 ∖ 𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω)) |
| 61 | 59, 60 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 ≼ ω) → ((𝐴 ∖ 𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω)) |
| 62 | 51, 61 | jca 511 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 ≼ ω) → ((𝐴 ∖ 𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω))) |
| 63 | | breq1 5146 |
. . . . . 6
⊢ (𝑦 = (𝐴 ∖ 𝑥) → (𝑦 ≼ ω ↔ (𝐴 ∖ 𝑥) ≼ ω)) |
| 64 | | difeq2 4120 |
. . . . . . 7
⊢ (𝑦 = (𝐴 ∖ 𝑥) → (𝐴 ∖ 𝑦) = (𝐴 ∖ (𝐴 ∖ 𝑥))) |
| 65 | 64 | breq1d 5153 |
. . . . . 6
⊢ (𝑦 = (𝐴 ∖ 𝑥) → ((𝐴 ∖ 𝑦) ≼ ω ↔ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω)) |
| 66 | 63, 65 | orbi12d 919 |
. . . . 5
⊢ (𝑦 = (𝐴 ∖ 𝑥) → ((𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω) ↔ ((𝐴 ∖ 𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω))) |
| 67 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 ≼ ω ↔ 𝑦 ≼ ω)) |
| 68 | | difeq2 4120 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝑦)) |
| 69 | 68 | breq1d 5153 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝐴 ∖ 𝑥) ≼ ω ↔ (𝐴 ∖ 𝑦) ≼ ω)) |
| 70 | 67, 69 | orbi12d 919 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω) ↔ (𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω))) |
| 71 | 70 | cbvrabv 3447 |
. . . . . 6
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)} = {𝑦 ∈ 𝒫 𝐴 ∣ (𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω)} |
| 72 | 1, 71 | eqtri 2765 |
. . . . 5
⊢ 𝑆 = {𝑦 ∈ 𝒫 𝐴 ∣ (𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω)} |
| 73 | 66, 72 | elrab2 3695 |
. . . 4
⊢ ((𝐴 ∖ 𝑥) ∈ 𝑆 ↔ ((𝐴 ∖ 𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω))) |
| 74 | 62, 73 | sylibr 234 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ 𝑥) ∈ 𝑆) |
| 75 | 50 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴 ∖ 𝑥) ∈ 𝒫 𝐴) |
| 76 | 1 | reqabi 3460 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑆 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω))) |
| 77 | 76 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑆 → (𝑥 ∈ 𝒫 𝐴 ∧ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω))) |
| 78 | 77 | simprd 495 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 → (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)) |
| 79 | 78 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)) |
| 80 | 79 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)) |
| 81 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ ¬ 𝑥 ≼ ω) → ¬ 𝑥 ≼
ω) |
| 82 | | pm2.53 852 |
. . . . . . 7
⊢ ((𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω) → (¬ 𝑥 ≼ ω → (𝐴 ∖ 𝑥) ≼ ω)) |
| 83 | 80, 81, 82 | sylc 65 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴 ∖ 𝑥) ≼ ω) |
| 84 | | orc 868 |
. . . . . 6
⊢ ((𝐴 ∖ 𝑥) ≼ ω → ((𝐴 ∖ 𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω)) |
| 85 | 83, 84 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ ¬ 𝑥 ≼ ω) → ((𝐴 ∖ 𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω)) |
| 86 | 75, 85 | jca 511 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ ¬ 𝑥 ≼ ω) → ((𝐴 ∖ 𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω))) |
| 87 | 86, 73 | sylibr 234 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴 ∖ 𝑥) ∈ 𝑆) |
| 88 | 74, 87 | pm2.61dan 813 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐴 ∖ 𝑥) ∈ 𝑆) |
| 89 | | elpwi 4607 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝒫 𝑆 → 𝑥 ⊆ 𝑆) |
| 90 | 89 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥) → 𝑥 ⊆ 𝑆) |
| 91 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) |
| 92 | 90, 91 | sseldd 3984 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑆) |
| 93 | 41 | sseli 3979 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑆 → 𝑦 ∈ 𝒫 𝐴) |
| 94 | | elpwi 4607 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝒫 𝐴 → 𝑦 ⊆ 𝐴) |
| 95 | 93, 94 | syl 17 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑆 → 𝑦 ⊆ 𝐴) |
| 96 | 92, 95 | syl 17 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥) → 𝑦 ⊆ 𝐴) |
| 97 | 96 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 𝑆 → ∀𝑦 ∈ 𝑥 𝑦 ⊆ 𝐴) |
| 98 | | unissb 4939 |
. . . . . . . 8
⊢ (∪ 𝑥
⊆ 𝐴 ↔
∀𝑦 ∈ 𝑥 𝑦 ⊆ 𝐴) |
| 99 | 97, 98 | sylibr 234 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝑆 → ∪ 𝑥
⊆ 𝐴) |
| 100 | | vuniex 7759 |
. . . . . . . 8
⊢ ∪ 𝑥
∈ V |
| 101 | 100 | elpw 4604 |
. . . . . . 7
⊢ (∪ 𝑥
∈ 𝒫 𝐴 ↔
∪ 𝑥 ⊆ 𝐴) |
| 102 | 99, 101 | sylibr 234 |
. . . . . 6
⊢ (𝑥 ∈ 𝒫 𝑆 → ∪ 𝑥
∈ 𝒫 𝐴) |
| 103 | 102 | adantr 480 |
. . . . 5
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω) → ∪ 𝑥
∈ 𝒫 𝐴) |
| 104 | | id 22 |
. . . . . . . 8
⊢ ((𝑥 ≼ ω ∧
∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → (𝑥 ≼ ω ∧ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω)) |
| 105 | 104 | adantll 714 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω) ∧ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → (𝑥 ≼ ω ∧ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω)) |
| 106 | | unictb 10615 |
. . . . . . 7
⊢ ((𝑥 ≼ ω ∧
∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → ∪ 𝑥
≼ ω) |
| 107 | | orc 868 |
. . . . . . 7
⊢ (∪ 𝑥
≼ ω → (∪ 𝑥 ≼ ω ∨ (𝐴 ∖ ∪ 𝑥) ≼
ω)) |
| 108 | 105, 106,
107 | 3syl 18 |
. . . . . 6
⊢ (((𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω) ∧ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → (∪ 𝑥
≼ ω ∨ (𝐴
∖ ∪ 𝑥) ≼ ω)) |
| 109 | | rexnal 3100 |
. . . . . . . . . . . 12
⊢
(∃𝑦 ∈
𝑥 ¬ 𝑦 ≼ ω ↔ ¬ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) |
| 110 | 109 | bicomi 224 |
. . . . . . . . . . 11
⊢ (¬
∀𝑦 ∈ 𝑥 𝑦 ≼ ω ↔ ∃𝑦 ∈ 𝑥 ¬ 𝑦 ≼ ω) |
| 111 | 110 | biimpi 216 |
. . . . . . . . . 10
⊢ (¬
∀𝑦 ∈ 𝑥 𝑦 ≼ ω → ∃𝑦 ∈ 𝑥 ¬ 𝑦 ≼ ω) |
| 112 | 111 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → ∃𝑦 ∈ 𝑥 ¬ 𝑦 ≼ ω) |
| 113 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑥 ∈ 𝒫 𝑆 |
| 114 | | nfra1 3284 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦∀𝑦 ∈ 𝑥 𝑦 ≼ ω |
| 115 | 114 | nfn 1857 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 ¬
∀𝑦 ∈ 𝑥 𝑦 ≼ ω |
| 116 | 113, 115 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) |
| 117 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝐴 ∖ ∪ 𝑥)
≼ ω |
| 118 | | elssuni 4937 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝑥 → 𝑦 ⊆ ∪ 𝑥) |
| 119 | 118 | 3ad2ant2 1135 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω) → 𝑦 ⊆ ∪ 𝑥) |
| 120 | 119 | sscond 4146 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴 ∖ ∪ 𝑥) ⊆ (𝐴 ∖ 𝑦)) |
| 121 | 92 | 3adant3 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω) → 𝑦 ∈ 𝑆) |
| 122 | | simp3 1139 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω) → ¬ 𝑦 ≼
ω) |
| 123 | 72 | reqabi 3460 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ 𝒫 𝐴 ∧ (𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω))) |
| 124 | 123 | biimpi 216 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑆 → (𝑦 ∈ 𝒫 𝐴 ∧ (𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω))) |
| 125 | 124 | simprd 495 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝑆 → (𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω)) |
| 126 | 125 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ≼ ω) → (𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω)) |
| 127 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ≼ ω) → ¬ 𝑦 ≼
ω) |
| 128 | | pm2.53 852 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω) → (¬ 𝑦 ≼ ω → (𝐴 ∖ 𝑦) ≼ ω)) |
| 129 | 126, 127,
128 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ≼ ω) → (𝐴 ∖ 𝑦) ≼ ω) |
| 130 | 121, 122,
129 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴 ∖ 𝑦) ≼ ω) |
| 131 | | ssct 9091 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∖ ∪ 𝑥)
⊆ (𝐴 ∖ 𝑦) ∧ (𝐴 ∖ 𝑦) ≼ ω) → (𝐴 ∖ ∪ 𝑥) ≼
ω) |
| 132 | 120, 130,
131 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴 ∖ ∪ 𝑥) ≼
ω) |
| 133 | 132 | 3exp 1120 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝑆 → (𝑦 ∈ 𝑥 → (¬ 𝑦 ≼ ω → (𝐴 ∖ ∪ 𝑥) ≼
ω))) |
| 134 | 133 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → (𝑦 ∈ 𝑥 → (¬ 𝑦 ≼ ω → (𝐴 ∖ ∪ 𝑥) ≼
ω))) |
| 135 | 116, 117,
134 | rexlimd 3266 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → (∃𝑦 ∈ 𝑥 ¬ 𝑦 ≼ ω → (𝐴 ∖ ∪ 𝑥) ≼
ω)) |
| 136 | 112, 135 | mpd 15 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → (𝐴 ∖ ∪ 𝑥) ≼
ω) |
| 137 | | olc 869 |
. . . . . . . 8
⊢ ((𝐴 ∖ ∪ 𝑥)
≼ ω → (∪ 𝑥 ≼ ω ∨ (𝐴 ∖ ∪ 𝑥) ≼
ω)) |
| 138 | 136, 137 | syl 17 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → (∪ 𝑥
≼ ω ∨ (𝐴
∖ ∪ 𝑥) ≼ ω)) |
| 139 | 138 | adantlr 715 |
. . . . . 6
⊢ (((𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω) ∧ ¬ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → (∪ 𝑥
≼ ω ∨ (𝐴
∖ ∪ 𝑥) ≼ ω)) |
| 140 | 108, 139 | pm2.61dan 813 |
. . . . 5
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω) → (∪ 𝑥
≼ ω ∨ (𝐴
∖ ∪ 𝑥) ≼ ω)) |
| 141 | 103, 140 | jca 511 |
. . . 4
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω) → (∪ 𝑥
∈ 𝒫 𝐴 ∧
(∪ 𝑥 ≼ ω ∨ (𝐴 ∖ ∪ 𝑥) ≼
ω))) |
| 142 | | breq1 5146 |
. . . . . 6
⊢ (𝑦 = ∪
𝑥 → (𝑦 ≼ ω ↔ ∪ 𝑥
≼ ω)) |
| 143 | | difeq2 4120 |
. . . . . . 7
⊢ (𝑦 = ∪
𝑥 → (𝐴 ∖ 𝑦) = (𝐴 ∖ ∪ 𝑥)) |
| 144 | 143 | breq1d 5153 |
. . . . . 6
⊢ (𝑦 = ∪
𝑥 → ((𝐴 ∖ 𝑦) ≼ ω ↔ (𝐴 ∖ ∪ 𝑥) ≼
ω)) |
| 145 | 142, 144 | orbi12d 919 |
. . . . 5
⊢ (𝑦 = ∪
𝑥 → ((𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω) ↔ (∪ 𝑥
≼ ω ∨ (𝐴
∖ ∪ 𝑥) ≼ ω))) |
| 146 | 145, 72 | elrab2 3695 |
. . . 4
⊢ (∪ 𝑥
∈ 𝑆 ↔ (∪ 𝑥
∈ 𝒫 𝐴 ∧
(∪ 𝑥 ≼ ω ∨ (𝐴 ∖ ∪ 𝑥) ≼
ω))) |
| 147 | 141, 146 | sylibr 234 |
. . 3
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω) → ∪ 𝑥
∈ 𝑆) |
| 148 | 147 | 3adant1 1131 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω) → ∪ 𝑥
∈ 𝑆) |
| 149 | 6, 20, 45, 88, 148 | issald 46348 |
1
⊢ (𝜑 → 𝑆 ∈ SAlg) |