Step | Hyp | Ref
| Expression |
1 | | isfin6 9005 |
. 2
⊢ (𝐴 ∈ FinVI ↔
(𝐴 ≺
2𝑜 ∨ 𝐴 ≺ (𝐴 × 𝐴))) |
2 | | 2onn 7607 |
. . . . . 6
⊢
2𝑜 ∈ ω |
3 | | ssid 3587 |
. . . . . 6
⊢
2𝑜 ⊆ 2𝑜 |
4 | | ssnnfi 8064 |
. . . . . 6
⊢
((2𝑜 ∈ ω ∧ 2𝑜
⊆ 2𝑜) → 2𝑜 ∈
Fin) |
5 | 2, 3, 4 | mp2an 704 |
. . . . 5
⊢
2𝑜 ∈ Fin |
6 | | sdomdom 7869 |
. . . . 5
⊢ (𝐴 ≺ 2𝑜
→ 𝐴 ≼
2𝑜) |
7 | | domfi 8066 |
. . . . 5
⊢
((2𝑜 ∈ Fin ∧ 𝐴 ≼ 2𝑜) → 𝐴 ∈ Fin) |
8 | 5, 6, 7 | sylancr 694 |
. . . 4
⊢ (𝐴 ≺ 2𝑜
→ 𝐴 ∈
Fin) |
9 | | fin17 9099 |
. . . 4
⊢ (𝐴 ∈ Fin → 𝐴 ∈
FinVII) |
10 | 8, 9 | syl 17 |
. . 3
⊢ (𝐴 ≺ 2𝑜
→ 𝐴 ∈
FinVII) |
11 | | sdomnen 7870 |
. . . . 5
⊢ (𝐴 ≺ (𝐴 × 𝐴) → ¬ 𝐴 ≈ (𝐴 × 𝐴)) |
12 | | eldifi 3694 |
. . . . . . . . 9
⊢ (𝑏 ∈ (On ∖ ω)
→ 𝑏 ∈
On) |
13 | | ensym 7891 |
. . . . . . . . 9
⊢ (𝐴 ≈ 𝑏 → 𝑏 ≈ 𝐴) |
14 | | isnumi 8655 |
. . . . . . . . 9
⊢ ((𝑏 ∈ On ∧ 𝑏 ≈ 𝐴) → 𝐴 ∈ dom card) |
15 | 12, 13, 14 | syl2an 493 |
. . . . . . . 8
⊢ ((𝑏 ∈ (On ∖ ω)
∧ 𝐴 ≈ 𝑏) → 𝐴 ∈ dom card) |
16 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑏 ∈ V |
17 | | eldif 3550 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ (On ∖ ω)
↔ (𝑏 ∈ On ∧
¬ 𝑏 ∈
ω)) |
18 | | ordom 6966 |
. . . . . . . . . . . . . 14
⊢ Ord
ω |
19 | | eloni 5650 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ On → Ord 𝑏) |
20 | | ordtri1 5673 |
. . . . . . . . . . . . . 14
⊢ ((Ord
ω ∧ Ord 𝑏) →
(ω ⊆ 𝑏 ↔
¬ 𝑏 ∈
ω)) |
21 | 18, 19, 20 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ On → (ω
⊆ 𝑏 ↔ ¬
𝑏 ∈
ω)) |
22 | 21 | biimpar 501 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ On ∧ ¬ 𝑏 ∈ ω) → ω
⊆ 𝑏) |
23 | 17, 22 | sylbi 206 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (On ∖ ω)
→ ω ⊆ 𝑏) |
24 | | ssdomg 7887 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ V → (ω
⊆ 𝑏 → ω
≼ 𝑏)) |
25 | 16, 23, 24 | mpsyl 66 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (On ∖ ω)
→ ω ≼ 𝑏) |
26 | | domen2 7988 |
. . . . . . . . . 10
⊢ (𝐴 ≈ 𝑏 → (ω ≼ 𝐴 ↔ ω ≼ 𝑏)) |
27 | 25, 26 | syl5ibr 235 |
. . . . . . . . 9
⊢ (𝐴 ≈ 𝑏 → (𝑏 ∈ (On ∖ ω) → ω
≼ 𝐴)) |
28 | 27 | impcom 445 |
. . . . . . . 8
⊢ ((𝑏 ∈ (On ∖ ω)
∧ 𝐴 ≈ 𝑏) → ω ≼ 𝐴) |
29 | | infxpidm2 8723 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴) |
30 | 15, 28, 29 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑏 ∈ (On ∖ ω)
∧ 𝐴 ≈ 𝑏) → (𝐴 × 𝐴) ≈ 𝐴) |
31 | | ensym 7891 |
. . . . . . 7
⊢ ((𝐴 × 𝐴) ≈ 𝐴 → 𝐴 ≈ (𝐴 × 𝐴)) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ ((𝑏 ∈ (On ∖ ω)
∧ 𝐴 ≈ 𝑏) → 𝐴 ≈ (𝐴 × 𝐴)) |
33 | 32 | rexlimiva 3010 |
. . . . 5
⊢
(∃𝑏 ∈ (On
∖ ω)𝐴 ≈
𝑏 → 𝐴 ≈ (𝐴 × 𝐴)) |
34 | 11, 33 | nsyl 134 |
. . . 4
⊢ (𝐴 ≺ (𝐴 × 𝐴) → ¬ ∃𝑏 ∈ (On ∖ ω)𝐴 ≈ 𝑏) |
35 | | relsdom 7848 |
. . . . . 6
⊢ Rel
≺ |
36 | 35 | brrelexi 5082 |
. . . . 5
⊢ (𝐴 ≺ (𝐴 × 𝐴) → 𝐴 ∈ V) |
37 | | isfin7 9006 |
. . . . 5
⊢ (𝐴 ∈ V → (𝐴 ∈ FinVII ↔
¬ ∃𝑏 ∈ (On
∖ ω)𝐴 ≈
𝑏)) |
38 | 36, 37 | syl 17 |
. . . 4
⊢ (𝐴 ≺ (𝐴 × 𝐴) → (𝐴 ∈ FinVII ↔ ¬
∃𝑏 ∈ (On ∖
ω)𝐴 ≈ 𝑏)) |
39 | 34, 38 | mpbird 246 |
. . 3
⊢ (𝐴 ≺ (𝐴 × 𝐴) → 𝐴 ∈ FinVII) |
40 | 10, 39 | jaoi 393 |
. 2
⊢ ((𝐴 ≺ 2𝑜
∨ 𝐴 ≺ (𝐴 × 𝐴)) → 𝐴 ∈ FinVII) |
41 | 1, 40 | sylbi 206 |
1
⊢ (𝐴 ∈ FinVI →
𝐴 ∈
FinVII) |