Metamath Proof Explorer

Theorem ackbij1b

Description: The Ackermann bijection, part 1b: the bijection from ackbij1 restricts naturally to the powers of particular naturals. (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Hypothesis ackbij.f ⊢ F = x ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ y ∈ x y × 𝒫 y
Assertion ackbij1b ⊢ A ∈ ω → F 𝒫 A = card ⁡ 𝒫 A

Proof

Step Hyp Ref Expression
1 ackbij.f ⊢ F = x ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ y ∈ x y × 𝒫 y
2 1 ackbij1lem17 ⊢ F : 𝒫 ω ∩ Fin ⟶ 1-1 ω
3 ackbij2lem1 ⊢ A ∈ ω → 𝒫 A ⊆ 𝒫 ω ∩ Fin
4 pwexg ⊢ A ∈ ω → 𝒫 A ∈ V
5 f1imaeng ⊢ F : 𝒫 ω ∩ Fin ⟶ 1-1 ω ∧ 𝒫 A ⊆ 𝒫 ω ∩ Fin ∧ 𝒫 A ∈ V → F 𝒫 A ≈ 𝒫 A
6 2 3 4 5 mp3an2i ⊢ A ∈ ω → F 𝒫 A ≈ 𝒫 A
7 nnfi ⊢ A ∈ ω → A ∈ Fin
8 pwfi ⊢ A ∈ Fin ↔ 𝒫 A ∈ Fin
9 7 8 sylib ⊢ A ∈ ω → 𝒫 A ∈ Fin
10 ficardid ⊢ 𝒫 A ∈ Fin → card ⁡ 𝒫 A ≈ 𝒫 A
11 ensym ⊢ card ⁡ 𝒫 A ≈ 𝒫 A → 𝒫 A ≈ card ⁡ 𝒫 A
12 9 10 11 3syl ⊢ A ∈ ω → 𝒫 A ≈ card ⁡ 𝒫 A
13 entr ⊢ F 𝒫 A ≈ 𝒫 A ∧ 𝒫 A ≈ card ⁡ 𝒫 A → F 𝒫 A ≈ card ⁡ 𝒫 A
14 6 12 13 syl2anc ⊢ A ∈ ω → F 𝒫 A ≈ card ⁡ 𝒫 A
15 onfin2 ⊢ ω = On ∩ Fin
16 inss2 ⊢ On ∩ Fin ⊆ Fin
17 15 16 eqsstri ⊢ ω ⊆ Fin
18 ficardom ⊢ 𝒫 A ∈ Fin → card ⁡ 𝒫 A ∈ ω
19 9 18 syl ⊢ A ∈ ω → card ⁡ 𝒫 A ∈ ω
20 17 19 sselid ⊢ A ∈ ω → card ⁡ 𝒫 A ∈ Fin
21 php3 ⊢ card ⁡ 𝒫 A ∈ Fin ∧ F 𝒫 A ⊂ card ⁡ 𝒫 A → F 𝒫 A ≺ card ⁡ 𝒫 A
22 21 ex ⊢ card ⁡ 𝒫 A ∈ Fin → F 𝒫 A ⊂ card ⁡ 𝒫 A → F 𝒫 A ≺ card ⁡ 𝒫 A
23 20 22 syl ⊢ A ∈ ω → F 𝒫 A ⊂ card ⁡ 𝒫 A → F 𝒫 A ≺ card ⁡ 𝒫 A
24 sdomnen ⊢ F 𝒫 A ≺ card ⁡ 𝒫 A → ¬ F 𝒫 A ≈ card ⁡ 𝒫 A
25 23 24 syl6 ⊢ A ∈ ω → F 𝒫 A ⊂ card ⁡ 𝒫 A → ¬ F 𝒫 A ≈ card ⁡ 𝒫 A
26 14 25 mt2d ⊢ A ∈ ω → ¬ F 𝒫 A ⊂ card ⁡ 𝒫 A
27 fvex ⊢ F ⁡ a ∈ V
28 ackbij1lem3 ⊢ A ∈ ω → A ∈ 𝒫 ω ∩ Fin
29 elpwi ⊢ a ∈ 𝒫 A → a ⊆ A
30 1 ackbij1lem12 ⊢ A ∈ 𝒫 ω ∩ Fin ∧ a ⊆ A → F ⁡ a ⊆ F ⁡ A
31 28 29 30 syl2an ⊢ A ∈ ω ∧ a ∈ 𝒫 A → F ⁡ a ⊆ F ⁡ A
32 1 ackbij1lem10 ⊢ F : 𝒫 ω ∩ Fin ⟶ ω
33 peano1 ⊢ ∅ ∈ ω
34 32 33 f0cli ⊢ F ⁡ a ∈ ω
35 nnord ⊢ F ⁡ a ∈ ω → Ord ⁡ F ⁡ a
36 34 35 ax-mp ⊢ Ord ⁡ F ⁡ a
37 32 33 f0cli ⊢ F ⁡ A ∈ ω
38 nnord ⊢ F ⁡ A ∈ ω → Ord ⁡ F ⁡ A
39 37 38 ax-mp ⊢ Ord ⁡ F ⁡ A
40 ordsucsssuc ⊢ Ord ⁡ F ⁡ a ∧ Ord ⁡ F ⁡ A → F ⁡ a ⊆ F ⁡ A ↔ suc ⁡ F ⁡ a ⊆ suc ⁡ F ⁡ A
41 36 39 40 mp2an ⊢ F ⁡ a ⊆ F ⁡ A ↔ suc ⁡ F ⁡ a ⊆ suc ⁡ F ⁡ A
42 31 41 sylib ⊢ A ∈ ω ∧ a ∈ 𝒫 A → suc ⁡ F ⁡ a ⊆ suc ⁡ F ⁡ A
43 1 ackbij1lem14 ⊢ A ∈ ω → F ⁡ A = suc ⁡ F ⁡ A
44 1 ackbij1lem8 ⊢ A ∈ ω → F ⁡ A = card ⁡ 𝒫 A
45 43 44 eqtr3d ⊢ A ∈ ω → suc ⁡ F ⁡ A = card ⁡ 𝒫 A
46 45 adantr ⊢ A ∈ ω ∧ a ∈ 𝒫 A → suc ⁡ F ⁡ A = card ⁡ 𝒫 A
47 42 46 sseqtrd ⊢ A ∈ ω ∧ a ∈ 𝒫 A → suc ⁡ F ⁡ a ⊆ card ⁡ 𝒫 A
48 sucssel ⊢ F ⁡ a ∈ V → suc ⁡ F ⁡ a ⊆ card ⁡ 𝒫 A → F ⁡ a ∈ card ⁡ 𝒫 A
49 27 47 48 mpsyl ⊢ A ∈ ω ∧ a ∈ 𝒫 A → F ⁡ a ∈ card ⁡ 𝒫 A
50 49 ralrimiva ⊢ A ∈ ω → ∀ a ∈ 𝒫 A F ⁡ a ∈ card ⁡ 𝒫 A
51 f1fun ⊢ F : 𝒫 ω ∩ Fin ⟶ 1-1 ω → Fun ⁡ F
52 2 51 ax-mp ⊢ Fun ⁡ F
53 f1dm ⊢ F : 𝒫 ω ∩ Fin ⟶ 1-1 ω → dom ⁡ F = 𝒫 ω ∩ Fin
54 2 53 ax-mp ⊢ dom ⁡ F = 𝒫 ω ∩ Fin
55 3 54 sseqtrrdi ⊢ A ∈ ω → 𝒫 A ⊆ dom ⁡ F
56 funimass4 ⊢ Fun ⁡ F ∧ 𝒫 A ⊆ dom ⁡ F → F 𝒫 A ⊆ card ⁡ 𝒫 A ↔ ∀ a ∈ 𝒫 A F ⁡ a ∈ card ⁡ 𝒫 A
57 52 55 56 sylancr ⊢ A ∈ ω → F 𝒫 A ⊆ card ⁡ 𝒫 A ↔ ∀ a ∈ 𝒫 A F ⁡ a ∈ card ⁡ 𝒫 A
58 50 57 mpbird ⊢ A ∈ ω → F 𝒫 A ⊆ card ⁡ 𝒫 A
59 sspss ⊢ F 𝒫 A ⊆ card ⁡ 𝒫 A ↔ F 𝒫 A ⊂ card ⁡ 𝒫 A ∨ F 𝒫 A = card ⁡ 𝒫 A
60 58 59 sylib ⊢ A ∈ ω → F 𝒫 A ⊂ card ⁡ 𝒫 A ∨ F 𝒫 A = card ⁡ 𝒫 A
61 orel1 ⊢ ¬ F 𝒫 A ⊂ card ⁡ 𝒫 A → F 𝒫 A ⊂ card ⁡ 𝒫 A ∨ F 𝒫 A = card ⁡ 𝒫 A → F 𝒫 A = card ⁡ 𝒫 A
62 26 60 61 sylc ⊢ A ∈ ω → F 𝒫 A = card ⁡ 𝒫 A