Step | Hyp | Ref
| Expression |
1 | | elun1 3294 |
. . . . 5
⊢ (𝑁 ∈ ω → 𝑁 ∈ (ω ∪
{ω})) |
2 | 1 | adantr 274 |
. . . 4
⊢ ((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) → 𝑁 ∈ (ω ∪
{ω})) |
3 | | endom 6738 |
. . . . 5
⊢ (𝑁 ≈ 𝐴 → 𝑁 ≼ 𝐴) |
4 | 3 | adantl 275 |
. . . 4
⊢ ((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) → 𝑁 ≼ 𝐴) |
5 | | breq1 3990 |
. . . . 5
⊢ (𝑦 = 𝑁 → (𝑦 ≼ 𝐴 ↔ 𝑁 ≼ 𝐴)) |
6 | 5 | elrab 2886 |
. . . 4
⊢ (𝑁 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴} ↔ (𝑁 ∈ (ω ∪ {ω}) ∧
𝑁 ≼ 𝐴)) |
7 | 2, 4, 6 | sylanbrc 415 |
. . 3
⊢ ((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) → 𝑁 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) |
8 | | breq1 3990 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝑦 ≼ 𝐴 ↔ 𝑧 ≼ 𝐴)) |
9 | 8 | elrab 2886 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴} ↔ (𝑧 ∈ (ω ∪ {ω}) ∧ 𝑧 ≼ 𝐴)) |
10 | 9 | biimpi 119 |
. . . . . . . . . 10
⊢ (𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴} → (𝑧 ∈ (ω ∪ {ω}) ∧ 𝑧 ≼ 𝐴)) |
11 | 10 | adantl 275 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) → (𝑧 ∈ (ω ∪ {ω}) ∧ 𝑧 ≼ 𝐴)) |
12 | 11 | simprd 113 |
. . . . . . . 8
⊢ (((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) → 𝑧 ≼ 𝐴) |
13 | | simplr 525 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) → 𝑁 ≈ 𝐴) |
14 | 13 | ensymd 6758 |
. . . . . . . 8
⊢ (((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) → 𝐴 ≈ 𝑁) |
15 | | domentr 6766 |
. . . . . . . 8
⊢ ((𝑧 ≼ 𝐴 ∧ 𝐴 ≈ 𝑁) → 𝑧 ≼ 𝑁) |
16 | 12, 14, 15 | syl2anc 409 |
. . . . . . 7
⊢ (((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) → 𝑧 ≼ 𝑁) |
17 | 16 | adantr 274 |
. . . . . 6
⊢ ((((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) ∧ 𝑧 ∈ ω) → 𝑧 ≼ 𝑁) |
18 | | simpr 109 |
. . . . . . 7
⊢ ((((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) ∧ 𝑧 ∈ ω) → 𝑧 ∈ ω) |
19 | | simplll 528 |
. . . . . . 7
⊢ ((((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) ∧ 𝑧 ∈ ω) → 𝑁 ∈ ω) |
20 | | nndomo 6839 |
. . . . . . 7
⊢ ((𝑧 ∈ ω ∧ 𝑁 ∈ ω) → (𝑧 ≼ 𝑁 ↔ 𝑧 ⊆ 𝑁)) |
21 | 18, 19, 20 | syl2anc 409 |
. . . . . 6
⊢ ((((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) ∧ 𝑧 ∈ ω) → (𝑧 ≼ 𝑁 ↔ 𝑧 ⊆ 𝑁)) |
22 | 17, 21 | mpbid 146 |
. . . . 5
⊢ ((((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) ∧ 𝑧 ∈ ω) → 𝑧 ⊆ 𝑁) |
23 | | nnfi 6847 |
. . . . . . . 8
⊢ (𝑁 ∈ ω → 𝑁 ∈ Fin) |
24 | 23 | ad3antrrr 489 |
. . . . . . 7
⊢ ((((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) ∧ 𝑧 ∈ {ω}) → 𝑁 ∈ Fin) |
25 | 14 | adantr 274 |
. . . . . . 7
⊢ ((((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) ∧ 𝑧 ∈ {ω}) → 𝐴 ≈ 𝑁) |
26 | | enfii 6849 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝐴 ≈ 𝑁) → 𝐴 ∈ Fin) |
27 | 24, 25, 26 | syl2anc 409 |
. . . . . 6
⊢ ((((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) ∧ 𝑧 ∈ {ω}) → 𝐴 ∈ Fin) |
28 | 12 | adantr 274 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) ∧ 𝑧 ∈ {ω}) → 𝑧 ≼ 𝐴) |
29 | | elsni 3599 |
. . . . . . . . . 10
⊢ (𝑧 ∈ {ω} → 𝑧 = ω) |
30 | 29 | breq1d 3997 |
. . . . . . . . 9
⊢ (𝑧 ∈ {ω} → (𝑧 ≼ 𝐴 ↔ ω ≼ 𝐴)) |
31 | 30 | adantl 275 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) ∧ 𝑧 ∈ {ω}) → (𝑧 ≼ 𝐴 ↔ ω ≼ 𝐴)) |
32 | 28, 31 | mpbid 146 |
. . . . . . 7
⊢ ((((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) ∧ 𝑧 ∈ {ω}) → ω ≼
𝐴) |
33 | | infnfi 6870 |
. . . . . . 7
⊢ (ω
≼ 𝐴 → ¬
𝐴 ∈
Fin) |
34 | 32, 33 | syl 14 |
. . . . . 6
⊢ ((((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) ∧ 𝑧 ∈ {ω}) → ¬ 𝐴 ∈ Fin) |
35 | 27, 34 | pm2.21dd 615 |
. . . . 5
⊢ ((((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) ∧ 𝑧 ∈ {ω}) → 𝑧 ⊆ 𝑁) |
36 | 11 | simpld 111 |
. . . . . 6
⊢ (((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) → 𝑧 ∈ (ω ∪
{ω})) |
37 | | elun 3268 |
. . . . . 6
⊢ (𝑧 ∈ (ω ∪
{ω}) ↔ (𝑧 ∈
ω ∨ 𝑧 ∈
{ω})) |
38 | 36, 37 | sylib 121 |
. . . . 5
⊢ (((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) → (𝑧 ∈ ω ∨ 𝑧 ∈ {ω})) |
39 | 22, 35, 38 | mpjaodan 793 |
. . . 4
⊢ (((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) ∧ 𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}) → 𝑧 ⊆ 𝑁) |
40 | 39 | ralrimiva 2543 |
. . 3
⊢ ((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) → ∀𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}𝑧 ⊆ 𝑁) |
41 | | ssunieq 3827 |
. . 3
⊢ ((𝑁 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴} ∧ ∀𝑧 ∈ {𝑦 ∈ (ω ∪ {ω}) ∣
𝑦 ≼ 𝐴}𝑧 ⊆ 𝑁) → 𝑁 = ∪ {𝑦 ∈ (ω ∪
{ω}) ∣ 𝑦
≼ 𝐴}) |
42 | 7, 40, 41 | syl2anc 409 |
. 2
⊢ ((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) → 𝑁 = ∪ {𝑦 ∈ (ω ∪
{ω}) ∣ 𝑦
≼ 𝐴}) |
43 | 42 | eqcomd 2176 |
1
⊢ ((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) → ∪ {𝑦 ∈ (ω ∪
{ω}) ∣ 𝑦
≼ 𝐴} = 𝑁) |