Step | Hyp | Ref
| Expression |
1 | | isfin6 10056 |
. 2
⊢ (𝐴 ∈ FinVI ↔
(𝐴 ≺ 2o
∨ 𝐴 ≺ (𝐴 × 𝐴))) |
2 | | 2onn 8472 |
. . . . . 6
⊢
2o ∈ ω |
3 | | ssid 3943 |
. . . . . 6
⊢
2o ⊆ 2o |
4 | | ssnnfi 8952 |
. . . . . 6
⊢
((2o ∈ ω ∧ 2o ⊆
2o) → 2o ∈ Fin) |
5 | 2, 3, 4 | mp2an 689 |
. . . . 5
⊢
2o ∈ Fin |
6 | | sdomdom 8768 |
. . . . 5
⊢ (𝐴 ≺ 2o →
𝐴 ≼
2o) |
7 | | domfi 8975 |
. . . . 5
⊢
((2o ∈ Fin ∧ 𝐴 ≼ 2o) → 𝐴 ∈ Fin) |
8 | 5, 6, 7 | sylancr 587 |
. . . 4
⊢ (𝐴 ≺ 2o →
𝐴 ∈
Fin) |
9 | | fin17 10150 |
. . . 4
⊢ (𝐴 ∈ Fin → 𝐴 ∈
FinVII) |
10 | 8, 9 | syl 17 |
. . 3
⊢ (𝐴 ≺ 2o →
𝐴 ∈
FinVII) |
11 | | sdomnen 8769 |
. . . . 5
⊢ (𝐴 ≺ (𝐴 × 𝐴) → ¬ 𝐴 ≈ (𝐴 × 𝐴)) |
12 | | eldifi 4061 |
. . . . . . . . 9
⊢ (𝑏 ∈ (On ∖ ω)
→ 𝑏 ∈
On) |
13 | | ensym 8789 |
. . . . . . . . 9
⊢ (𝐴 ≈ 𝑏 → 𝑏 ≈ 𝐴) |
14 | | isnumi 9704 |
. . . . . . . . 9
⊢ ((𝑏 ∈ On ∧ 𝑏 ≈ 𝐴) → 𝐴 ∈ dom card) |
15 | 12, 13, 14 | syl2an 596 |
. . . . . . . 8
⊢ ((𝑏 ∈ (On ∖ ω)
∧ 𝐴 ≈ 𝑏) → 𝐴 ∈ dom card) |
16 | | vex 3436 |
. . . . . . . . . . 11
⊢ 𝑏 ∈ V |
17 | | eldif 3897 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ (On ∖ ω)
↔ (𝑏 ∈ On ∧
¬ 𝑏 ∈
ω)) |
18 | | ordom 7722 |
. . . . . . . . . . . . . 14
⊢ Ord
ω |
19 | | eloni 6276 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ On → Ord 𝑏) |
20 | | ordtri1 6299 |
. . . . . . . . . . . . . 14
⊢ ((Ord
ω ∧ Ord 𝑏) →
(ω ⊆ 𝑏 ↔
¬ 𝑏 ∈
ω)) |
21 | 18, 19, 20 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ On → (ω
⊆ 𝑏 ↔ ¬
𝑏 ∈
ω)) |
22 | 21 | biimpar 478 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ On ∧ ¬ 𝑏 ∈ ω) → ω
⊆ 𝑏) |
23 | 17, 22 | sylbi 216 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (On ∖ ω)
→ ω ⊆ 𝑏) |
24 | | ssdomg 8786 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ V → (ω
⊆ 𝑏 → ω
≼ 𝑏)) |
25 | 16, 23, 24 | mpsyl 68 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (On ∖ ω)
→ ω ≼ 𝑏) |
26 | | domen2 8907 |
. . . . . . . . . 10
⊢ (𝐴 ≈ 𝑏 → (ω ≼ 𝐴 ↔ ω ≼ 𝑏)) |
27 | 25, 26 | syl5ibr 245 |
. . . . . . . . 9
⊢ (𝐴 ≈ 𝑏 → (𝑏 ∈ (On ∖ ω) → ω
≼ 𝐴)) |
28 | 27 | impcom 408 |
. . . . . . . 8
⊢ ((𝑏 ∈ (On ∖ ω)
∧ 𝐴 ≈ 𝑏) → ω ≼ 𝐴) |
29 | | infxpidm2 9773 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴) |
30 | 15, 28, 29 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑏 ∈ (On ∖ ω)
∧ 𝐴 ≈ 𝑏) → (𝐴 × 𝐴) ≈ 𝐴) |
31 | | ensym 8789 |
. . . . . . 7
⊢ ((𝐴 × 𝐴) ≈ 𝐴 → 𝐴 ≈ (𝐴 × 𝐴)) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ ((𝑏 ∈ (On ∖ ω)
∧ 𝐴 ≈ 𝑏) → 𝐴 ≈ (𝐴 × 𝐴)) |
33 | 32 | rexlimiva 3210 |
. . . . 5
⊢
(∃𝑏 ∈ (On
∖ ω)𝐴 ≈
𝑏 → 𝐴 ≈ (𝐴 × 𝐴)) |
34 | 11, 33 | nsyl 140 |
. . . 4
⊢ (𝐴 ≺ (𝐴 × 𝐴) → ¬ ∃𝑏 ∈ (On ∖ ω)𝐴 ≈ 𝑏) |
35 | | relsdom 8740 |
. . . . . 6
⊢ Rel
≺ |
36 | 35 | brrelex1i 5643 |
. . . . 5
⊢ (𝐴 ≺ (𝐴 × 𝐴) → 𝐴 ∈ V) |
37 | | isfin7 10057 |
. . . . 5
⊢ (𝐴 ∈ V → (𝐴 ∈ FinVII ↔
¬ ∃𝑏 ∈ (On
∖ ω)𝐴 ≈
𝑏)) |
38 | 36, 37 | syl 17 |
. . . 4
⊢ (𝐴 ≺ (𝐴 × 𝐴) → (𝐴 ∈ FinVII ↔ ¬
∃𝑏 ∈ (On ∖
ω)𝐴 ≈ 𝑏)) |
39 | 34, 38 | mpbird 256 |
. . 3
⊢ (𝐴 ≺ (𝐴 × 𝐴) → 𝐴 ∈ FinVII) |
40 | 10, 39 | jaoi 854 |
. 2
⊢ ((𝐴 ≺ 2o ∨
𝐴 ≺ (𝐴 × 𝐴)) → 𝐴 ∈ FinVII) |
41 | 1, 40 | sylbi 216 |
1
⊢ (𝐴 ∈ FinVI →
𝐴 ∈
FinVII) |