Step | Hyp | Ref
| Expression |
1 | | ackbij.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) |
2 | 1 | ackbij1lem17 9729 |
. . . . 5
⊢ 𝐹:(𝒫 ω ∩
Fin)–1-1→ω |
3 | | ackbij2lem1 9712 |
. . . . 5
⊢ (𝐴 ∈ ω → 𝒫
𝐴 ⊆ (𝒫
ω ∩ Fin)) |
4 | | pwexg 5242 |
. . . . 5
⊢ (𝐴 ∈ ω → 𝒫
𝐴 ∈
V) |
5 | | f1imaeng 8608 |
. . . . 5
⊢ ((𝐹:(𝒫 ω ∩
Fin)–1-1→ω ∧
𝒫 𝐴 ⊆
(𝒫 ω ∩ Fin) ∧ 𝒫 𝐴 ∈ V) → (𝐹 “ 𝒫 𝐴) ≈ 𝒫 𝐴) |
6 | 2, 3, 4, 5 | mp3an2i 1467 |
. . . 4
⊢ (𝐴 ∈ ω → (𝐹 “ 𝒫 𝐴) ≈ 𝒫 𝐴) |
7 | | nnfi 8759 |
. . . . . 6
⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin) |
8 | | pwfi 8769 |
. . . . . 6
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
9 | 7, 8 | sylib 221 |
. . . . 5
⊢ (𝐴 ∈ ω → 𝒫
𝐴 ∈
Fin) |
10 | | ficardid 9457 |
. . . . 5
⊢
(𝒫 𝐴 ∈
Fin → (card‘𝒫 𝐴) ≈ 𝒫 𝐴) |
11 | | ensym 8597 |
. . . . 5
⊢
((card‘𝒫 𝐴) ≈ 𝒫 𝐴 → 𝒫 𝐴 ≈ (card‘𝒫 𝐴)) |
12 | 9, 10, 11 | 3syl 18 |
. . . 4
⊢ (𝐴 ∈ ω → 𝒫
𝐴 ≈
(card‘𝒫 𝐴)) |
13 | | entr 8600 |
. . . 4
⊢ (((𝐹 “ 𝒫 𝐴) ≈ 𝒫 𝐴 ∧ 𝒫 𝐴 ≈ (card‘𝒫
𝐴)) → (𝐹 “ 𝒫 𝐴) ≈ (card‘𝒫
𝐴)) |
14 | 6, 12, 13 | syl2anc 587 |
. . 3
⊢ (𝐴 ∈ ω → (𝐹 “ 𝒫 𝐴) ≈ (card‘𝒫
𝐴)) |
15 | | onfin2 8783 |
. . . . . . 7
⊢ ω =
(On ∩ Fin) |
16 | | inss2 4118 |
. . . . . . 7
⊢ (On ∩
Fin) ⊆ Fin |
17 | 15, 16 | eqsstri 3909 |
. . . . . 6
⊢ ω
⊆ Fin |
18 | | ficardom 9456 |
. . . . . . 7
⊢
(𝒫 𝐴 ∈
Fin → (card‘𝒫 𝐴) ∈ ω) |
19 | 9, 18 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ω →
(card‘𝒫 𝐴)
∈ ω) |
20 | 17, 19 | sseldi 3873 |
. . . . 5
⊢ (𝐴 ∈ ω →
(card‘𝒫 𝐴)
∈ Fin) |
21 | | php3 8746 |
. . . . . 6
⊢
(((card‘𝒫 𝐴) ∈ Fin ∧ (𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫 𝐴)) → (𝐹 “ 𝒫 𝐴) ≺ (card‘𝒫 𝐴)) |
22 | 21 | ex 416 |
. . . . 5
⊢
((card‘𝒫 𝐴) ∈ Fin → ((𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫 𝐴) → (𝐹 “ 𝒫 𝐴) ≺ (card‘𝒫 𝐴))) |
23 | 20, 22 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ω → ((𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫
𝐴) → (𝐹 “ 𝒫 𝐴) ≺ (card‘𝒫
𝐴))) |
24 | | sdomnen 8577 |
. . . 4
⊢ ((𝐹 “ 𝒫 𝐴) ≺ (card‘𝒫
𝐴) → ¬ (𝐹 “ 𝒫 𝐴) ≈ (card‘𝒫
𝐴)) |
25 | 23, 24 | syl6 35 |
. . 3
⊢ (𝐴 ∈ ω → ((𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫
𝐴) → ¬ (𝐹 “ 𝒫 𝐴) ≈ (card‘𝒫
𝐴))) |
26 | 14, 25 | mt2d 138 |
. 2
⊢ (𝐴 ∈ ω → ¬
(𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫
𝐴)) |
27 | | fvex 6681 |
. . . . . 6
⊢ (𝐹‘𝑎) ∈ V |
28 | | ackbij1lem3 9715 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → 𝐴 ∈ (𝒫 ω ∩
Fin)) |
29 | | elpwi 4494 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝒫 𝐴 → 𝑎 ⊆ 𝐴) |
30 | 1 | ackbij1lem12 9724 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝑎 ⊆ 𝐴) → (𝐹‘𝑎) ⊆ (𝐹‘𝐴)) |
31 | 28, 29, 30 | syl2an 599 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑎 ∈ 𝒫 𝐴) → (𝐹‘𝑎) ⊆ (𝐹‘𝐴)) |
32 | 1 | ackbij1lem10 9722 |
. . . . . . . . . . 11
⊢ 𝐹:(𝒫 ω ∩
Fin)⟶ω |
33 | | peano1 7614 |
. . . . . . . . . . 11
⊢ ∅
∈ ω |
34 | 32, 33 | f0cli 6868 |
. . . . . . . . . 10
⊢ (𝐹‘𝑎) ∈ ω |
35 | | nnord 7601 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑎) ∈ ω → Ord (𝐹‘𝑎)) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . 9
⊢ Ord
(𝐹‘𝑎) |
37 | 32, 33 | f0cli 6868 |
. . . . . . . . . 10
⊢ (𝐹‘𝐴) ∈ ω |
38 | | nnord 7601 |
. . . . . . . . . 10
⊢ ((𝐹‘𝐴) ∈ ω → Ord (𝐹‘𝐴)) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . 9
⊢ Ord
(𝐹‘𝐴) |
40 | | ordsucsssuc 7551 |
. . . . . . . . 9
⊢ ((Ord
(𝐹‘𝑎) ∧ Ord (𝐹‘𝐴)) → ((𝐹‘𝑎) ⊆ (𝐹‘𝐴) ↔ suc (𝐹‘𝑎) ⊆ suc (𝐹‘𝐴))) |
41 | 36, 39, 40 | mp2an 692 |
. . . . . . . 8
⊢ ((𝐹‘𝑎) ⊆ (𝐹‘𝐴) ↔ suc (𝐹‘𝑎) ⊆ suc (𝐹‘𝐴)) |
42 | 31, 41 | sylib 221 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝑎 ∈ 𝒫 𝐴) → suc (𝐹‘𝑎) ⊆ suc (𝐹‘𝐴)) |
43 | 1 | ackbij1lem14 9726 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = suc (𝐹‘𝐴)) |
44 | 1 | ackbij1lem8 9720 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = (card‘𝒫 𝐴)) |
45 | 43, 44 | eqtr3d 2775 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → suc
(𝐹‘𝐴) = (card‘𝒫 𝐴)) |
46 | 45 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝑎 ∈ 𝒫 𝐴) → suc (𝐹‘𝐴) = (card‘𝒫 𝐴)) |
47 | 42, 46 | sseqtrd 3915 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝑎 ∈ 𝒫 𝐴) → suc (𝐹‘𝑎) ⊆ (card‘𝒫 𝐴)) |
48 | | sucssel 6258 |
. . . . . 6
⊢ ((𝐹‘𝑎) ∈ V → (suc (𝐹‘𝑎) ⊆ (card‘𝒫 𝐴) → (𝐹‘𝑎) ∈ (card‘𝒫 𝐴))) |
49 | 27, 47, 48 | mpsyl 68 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝑎 ∈ 𝒫 𝐴) → (𝐹‘𝑎) ∈ (card‘𝒫 𝐴)) |
50 | 49 | ralrimiva 3096 |
. . . 4
⊢ (𝐴 ∈ ω →
∀𝑎 ∈ 𝒫
𝐴(𝐹‘𝑎) ∈ (card‘𝒫 𝐴)) |
51 | | f1fun 6570 |
. . . . . 6
⊢ (𝐹:(𝒫 ω ∩
Fin)–1-1→ω → Fun
𝐹) |
52 | 2, 51 | ax-mp 5 |
. . . . 5
⊢ Fun 𝐹 |
53 | | f1dm 6572 |
. . . . . . 7
⊢ (𝐹:(𝒫 ω ∩
Fin)–1-1→ω → dom
𝐹 = (𝒫 ω
∩ Fin)) |
54 | 2, 53 | ax-mp 5 |
. . . . . 6
⊢ dom 𝐹 = (𝒫 ω ∩
Fin) |
55 | 3, 54 | sseqtrrdi 3926 |
. . . . 5
⊢ (𝐴 ∈ ω → 𝒫
𝐴 ⊆ dom 𝐹) |
56 | | funimass4 6728 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝒫 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝒫 𝐴) ⊆ (card‘𝒫 𝐴) ↔ ∀𝑎 ∈ 𝒫 𝐴(𝐹‘𝑎) ∈ (card‘𝒫 𝐴))) |
57 | 52, 55, 56 | sylancr 590 |
. . . 4
⊢ (𝐴 ∈ ω → ((𝐹 “ 𝒫 𝐴) ⊆ (card‘𝒫
𝐴) ↔ ∀𝑎 ∈ 𝒫 𝐴(𝐹‘𝑎) ∈ (card‘𝒫 𝐴))) |
58 | 50, 57 | mpbird 260 |
. . 3
⊢ (𝐴 ∈ ω → (𝐹 “ 𝒫 𝐴) ⊆ (card‘𝒫
𝐴)) |
59 | | sspss 3988 |
. . 3
⊢ ((𝐹 “ 𝒫 𝐴) ⊆ (card‘𝒫
𝐴) ↔ ((𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫
𝐴) ∨ (𝐹 “ 𝒫 𝐴) = (card‘𝒫 𝐴))) |
60 | 58, 59 | sylib 221 |
. 2
⊢ (𝐴 ∈ ω → ((𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫
𝐴) ∨ (𝐹 “ 𝒫 𝐴) = (card‘𝒫 𝐴))) |
61 | | orel1 888 |
. 2
⊢ (¬
(𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫
𝐴) → (((𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫
𝐴) ∨ (𝐹 “ 𝒫 𝐴) = (card‘𝒫 𝐴)) → (𝐹 “ 𝒫 𝐴) = (card‘𝒫 𝐴))) |
62 | 26, 60, 61 | sylc 65 |
1
⊢ (𝐴 ∈ ω → (𝐹 “ 𝒫 𝐴) = (card‘𝒫 𝐴)) |