| Step | Hyp | Ref
| Expression |
| 1 | | isfin6 10340 |
. 2
⊢ (𝐴 ∈ FinVI ↔
(𝐴 ≺ 2o
∨ 𝐴 ≺ (𝐴 × 𝐴))) |
| 2 | | 2onn 8680 |
. . . . . 6
⊢
2o ∈ ω |
| 3 | | ssid 4006 |
. . . . . 6
⊢
2o ⊆ 2o |
| 4 | | ssnnfi 9209 |
. . . . . 6
⊢
((2o ∈ ω ∧ 2o ⊆
2o) → 2o ∈ Fin) |
| 5 | 2, 3, 4 | mp2an 692 |
. . . . 5
⊢
2o ∈ Fin |
| 6 | | sdomdom 9020 |
. . . . 5
⊢ (𝐴 ≺ 2o →
𝐴 ≼
2o) |
| 7 | | domfi 9229 |
. . . . 5
⊢
((2o ∈ Fin ∧ 𝐴 ≼ 2o) → 𝐴 ∈ Fin) |
| 8 | 5, 6, 7 | sylancr 587 |
. . . 4
⊢ (𝐴 ≺ 2o →
𝐴 ∈
Fin) |
| 9 | | fin17 10434 |
. . . 4
⊢ (𝐴 ∈ Fin → 𝐴 ∈
FinVII) |
| 10 | 8, 9 | syl 17 |
. . 3
⊢ (𝐴 ≺ 2o →
𝐴 ∈
FinVII) |
| 11 | | sdomnen 9021 |
. . . . 5
⊢ (𝐴 ≺ (𝐴 × 𝐴) → ¬ 𝐴 ≈ (𝐴 × 𝐴)) |
| 12 | | eldifi 4131 |
. . . . . . . . 9
⊢ (𝑏 ∈ (On ∖ ω)
→ 𝑏 ∈
On) |
| 13 | | ensym 9043 |
. . . . . . . . 9
⊢ (𝐴 ≈ 𝑏 → 𝑏 ≈ 𝐴) |
| 14 | | isnumi 9986 |
. . . . . . . . 9
⊢ ((𝑏 ∈ On ∧ 𝑏 ≈ 𝐴) → 𝐴 ∈ dom card) |
| 15 | 12, 13, 14 | syl2an 596 |
. . . . . . . 8
⊢ ((𝑏 ∈ (On ∖ ω)
∧ 𝐴 ≈ 𝑏) → 𝐴 ∈ dom card) |
| 16 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑏 ∈ V |
| 17 | | eldif 3961 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ (On ∖ ω)
↔ (𝑏 ∈ On ∧
¬ 𝑏 ∈
ω)) |
| 18 | | ordom 7897 |
. . . . . . . . . . . . . 14
⊢ Ord
ω |
| 19 | | eloni 6394 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ On → Ord 𝑏) |
| 20 | | ordtri1 6417 |
. . . . . . . . . . . . . 14
⊢ ((Ord
ω ∧ Ord 𝑏) →
(ω ⊆ 𝑏 ↔
¬ 𝑏 ∈
ω)) |
| 21 | 18, 19, 20 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ On → (ω
⊆ 𝑏 ↔ ¬
𝑏 ∈
ω)) |
| 22 | 21 | biimpar 477 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ On ∧ ¬ 𝑏 ∈ ω) → ω
⊆ 𝑏) |
| 23 | 17, 22 | sylbi 217 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (On ∖ ω)
→ ω ⊆ 𝑏) |
| 24 | | ssdomg 9040 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ V → (ω
⊆ 𝑏 → ω
≼ 𝑏)) |
| 25 | 16, 23, 24 | mpsyl 68 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (On ∖ ω)
→ ω ≼ 𝑏) |
| 26 | | domen2 9160 |
. . . . . . . . . 10
⊢ (𝐴 ≈ 𝑏 → (ω ≼ 𝐴 ↔ ω ≼ 𝑏)) |
| 27 | 25, 26 | imbitrrid 246 |
. . . . . . . . 9
⊢ (𝐴 ≈ 𝑏 → (𝑏 ∈ (On ∖ ω) → ω
≼ 𝐴)) |
| 28 | 27 | impcom 407 |
. . . . . . . 8
⊢ ((𝑏 ∈ (On ∖ ω)
∧ 𝐴 ≈ 𝑏) → ω ≼ 𝐴) |
| 29 | | infxpidm2 10057 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴) |
| 30 | 15, 28, 29 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑏 ∈ (On ∖ ω)
∧ 𝐴 ≈ 𝑏) → (𝐴 × 𝐴) ≈ 𝐴) |
| 31 | | ensym 9043 |
. . . . . . 7
⊢ ((𝐴 × 𝐴) ≈ 𝐴 → 𝐴 ≈ (𝐴 × 𝐴)) |
| 32 | 30, 31 | syl 17 |
. . . . . 6
⊢ ((𝑏 ∈ (On ∖ ω)
∧ 𝐴 ≈ 𝑏) → 𝐴 ≈ (𝐴 × 𝐴)) |
| 33 | 32 | rexlimiva 3147 |
. . . . 5
⊢
(∃𝑏 ∈ (On
∖ ω)𝐴 ≈
𝑏 → 𝐴 ≈ (𝐴 × 𝐴)) |
| 34 | 11, 33 | nsyl 140 |
. . . 4
⊢ (𝐴 ≺ (𝐴 × 𝐴) → ¬ ∃𝑏 ∈ (On ∖ ω)𝐴 ≈ 𝑏) |
| 35 | | relsdom 8992 |
. . . . . 6
⊢ Rel
≺ |
| 36 | 35 | brrelex1i 5741 |
. . . . 5
⊢ (𝐴 ≺ (𝐴 × 𝐴) → 𝐴 ∈ V) |
| 37 | | isfin7 10341 |
. . . . 5
⊢ (𝐴 ∈ V → (𝐴 ∈ FinVII ↔
¬ ∃𝑏 ∈ (On
∖ ω)𝐴 ≈
𝑏)) |
| 38 | 36, 37 | syl 17 |
. . . 4
⊢ (𝐴 ≺ (𝐴 × 𝐴) → (𝐴 ∈ FinVII ↔ ¬
∃𝑏 ∈ (On ∖
ω)𝐴 ≈ 𝑏)) |
| 39 | 34, 38 | mpbird 257 |
. . 3
⊢ (𝐴 ≺ (𝐴 × 𝐴) → 𝐴 ∈ FinVII) |
| 40 | 10, 39 | jaoi 858 |
. 2
⊢ ((𝐴 ≺ 2o ∨
𝐴 ≺ (𝐴 × 𝐴)) → 𝐴 ∈ FinVII) |
| 41 | 1, 40 | sylbi 217 |
1
⊢ (𝐴 ∈ FinVI →
𝐴 ∈
FinVII) |