Proof of Theorem sdom2en01
Step | Hyp | Ref
| Expression |
1 | | onfin2 8152 |
. . . . 5
⊢ ω =
(On ∩ Fin) |
2 | | inss2 3834 |
. . . . 5
⊢ (On ∩
Fin) ⊆ Fin |
3 | 1, 2 | eqsstri 3635 |
. . . 4
⊢ ω
⊆ Fin |
4 | | 2onn 7720 |
. . . 4
⊢
2𝑜 ∈ ω |
5 | 3, 4 | sselii 3600 |
. . 3
⊢
2𝑜 ∈ Fin |
6 | | sdomdom 7983 |
. . 3
⊢ (𝐴 ≺ 2𝑜
→ 𝐴 ≼
2𝑜) |
7 | | domfi 8181 |
. . 3
⊢
((2𝑜 ∈ Fin ∧ 𝐴 ≼ 2𝑜) → 𝐴 ∈ Fin) |
8 | 5, 6, 7 | sylancr 695 |
. 2
⊢ (𝐴 ≺ 2𝑜
→ 𝐴 ∈
Fin) |
9 | | id 22 |
. . . 4
⊢ (𝐴 = ∅ → 𝐴 = ∅) |
10 | | 0fin 8188 |
. . . 4
⊢ ∅
∈ Fin |
11 | 9, 10 | syl6eqel 2709 |
. . 3
⊢ (𝐴 = ∅ → 𝐴 ∈ Fin) |
12 | | 1onn 7719 |
. . . . 5
⊢
1𝑜 ∈ ω |
13 | 3, 12 | sselii 3600 |
. . . 4
⊢
1𝑜 ∈ Fin |
14 | | enfi 8176 |
. . . 4
⊢ (𝐴 ≈ 1𝑜
→ (𝐴 ∈ Fin ↔
1𝑜 ∈ Fin)) |
15 | 13, 14 | mpbiri 248 |
. . 3
⊢ (𝐴 ≈ 1𝑜
→ 𝐴 ∈
Fin) |
16 | 11, 15 | jaoi 394 |
. 2
⊢ ((𝐴 = ∅ ∨ 𝐴 ≈ 1𝑜)
→ 𝐴 ∈
Fin) |
17 | | df2o3 7573 |
. . . . . 6
⊢
2𝑜 = {∅,
1𝑜} |
18 | 17 | eleq2i 2693 |
. . . . 5
⊢
((card‘𝐴)
∈ 2𝑜 ↔ (card‘𝐴) ∈ {∅,
1𝑜}) |
19 | | fvex 6201 |
. . . . . 6
⊢
(card‘𝐴)
∈ V |
20 | 19 | elpr 4198 |
. . . . 5
⊢
((card‘𝐴)
∈ {∅, 1𝑜} ↔ ((card‘𝐴) = ∅ ∨ (card‘𝐴) =
1𝑜)) |
21 | 18, 20 | bitri 264 |
. . . 4
⊢
((card‘𝐴)
∈ 2𝑜 ↔ ((card‘𝐴) = ∅ ∨ (card‘𝐴) =
1𝑜)) |
22 | 21 | a1i 11 |
. . 3
⊢ (𝐴 ∈ Fin →
((card‘𝐴) ∈
2𝑜 ↔ ((card‘𝐴) = ∅ ∨ (card‘𝐴) =
1𝑜))) |
23 | | cardnn 8789 |
. . . . . 6
⊢
(2𝑜 ∈ ω →
(card‘2𝑜) = 2𝑜) |
24 | 4, 23 | ax-mp 5 |
. . . . 5
⊢
(card‘2𝑜) =
2𝑜 |
25 | 24 | eleq2i 2693 |
. . . 4
⊢
((card‘𝐴)
∈ (card‘2𝑜) ↔ (card‘𝐴) ∈
2𝑜) |
26 | | finnum 8774 |
. . . . 5
⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom
card) |
27 | | 2on 7568 |
. . . . . 6
⊢
2𝑜 ∈ On |
28 | | onenon 8775 |
. . . . . 6
⊢
(2𝑜 ∈ On → 2𝑜 ∈ dom
card) |
29 | 27, 28 | ax-mp 5 |
. . . . 5
⊢
2𝑜 ∈ dom card |
30 | | cardsdom2 8814 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧
2𝑜 ∈ dom card) → ((card‘𝐴) ∈ (card‘2𝑜)
↔ 𝐴 ≺
2𝑜)) |
31 | 26, 29, 30 | sylancl 694 |
. . . 4
⊢ (𝐴 ∈ Fin →
((card‘𝐴) ∈
(card‘2𝑜) ↔ 𝐴 ≺
2𝑜)) |
32 | 25, 31 | syl5bbr 274 |
. . 3
⊢ (𝐴 ∈ Fin →
((card‘𝐴) ∈
2𝑜 ↔ 𝐴 ≺
2𝑜)) |
33 | | cardnueq0 8790 |
. . . . 5
⊢ (𝐴 ∈ dom card →
((card‘𝐴) = ∅
↔ 𝐴 =
∅)) |
34 | 26, 33 | syl 17 |
. . . 4
⊢ (𝐴 ∈ Fin →
((card‘𝐴) = ∅
↔ 𝐴 =
∅)) |
35 | | cardnn 8789 |
. . . . . . 7
⊢
(1𝑜 ∈ ω →
(card‘1𝑜) = 1𝑜) |
36 | 12, 35 | ax-mp 5 |
. . . . . 6
⊢
(card‘1𝑜) =
1𝑜 |
37 | 36 | eqeq2i 2634 |
. . . . 5
⊢
((card‘𝐴) =
(card‘1𝑜) ↔ (card‘𝐴) = 1𝑜) |
38 | | finnum 8774 |
. . . . . . 7
⊢
(1𝑜 ∈ Fin → 1𝑜 ∈
dom card) |
39 | 13, 38 | ax-mp 5 |
. . . . . 6
⊢
1𝑜 ∈ dom card |
40 | | carden2 8813 |
. . . . . 6
⊢ ((𝐴 ∈ dom card ∧
1𝑜 ∈ dom card) → ((card‘𝐴) = (card‘1𝑜)
↔ 𝐴 ≈
1𝑜)) |
41 | 26, 39, 40 | sylancl 694 |
. . . . 5
⊢ (𝐴 ∈ Fin →
((card‘𝐴) =
(card‘1𝑜) ↔ 𝐴 ≈
1𝑜)) |
42 | 37, 41 | syl5bbr 274 |
. . . 4
⊢ (𝐴 ∈ Fin →
((card‘𝐴) =
1𝑜 ↔ 𝐴 ≈
1𝑜)) |
43 | 34, 42 | orbi12d 746 |
. . 3
⊢ (𝐴 ∈ Fin →
(((card‘𝐴) = ∅
∨ (card‘𝐴) =
1𝑜) ↔ (𝐴 = ∅ ∨ 𝐴 ≈
1𝑜))) |
44 | 22, 32, 43 | 3bitr3d 298 |
. 2
⊢ (𝐴 ∈ Fin → (𝐴 ≺ 2𝑜
↔ (𝐴 = ∅ ∨
𝐴 ≈
1𝑜))) |
45 | 8, 16, 44 | pm5.21nii 368 |
1
⊢ (𝐴 ≺ 2𝑜
↔ (𝐴 = ∅ ∨
𝐴 ≈
1𝑜)) |