Step | Hyp | Ref
| Expression |
1 | | ackbij2lem1 8924 |
. . . . 5
⊢ (𝐴 ∈ ω → 𝒫
𝐴 ⊆ (𝒫
ω ∩ Fin)) |
2 | | pwexg 4776 |
. . . . 5
⊢ (𝐴 ∈ ω → 𝒫
𝐴 ∈
V) |
3 | | ackbij.f |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) |
4 | 3 | ackbij1lem17 8941 |
. . . . . 6
⊢ 𝐹:(𝒫 ω ∩
Fin)–1-1→ω |
5 | | f1imaeng 7902 |
. . . . . 6
⊢ ((𝐹:(𝒫 ω ∩
Fin)–1-1→ω ∧
𝒫 𝐴 ⊆
(𝒫 ω ∩ Fin) ∧ 𝒫 𝐴 ∈ V) → (𝐹 “ 𝒫 𝐴) ≈ 𝒫 𝐴) |
6 | 4, 5 | mp3an1 1403 |
. . . . 5
⊢
((𝒫 𝐴
⊆ (𝒫 ω ∩ Fin) ∧ 𝒫 𝐴 ∈ V) → (𝐹 “ 𝒫 𝐴) ≈ 𝒫 𝐴) |
7 | 1, 2, 6 | syl2anc 691 |
. . . 4
⊢ (𝐴 ∈ ω → (𝐹 “ 𝒫 𝐴) ≈ 𝒫 𝐴) |
8 | | nnfi 8038 |
. . . . . 6
⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin) |
9 | | pwfi 8144 |
. . . . . 6
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
10 | 8, 9 | sylib 207 |
. . . . 5
⊢ (𝐴 ∈ ω → 𝒫
𝐴 ∈
Fin) |
11 | | ficardid 8671 |
. . . . 5
⊢
(𝒫 𝐴 ∈
Fin → (card‘𝒫 𝐴) ≈ 𝒫 𝐴) |
12 | | ensym 7891 |
. . . . 5
⊢
((card‘𝒫 𝐴) ≈ 𝒫 𝐴 → 𝒫 𝐴 ≈ (card‘𝒫 𝐴)) |
13 | 10, 11, 12 | 3syl 18 |
. . . 4
⊢ (𝐴 ∈ ω → 𝒫
𝐴 ≈
(card‘𝒫 𝐴)) |
14 | | entr 7894 |
. . . 4
⊢ (((𝐹 “ 𝒫 𝐴) ≈ 𝒫 𝐴 ∧ 𝒫 𝐴 ≈ (card‘𝒫
𝐴)) → (𝐹 “ 𝒫 𝐴) ≈ (card‘𝒫
𝐴)) |
15 | 7, 13, 14 | syl2anc 691 |
. . 3
⊢ (𝐴 ∈ ω → (𝐹 “ 𝒫 𝐴) ≈ (card‘𝒫
𝐴)) |
16 | | onfin2 8037 |
. . . . . . 7
⊢ ω =
(On ∩ Fin) |
17 | | inss2 3796 |
. . . . . . 7
⊢ (On ∩
Fin) ⊆ Fin |
18 | 16, 17 | eqsstri 3598 |
. . . . . 6
⊢ ω
⊆ Fin |
19 | | ficardom 8670 |
. . . . . . 7
⊢
(𝒫 𝐴 ∈
Fin → (card‘𝒫 𝐴) ∈ ω) |
20 | 10, 19 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ω →
(card‘𝒫 𝐴)
∈ ω) |
21 | 18, 20 | sseldi 3566 |
. . . . 5
⊢ (𝐴 ∈ ω →
(card‘𝒫 𝐴)
∈ Fin) |
22 | | php3 8031 |
. . . . . 6
⊢
(((card‘𝒫 𝐴) ∈ Fin ∧ (𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫 𝐴)) → (𝐹 “ 𝒫 𝐴) ≺ (card‘𝒫 𝐴)) |
23 | 22 | ex 449 |
. . . . 5
⊢
((card‘𝒫 𝐴) ∈ Fin → ((𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫 𝐴) → (𝐹 “ 𝒫 𝐴) ≺ (card‘𝒫 𝐴))) |
24 | 21, 23 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ω → ((𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫
𝐴) → (𝐹 “ 𝒫 𝐴) ≺ (card‘𝒫
𝐴))) |
25 | | sdomnen 7870 |
. . . 4
⊢ ((𝐹 “ 𝒫 𝐴) ≺ (card‘𝒫
𝐴) → ¬ (𝐹 “ 𝒫 𝐴) ≈ (card‘𝒫
𝐴)) |
26 | 24, 25 | syl6 34 |
. . 3
⊢ (𝐴 ∈ ω → ((𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫
𝐴) → ¬ (𝐹 “ 𝒫 𝐴) ≈ (card‘𝒫
𝐴))) |
27 | 15, 26 | mt2d 130 |
. 2
⊢ (𝐴 ∈ ω → ¬
(𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫
𝐴)) |
28 | | fvex 6113 |
. . . . . 6
⊢ (𝐹‘𝑎) ∈ V |
29 | | ackbij1lem3 8927 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → 𝐴 ∈ (𝒫 ω ∩
Fin)) |
30 | | elpwi 4117 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝒫 𝐴 → 𝑎 ⊆ 𝐴) |
31 | 3 | ackbij1lem12 8936 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝑎 ⊆ 𝐴) → (𝐹‘𝑎) ⊆ (𝐹‘𝐴)) |
32 | 29, 30, 31 | syl2an 493 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑎 ∈ 𝒫 𝐴) → (𝐹‘𝑎) ⊆ (𝐹‘𝐴)) |
33 | 3 | ackbij1lem10 8934 |
. . . . . . . . . . 11
⊢ 𝐹:(𝒫 ω ∩
Fin)⟶ω |
34 | | peano1 6977 |
. . . . . . . . . . 11
⊢ ∅
∈ ω |
35 | 33, 34 | f0cli 6278 |
. . . . . . . . . 10
⊢ (𝐹‘𝑎) ∈ ω |
36 | | nnord 6965 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑎) ∈ ω → Ord (𝐹‘𝑎)) |
37 | 35, 36 | ax-mp 5 |
. . . . . . . . 9
⊢ Ord
(𝐹‘𝑎) |
38 | 33, 34 | f0cli 6278 |
. . . . . . . . . 10
⊢ (𝐹‘𝐴) ∈ ω |
39 | | nnord 6965 |
. . . . . . . . . 10
⊢ ((𝐹‘𝐴) ∈ ω → Ord (𝐹‘𝐴)) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . 9
⊢ Ord
(𝐹‘𝐴) |
41 | | ordsucsssuc 6915 |
. . . . . . . . 9
⊢ ((Ord
(𝐹‘𝑎) ∧ Ord (𝐹‘𝐴)) → ((𝐹‘𝑎) ⊆ (𝐹‘𝐴) ↔ suc (𝐹‘𝑎) ⊆ suc (𝐹‘𝐴))) |
42 | 37, 40, 41 | mp2an 704 |
. . . . . . . 8
⊢ ((𝐹‘𝑎) ⊆ (𝐹‘𝐴) ↔ suc (𝐹‘𝑎) ⊆ suc (𝐹‘𝐴)) |
43 | 32, 42 | sylib 207 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝑎 ∈ 𝒫 𝐴) → suc (𝐹‘𝑎) ⊆ suc (𝐹‘𝐴)) |
44 | 3 | ackbij1lem14 8938 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = suc (𝐹‘𝐴)) |
45 | 3 | ackbij1lem8 8932 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = (card‘𝒫 𝐴)) |
46 | 44, 45 | eqtr3d 2646 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → suc
(𝐹‘𝐴) = (card‘𝒫 𝐴)) |
47 | 46 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝑎 ∈ 𝒫 𝐴) → suc (𝐹‘𝐴) = (card‘𝒫 𝐴)) |
48 | 43, 47 | sseqtrd 3604 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝑎 ∈ 𝒫 𝐴) → suc (𝐹‘𝑎) ⊆ (card‘𝒫 𝐴)) |
49 | | sucssel 5736 |
. . . . . 6
⊢ ((𝐹‘𝑎) ∈ V → (suc (𝐹‘𝑎) ⊆ (card‘𝒫 𝐴) → (𝐹‘𝑎) ∈ (card‘𝒫 𝐴))) |
50 | 28, 48, 49 | mpsyl 66 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝑎 ∈ 𝒫 𝐴) → (𝐹‘𝑎) ∈ (card‘𝒫 𝐴)) |
51 | 50 | ralrimiva 2949 |
. . . 4
⊢ (𝐴 ∈ ω →
∀𝑎 ∈ 𝒫
𝐴(𝐹‘𝑎) ∈ (card‘𝒫 𝐴)) |
52 | | f1fun 6016 |
. . . . . 6
⊢ (𝐹:(𝒫 ω ∩
Fin)–1-1→ω → Fun
𝐹) |
53 | 4, 52 | ax-mp 5 |
. . . . 5
⊢ Fun 𝐹 |
54 | | f1dm 6018 |
. . . . . . 7
⊢ (𝐹:(𝒫 ω ∩
Fin)–1-1→ω → dom
𝐹 = (𝒫 ω
∩ Fin)) |
55 | 4, 54 | ax-mp 5 |
. . . . . 6
⊢ dom 𝐹 = (𝒫 ω ∩
Fin) |
56 | 1, 55 | syl6sseqr 3615 |
. . . . 5
⊢ (𝐴 ∈ ω → 𝒫
𝐴 ⊆ dom 𝐹) |
57 | | funimass4 6157 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝒫 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝒫 𝐴) ⊆ (card‘𝒫 𝐴) ↔ ∀𝑎 ∈ 𝒫 𝐴(𝐹‘𝑎) ∈ (card‘𝒫 𝐴))) |
58 | 53, 56, 57 | sylancr 694 |
. . . 4
⊢ (𝐴 ∈ ω → ((𝐹 “ 𝒫 𝐴) ⊆ (card‘𝒫
𝐴) ↔ ∀𝑎 ∈ 𝒫 𝐴(𝐹‘𝑎) ∈ (card‘𝒫 𝐴))) |
59 | 51, 58 | mpbird 246 |
. . 3
⊢ (𝐴 ∈ ω → (𝐹 “ 𝒫 𝐴) ⊆ (card‘𝒫
𝐴)) |
60 | | sspss 3668 |
. . 3
⊢ ((𝐹 “ 𝒫 𝐴) ⊆ (card‘𝒫
𝐴) ↔ ((𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫
𝐴) ∨ (𝐹 “ 𝒫 𝐴) = (card‘𝒫 𝐴))) |
61 | 59, 60 | sylib 207 |
. 2
⊢ (𝐴 ∈ ω → ((𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫
𝐴) ∨ (𝐹 “ 𝒫 𝐴) = (card‘𝒫 𝐴))) |
62 | | orel1 396 |
. 2
⊢ (¬
(𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫
𝐴) → (((𝐹 “ 𝒫 𝐴) ⊊ (card‘𝒫
𝐴) ∨ (𝐹 “ 𝒫 𝐴) = (card‘𝒫 𝐴)) → (𝐹 “ 𝒫 𝐴) = (card‘𝒫 𝐴))) |
63 | 27, 61, 62 | sylc 63 |
1
⊢ (𝐴 ∈ ω → (𝐹 “ 𝒫 𝐴) = (card‘𝒫 𝐴)) |