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 ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
Assertion ackbij1b ( 𝐴 ∈ ω → ( 𝐹 “ 𝒫 𝐴 ) = ( card ‘ 𝒫 𝐴 ) )

Proof

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