Step | Hyp | Ref
| Expression |
1 | | salexct.b |
. . 3
⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)} |
2 | | salexct.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | | pwexg 4776 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (𝜑 → 𝒫 𝐴 ∈ V) |
5 | | rabexg 4739 |
. . . 4
⊢
(𝒫 𝐴 ∈
V → {𝑥 ∈
𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)} ∈
V) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)} ∈
V) |
7 | 1, 6 | syl5eqel 2692 |
. 2
⊢ (𝜑 → 𝑆 ∈ V) |
8 | | 0elpw 4760 |
. . . . 5
⊢ ∅
∈ 𝒫 𝐴 |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝜑 → ∅ ∈ 𝒫
𝐴) |
10 | | 0fin 8073 |
. . . . . . 7
⊢ ∅
∈ Fin |
11 | | fict 8433 |
. . . . . . 7
⊢ (∅
∈ Fin → ∅ ≼ ω) |
12 | 10, 11 | ax-mp 5 |
. . . . . 6
⊢ ∅
≼ ω |
13 | 12 | orci 404 |
. . . . 5
⊢ (∅
≼ ω ∨ (𝐴
∖ ∅) ≼ ω) |
14 | 13 | a1i 11 |
. . . 4
⊢ (𝜑 → (∅ ≼ ω
∨ (𝐴 ∖ ∅)
≼ ω)) |
15 | 9, 14 | jca 553 |
. . 3
⊢ (𝜑 → (∅ ∈ 𝒫
𝐴 ∧ (∅ ≼
ω ∨ (𝐴 ∖
∅) ≼ ω))) |
16 | | breq1 4586 |
. . . . 5
⊢ (𝑥 = ∅ → (𝑥 ≼ ω ↔ ∅
≼ ω)) |
17 | | difeq2 3684 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐴 ∖ 𝑥) = (𝐴 ∖ ∅)) |
18 | 17 | breq1d 4593 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝐴 ∖ 𝑥) ≼ ω ↔ (𝐴 ∖ ∅) ≼
ω)) |
19 | 16, 18 | orbi12d 742 |
. . . 4
⊢ (𝑥 = ∅ → ((𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω) ↔ (∅ ≼
ω ∨ (𝐴 ∖
∅) ≼ ω))) |
20 | 19, 1 | elrab2 3333 |
. . 3
⊢ (∅
∈ 𝑆 ↔ (∅
∈ 𝒫 𝐴 ∧
(∅ ≼ ω ∨ (𝐴 ∖ ∅) ≼
ω))) |
21 | 15, 20 | sylibr 223 |
. 2
⊢ (𝜑 → ∅ ∈ 𝑆) |
22 | | snidg 4153 |
. . . . . 6
⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ {𝑦}) |
23 | | snelpwi 4839 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝒫 𝐴) |
24 | | snfi 7923 |
. . . . . . . . . . 11
⊢ {𝑦} ∈ Fin |
25 | | fict 8433 |
. . . . . . . . . . 11
⊢ ({𝑦} ∈ Fin → {𝑦} ≼
ω) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . 10
⊢ {𝑦} ≼
ω |
27 | 26 | orci 404 |
. . . . . . . . 9
⊢ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω) |
28 | 27 | a1i 11 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω)) |
29 | 23, 28 | jca 553 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 → ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))) |
30 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑥 = {𝑦} → (𝑥 ≼ ω ↔ {𝑦} ≼ ω)) |
31 | | difeq2 3684 |
. . . . . . . . . 10
⊢ (𝑥 = {𝑦} → (𝐴 ∖ 𝑥) = (𝐴 ∖ {𝑦})) |
32 | 31 | breq1d 4593 |
. . . . . . . . 9
⊢ (𝑥 = {𝑦} → ((𝐴 ∖ 𝑥) ≼ ω ↔ (𝐴 ∖ {𝑦}) ≼ ω)) |
33 | 30, 32 | orbi12d 742 |
. . . . . . . 8
⊢ (𝑥 = {𝑦} → ((𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω) ↔ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))) |
34 | 33, 1 | elrab2 3333 |
. . . . . . 7
⊢ ({𝑦} ∈ 𝑆 ↔ ({𝑦} ∈ 𝒫 𝐴 ∧ ({𝑦} ≼ ω ∨ (𝐴 ∖ {𝑦}) ≼ ω))) |
35 | 29, 34 | sylibr 223 |
. . . . . 6
⊢ (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝑆) |
36 | | elunii 4377 |
. . . . . 6
⊢ ((𝑦 ∈ {𝑦} ∧ {𝑦} ∈ 𝑆) → 𝑦 ∈ ∪ 𝑆) |
37 | 22, 35, 36 | syl2anc 691 |
. . . . 5
⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ ∪ 𝑆) |
38 | 37 | rgen 2906 |
. . . 4
⊢
∀𝑦 ∈
𝐴 𝑦 ∈ ∪ 𝑆 |
39 | | dfss3 3558 |
. . . 4
⊢ (𝐴 ⊆ ∪ 𝑆
↔ ∀𝑦 ∈
𝐴 𝑦 ∈ ∪ 𝑆) |
40 | 38, 39 | mpbir 220 |
. . 3
⊢ 𝐴 ⊆ ∪ 𝑆 |
41 | | ssrab2 3650 |
. . . . . 6
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)} ⊆ 𝒫 𝐴 |
42 | 1, 41 | eqsstri 3598 |
. . . . 5
⊢ 𝑆 ⊆ 𝒫 𝐴 |
43 | 42 | unissi 4397 |
. . . 4
⊢ ∪ 𝑆
⊆ ∪ 𝒫 𝐴 |
44 | | unipw 4845 |
. . . 4
⊢ ∪ 𝒫 𝐴 = 𝐴 |
45 | 43, 44 | sseqtri 3600 |
. . 3
⊢ ∪ 𝑆
⊆ 𝐴 |
46 | 40, 45 | eqssi 3584 |
. 2
⊢ 𝐴 = ∪
𝑆 |
47 | | difssd 3700 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∖ 𝑥) ⊆ 𝐴) |
48 | 2, 47 | ssexd 4733 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∖ 𝑥) ∈ V) |
49 | | elpwg 4116 |
. . . . . . . 8
⊢ ((𝐴 ∖ 𝑥) ∈ V → ((𝐴 ∖ 𝑥) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ 𝑥) ⊆ 𝐴)) |
50 | 48, 49 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 ∖ 𝑥) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ 𝑥) ⊆ 𝐴)) |
51 | 47, 50 | mpbird 246 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∖ 𝑥) ∈ 𝒫 𝐴) |
52 | 51 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ 𝑥) ∈ 𝒫 𝐴) |
53 | 42 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ 𝒫 𝐴) |
54 | | elpwi 4117 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴) |
55 | 53, 54 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 → 𝑥 ⊆ 𝐴) |
56 | | dfss4 3820 |
. . . . . . . . 9
⊢ (𝑥 ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ 𝑥)) = 𝑥) |
57 | 55, 56 | sylib 207 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑆 → (𝐴 ∖ (𝐴 ∖ 𝑥)) = 𝑥) |
58 | 57 | ad2antlr 759 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ (𝐴 ∖ 𝑥)) = 𝑥) |
59 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 ≼ ω) → 𝑥 ≼ ω) |
60 | 58, 59 | eqbrtrd 4605 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω) |
61 | | olc 398 |
. . . . . 6
⊢ ((𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω → ((𝐴 ∖ 𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω)) |
62 | 60, 61 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 ≼ ω) → ((𝐴 ∖ 𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω)) |
63 | 52, 62 | jca 553 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 ≼ ω) → ((𝐴 ∖ 𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω))) |
64 | | breq1 4586 |
. . . . . 6
⊢ (𝑦 = (𝐴 ∖ 𝑥) → (𝑦 ≼ ω ↔ (𝐴 ∖ 𝑥) ≼ ω)) |
65 | | difeq2 3684 |
. . . . . . 7
⊢ (𝑦 = (𝐴 ∖ 𝑥) → (𝐴 ∖ 𝑦) = (𝐴 ∖ (𝐴 ∖ 𝑥))) |
66 | 65 | breq1d 4593 |
. . . . . 6
⊢ (𝑦 = (𝐴 ∖ 𝑥) → ((𝐴 ∖ 𝑦) ≼ ω ↔ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω)) |
67 | 64, 66 | orbi12d 742 |
. . . . 5
⊢ (𝑦 = (𝐴 ∖ 𝑥) → ((𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω) ↔ ((𝐴 ∖ 𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω))) |
68 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 ≼ ω ↔ 𝑦 ≼ ω)) |
69 | | difeq2 3684 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝑦)) |
70 | 69 | breq1d 4593 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝐴 ∖ 𝑥) ≼ ω ↔ (𝐴 ∖ 𝑦) ≼ ω)) |
71 | 68, 70 | orbi12d 742 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω) ↔ (𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω))) |
72 | 71 | cbvrabv 3172 |
. . . . . 6
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)} = {𝑦 ∈ 𝒫 𝐴 ∣ (𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω)} |
73 | 1, 72 | eqtri 2632 |
. . . . 5
⊢ 𝑆 = {𝑦 ∈ 𝒫 𝐴 ∣ (𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω)} |
74 | 67, 73 | elrab2 3333 |
. . . 4
⊢ ((𝐴 ∖ 𝑥) ∈ 𝑆 ↔ ((𝐴 ∖ 𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω))) |
75 | 63, 74 | sylibr 223 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 ≼ ω) → (𝐴 ∖ 𝑥) ∈ 𝑆) |
76 | 51 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴 ∖ 𝑥) ∈ 𝒫 𝐴) |
77 | 1 | rabeq2i 3170 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑆 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω))) |
78 | 77 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑆 → (𝑥 ∈ 𝒫 𝐴 ∧ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω))) |
79 | 78 | simprd 478 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 → (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)) |
80 | 79 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)) |
81 | 80 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)) |
82 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ ¬ 𝑥 ≼ ω) → ¬ 𝑥 ≼
ω) |
83 | | pm2.53 387 |
. . . . . . 7
⊢ ((𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω) → (¬ 𝑥 ≼ ω → (𝐴 ∖ 𝑥) ≼ ω)) |
84 | 81, 82, 83 | sylc 63 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴 ∖ 𝑥) ≼ ω) |
85 | | orc 399 |
. . . . . 6
⊢ ((𝐴 ∖ 𝑥) ≼ ω → ((𝐴 ∖ 𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω)) |
86 | 84, 85 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ ¬ 𝑥 ≼ ω) → ((𝐴 ∖ 𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω)) |
87 | 76, 86 | jca 553 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ ¬ 𝑥 ≼ ω) → ((𝐴 ∖ 𝑥) ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑥) ≼ ω ∨ (𝐴 ∖ (𝐴 ∖ 𝑥)) ≼ ω))) |
88 | 87, 74 | sylibr 223 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ ¬ 𝑥 ≼ ω) → (𝐴 ∖ 𝑥) ∈ 𝑆) |
89 | 75, 88 | pm2.61dan 828 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐴 ∖ 𝑥) ∈ 𝑆) |
90 | | elpwi 4117 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝒫 𝑆 → 𝑥 ⊆ 𝑆) |
91 | 90 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥) → 𝑥 ⊆ 𝑆) |
92 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) |
93 | 91, 92 | sseldd 3569 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑆) |
94 | 42 | sseli 3564 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑆 → 𝑦 ∈ 𝒫 𝐴) |
95 | | elpwi 4117 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝒫 𝐴 → 𝑦 ⊆ 𝐴) |
96 | 94, 95 | syl 17 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑆 → 𝑦 ⊆ 𝐴) |
97 | 93, 96 | syl 17 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥) → 𝑦 ⊆ 𝐴) |
98 | 97 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 𝑆 → ∀𝑦 ∈ 𝑥 𝑦 ⊆ 𝐴) |
99 | | unissb 4405 |
. . . . . . . 8
⊢ (∪ 𝑥
⊆ 𝐴 ↔
∀𝑦 ∈ 𝑥 𝑦 ⊆ 𝐴) |
100 | 98, 99 | sylibr 223 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝑆 → ∪ 𝑥
⊆ 𝐴) |
101 | | vuniex 6852 |
. . . . . . . 8
⊢ ∪ 𝑥
∈ V |
102 | 101 | elpw 4114 |
. . . . . . 7
⊢ (∪ 𝑥
∈ 𝒫 𝐴 ↔
∪ 𝑥 ⊆ 𝐴) |
103 | 100, 102 | sylibr 223 |
. . . . . 6
⊢ (𝑥 ∈ 𝒫 𝑆 → ∪ 𝑥
∈ 𝒫 𝐴) |
104 | 103 | adantr 480 |
. . . . 5
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω) → ∪ 𝑥
∈ 𝒫 𝐴) |
105 | | id 22 |
. . . . . . . 8
⊢ ((𝑥 ≼ ω ∧
∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → (𝑥 ≼ ω ∧ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω)) |
106 | 105 | adantll 746 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω) ∧ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → (𝑥 ≼ ω ∧ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω)) |
107 | | unictb 9276 |
. . . . . . 7
⊢ ((𝑥 ≼ ω ∧
∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → ∪ 𝑥
≼ ω) |
108 | | orc 399 |
. . . . . . 7
⊢ (∪ 𝑥
≼ ω → (∪ 𝑥 ≼ ω ∨ (𝐴 ∖ ∪ 𝑥) ≼
ω)) |
109 | 106, 107,
108 | 3syl 18 |
. . . . . 6
⊢ (((𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω) ∧ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → (∪ 𝑥
≼ ω ∨ (𝐴
∖ ∪ 𝑥) ≼ ω)) |
110 | | rexnal 2978 |
. . . . . . . . . . . 12
⊢
(∃𝑦 ∈
𝑥 ¬ 𝑦 ≼ ω ↔ ¬ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) |
111 | 110 | bicomi 213 |
. . . . . . . . . . 11
⊢ (¬
∀𝑦 ∈ 𝑥 𝑦 ≼ ω ↔ ∃𝑦 ∈ 𝑥 ¬ 𝑦 ≼ ω) |
112 | 111 | biimpi 205 |
. . . . . . . . . 10
⊢ (¬
∀𝑦 ∈ 𝑥 𝑦 ≼ ω → ∃𝑦 ∈ 𝑥 ¬ 𝑦 ≼ ω) |
113 | 112 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → ∃𝑦 ∈ 𝑥 ¬ 𝑦 ≼ ω) |
114 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑥 ∈ 𝒫 𝑆 |
115 | | nfra1 2925 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦∀𝑦 ∈ 𝑥 𝑦 ≼ ω |
116 | 115 | nfn 1768 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 ¬
∀𝑦 ∈ 𝑥 𝑦 ≼ ω |
117 | 114, 116 | nfan 1816 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) |
118 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝐴 ∖ ∪ 𝑥)
≼ ω |
119 | | elssuni 4403 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝑥 → 𝑦 ⊆ ∪ 𝑥) |
120 | 119 | 3ad2ant2 1076 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω) → 𝑦 ⊆ ∪ 𝑥) |
121 | 120 | sscond 3709 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴 ∖ ∪ 𝑥) ⊆ (𝐴 ∖ 𝑦)) |
122 | 93 | 3adant3 1074 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω) → 𝑦 ∈ 𝑆) |
123 | | simp3 1056 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω) → ¬ 𝑦 ≼
ω) |
124 | 73 | rabeq2i 3170 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ 𝒫 𝐴 ∧ (𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω))) |
125 | 124 | biimpi 205 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑆 → (𝑦 ∈ 𝒫 𝐴 ∧ (𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω))) |
126 | 125 | simprd 478 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝑆 → (𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω)) |
127 | 126 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ≼ ω) → (𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω)) |
128 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ≼ ω) → ¬ 𝑦 ≼
ω) |
129 | | pm2.53 387 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω) → (¬ 𝑦 ≼ ω → (𝐴 ∖ 𝑦) ≼ ω)) |
130 | 127, 128,
129 | sylc 63 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ≼ ω) → (𝐴 ∖ 𝑦) ≼ ω) |
131 | 122, 123,
130 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴 ∖ 𝑦) ≼ ω) |
132 | | ssct 7926 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∖ ∪ 𝑥)
⊆ (𝐴 ∖ 𝑦) ∧ (𝐴 ∖ 𝑦) ≼ ω) → (𝐴 ∖ ∪ 𝑥) ≼
ω) |
133 | 121, 131,
132 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ≼ ω) → (𝐴 ∖ ∪ 𝑥) ≼
ω) |
134 | 133 | 3exp 1256 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝑆 → (𝑦 ∈ 𝑥 → (¬ 𝑦 ≼ ω → (𝐴 ∖ ∪ 𝑥) ≼
ω))) |
135 | 134 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → (𝑦 ∈ 𝑥 → (¬ 𝑦 ≼ ω → (𝐴 ∖ ∪ 𝑥) ≼
ω))) |
136 | 117, 118,
135 | rexlimd 3008 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → (∃𝑦 ∈ 𝑥 ¬ 𝑦 ≼ ω → (𝐴 ∖ ∪ 𝑥) ≼
ω)) |
137 | 113, 136 | mpd 15 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → (𝐴 ∖ ∪ 𝑥) ≼
ω) |
138 | | olc 398 |
. . . . . . . 8
⊢ ((𝐴 ∖ ∪ 𝑥)
≼ ω → (∪ 𝑥 ≼ ω ∨ (𝐴 ∖ ∪ 𝑥) ≼
ω)) |
139 | 137, 138 | syl 17 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ ¬ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → (∪ 𝑥
≼ ω ∨ (𝐴
∖ ∪ 𝑥) ≼ ω)) |
140 | 139 | adantlr 747 |
. . . . . 6
⊢ (((𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω) ∧ ¬ ∀𝑦 ∈ 𝑥 𝑦 ≼ ω) → (∪ 𝑥
≼ ω ∨ (𝐴
∖ ∪ 𝑥) ≼ ω)) |
141 | 109, 140 | pm2.61dan 828 |
. . . . 5
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω) → (∪ 𝑥
≼ ω ∨ (𝐴
∖ ∪ 𝑥) ≼ ω)) |
142 | 104, 141 | jca 553 |
. . . 4
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω) → (∪ 𝑥
∈ 𝒫 𝐴 ∧
(∪ 𝑥 ≼ ω ∨ (𝐴 ∖ ∪ 𝑥) ≼
ω))) |
143 | | breq1 4586 |
. . . . . 6
⊢ (𝑦 = ∪
𝑥 → (𝑦 ≼ ω ↔ ∪ 𝑥
≼ ω)) |
144 | | difeq2 3684 |
. . . . . . 7
⊢ (𝑦 = ∪
𝑥 → (𝐴 ∖ 𝑦) = (𝐴 ∖ ∪ 𝑥)) |
145 | 144 | breq1d 4593 |
. . . . . 6
⊢ (𝑦 = ∪
𝑥 → ((𝐴 ∖ 𝑦) ≼ ω ↔ (𝐴 ∖ ∪ 𝑥) ≼
ω)) |
146 | 143, 145 | orbi12d 742 |
. . . . 5
⊢ (𝑦 = ∪
𝑥 → ((𝑦 ≼ ω ∨ (𝐴 ∖ 𝑦) ≼ ω) ↔ (∪ 𝑥
≼ ω ∨ (𝐴
∖ ∪ 𝑥) ≼ ω))) |
147 | 146, 73 | elrab2 3333 |
. . . 4
⊢ (∪ 𝑥
∈ 𝑆 ↔ (∪ 𝑥
∈ 𝒫 𝐴 ∧
(∪ 𝑥 ≼ ω ∨ (𝐴 ∖ ∪ 𝑥) ≼
ω))) |
148 | 142, 147 | sylibr 223 |
. . 3
⊢ ((𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω) → ∪ 𝑥
∈ 𝑆) |
149 | 148 | 3adant1 1072 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝑆 ∧ 𝑥 ≼ ω) → ∪ 𝑥
∈ 𝑆) |
150 | 7, 21, 46, 89, 149 | issald 39227 |
1
⊢ (𝜑 → 𝑆 ∈ SAlg) |