This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ackbij1lem14

Description: Lemma for ackbij1 . (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Hypothesis ackbij.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
Assertion ackbij1lem14 ( 𝐴 ∈ ω → ( 𝐹 ‘ { 𝐴 } ) = suc ( 𝐹 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ackbij.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
2 1 ackbij1lem8 ⊢ ( 𝐴 ∈ ω → ( 𝐹 ‘ { 𝐴 } ) = ( card ‘ 𝒫 𝐴 ) )
3 pweq ⊢ ( 𝑎 = ∅ → 𝒫 𝑎 = 𝒫 ∅ )
4 3 fveq2d ⊢ ( 𝑎 = ∅ → ( card ‘ 𝒫 𝑎 ) = ( card ‘ 𝒫 ∅ ) )
5 fveq2 ⊢ ( 𝑎 = ∅ → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ ∅ ) )
6 suceq ⊢ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ ∅ ) → suc ( 𝐹 ‘ 𝑎 ) = suc ( 𝐹 ‘ ∅ ) )
7 5 6 syl ⊢ ( 𝑎 = ∅ → suc ( 𝐹 ‘ 𝑎 ) = suc ( 𝐹 ‘ ∅ ) )
8 4 7 eqeq12d ⊢ ( 𝑎 = ∅ → ( ( card ‘ 𝒫 𝑎 ) = suc ( 𝐹 ‘ 𝑎 ) ↔ ( card ‘ 𝒫 ∅ ) = suc ( 𝐹 ‘ ∅ ) ) )
9 pweq ⊢ ( 𝑎 = 𝑏 → 𝒫 𝑎 = 𝒫 𝑏 )
10 9 fveq2d ⊢ ( 𝑎 = 𝑏 → ( card ‘ 𝒫 𝑎 ) = ( card ‘ 𝒫 𝑏 ) )
11 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) )
12 suceq ⊢ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → suc ( 𝐹 ‘ 𝑎 ) = suc ( 𝐹 ‘ 𝑏 ) )
13 11 12 syl ⊢ ( 𝑎 = 𝑏 → suc ( 𝐹 ‘ 𝑎 ) = suc ( 𝐹 ‘ 𝑏 ) )
14 10 13 eqeq12d ⊢ ( 𝑎 = 𝑏 → ( ( card ‘ 𝒫 𝑎 ) = suc ( 𝐹 ‘ 𝑎 ) ↔ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) )
15 pweq ⊢ ( 𝑎 = suc 𝑏 → 𝒫 𝑎 = 𝒫 suc 𝑏 )
16 15 fveq2d ⊢ ( 𝑎 = suc 𝑏 → ( card ‘ 𝒫 𝑎 ) = ( card ‘ 𝒫 suc 𝑏 ) )
17 fveq2 ⊢ ( 𝑎 = suc 𝑏 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ suc 𝑏 ) )
18 suceq ⊢ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ suc 𝑏 ) → suc ( 𝐹 ‘ 𝑎 ) = suc ( 𝐹 ‘ suc 𝑏 ) )
19 17 18 syl ⊢ ( 𝑎 = suc 𝑏 → suc ( 𝐹 ‘ 𝑎 ) = suc ( 𝐹 ‘ suc 𝑏 ) )
20 16 19 eqeq12d ⊢ ( 𝑎 = suc 𝑏 → ( ( card ‘ 𝒫 𝑎 ) = suc ( 𝐹 ‘ 𝑎 ) ↔ ( card ‘ 𝒫 suc 𝑏 ) = suc ( 𝐹 ‘ suc 𝑏 ) ) )
21 pweq ⊢ ( 𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴 )
22 21 fveq2d ⊢ ( 𝑎 = 𝐴 → ( card ‘ 𝒫 𝑎 ) = ( card ‘ 𝒫 𝐴 ) )
23 fveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝐴 ) )
24 suceq ⊢ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝐴 ) → suc ( 𝐹 ‘ 𝑎 ) = suc ( 𝐹 ‘ 𝐴 ) )
25 23 24 syl ⊢ ( 𝑎 = 𝐴 → suc ( 𝐹 ‘ 𝑎 ) = suc ( 𝐹 ‘ 𝐴 ) )
26 22 25 eqeq12d ⊢ ( 𝑎 = 𝐴 → ( ( card ‘ 𝒫 𝑎 ) = suc ( 𝐹 ‘ 𝑎 ) ↔ ( card ‘ 𝒫 𝐴 ) = suc ( 𝐹 ‘ 𝐴 ) ) )
27 df-1o ⊢ 1o = suc ∅
28 pw0 ⊢ 𝒫 ∅ = { ∅ }
29 28 fveq2i ⊢ ( card ‘ 𝒫 ∅ ) = ( card ‘ { ∅ } )
30 0ex ⊢ ∅ ∈ V
31 cardsn ⊢ ( ∅ ∈ V → ( card ‘ { ∅ } ) = 1o )
32 30 31 ax-mp ⊢ ( card ‘ { ∅ } ) = 1o
33 29 32 eqtri ⊢ ( card ‘ 𝒫 ∅ ) = 1o
34 1 ackbij1lem13 ⊢ ( 𝐹 ‘ ∅ ) = ∅
35 suceq ⊢ ( ( 𝐹 ‘ ∅ ) = ∅ → suc ( 𝐹 ‘ ∅ ) = suc ∅ )
36 34 35 ax-mp ⊢ suc ( 𝐹 ‘ ∅ ) = suc ∅
37 27 33 36 3eqtr4i ⊢ ( card ‘ 𝒫 ∅ ) = suc ( 𝐹 ‘ ∅ )
38 oveq2 ⊢ ( ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) → ( ( card ‘ 𝒫 𝑏 ) +o ( card ‘ 𝒫 𝑏 ) ) = ( ( card ‘ 𝒫 𝑏 ) +o suc ( 𝐹 ‘ 𝑏 ) ) )
39 38 adantl ⊢ ( ( 𝑏 ∈ ω ∧ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) → ( ( card ‘ 𝒫 𝑏 ) +o ( card ‘ 𝒫 𝑏 ) ) = ( ( card ‘ 𝒫 𝑏 ) +o suc ( 𝐹 ‘ 𝑏 ) ) )
40 ackbij1lem5 ⊢ ( 𝑏 ∈ ω → ( card ‘ 𝒫 suc 𝑏 ) = ( ( card ‘ 𝒫 𝑏 ) +o ( card ‘ 𝒫 𝑏 ) ) )
41 40 adantr ⊢ ( ( 𝑏 ∈ ω ∧ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) → ( card ‘ 𝒫 suc 𝑏 ) = ( ( card ‘ 𝒫 𝑏 ) +o ( card ‘ 𝒫 𝑏 ) ) )
42 df-suc ⊢ suc 𝑏 = ( 𝑏 ∪ { 𝑏 } )
43 42 equncomi ⊢ suc 𝑏 = ( { 𝑏 } ∪ 𝑏 )
44 43 fveq2i ⊢ ( 𝐹 ‘ suc 𝑏 ) = ( 𝐹 ‘ ( { 𝑏 } ∪ 𝑏 ) )
45 ackbij1lem4 ⊢ ( 𝑏 ∈ ω → { 𝑏 } ∈ ( 𝒫 ω ∩ Fin ) )
46 45 adantr ⊢ ( ( 𝑏 ∈ ω ∧ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) → { 𝑏 } ∈ ( 𝒫 ω ∩ Fin ) )
47 ackbij1lem3 ⊢ ( 𝑏 ∈ ω → 𝑏 ∈ ( 𝒫 ω ∩ Fin ) )
48 47 adantr ⊢ ( ( 𝑏 ∈ ω ∧ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) → 𝑏 ∈ ( 𝒫 ω ∩ Fin ) )
49 incom ⊢ ( { 𝑏 } ∩ 𝑏 ) = ( 𝑏 ∩ { 𝑏 } )
50 nnord ⊢ ( 𝑏 ∈ ω → Ord 𝑏 )
51 orddisj ⊢ ( Ord 𝑏 → ( 𝑏 ∩ { 𝑏 } ) = ∅ )
52 50 51 syl ⊢ ( 𝑏 ∈ ω → ( 𝑏 ∩ { 𝑏 } ) = ∅ )
53 49 52 eqtrid ⊢ ( 𝑏 ∈ ω → ( { 𝑏 } ∩ 𝑏 ) = ∅ )
54 53 adantr ⊢ ( ( 𝑏 ∈ ω ∧ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) → ( { 𝑏 } ∩ 𝑏 ) = ∅ )
55 1 ackbij1lem9 ⊢ ( ( { 𝑏 } ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( { 𝑏 } ∩ 𝑏 ) = ∅ ) → ( 𝐹 ‘ ( { 𝑏 } ∪ 𝑏 ) ) = ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ 𝑏 ) ) )
56 46 48 54 55 syl3anc ⊢ ( ( 𝑏 ∈ ω ∧ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) → ( 𝐹 ‘ ( { 𝑏 } ∪ 𝑏 ) ) = ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ 𝑏 ) ) )
57 1 ackbij1lem8 ⊢ ( 𝑏 ∈ ω → ( 𝐹 ‘ { 𝑏 } ) = ( card ‘ 𝒫 𝑏 ) )
58 57 adantr ⊢ ( ( 𝑏 ∈ ω ∧ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) → ( 𝐹 ‘ { 𝑏 } ) = ( card ‘ 𝒫 𝑏 ) )
59 58 oveq1d ⊢ ( ( 𝑏 ∈ ω ∧ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) → ( ( 𝐹 ‘ { 𝑏 } ) +o ( 𝐹 ‘ 𝑏 ) ) = ( ( card ‘ 𝒫 𝑏 ) +o ( 𝐹 ‘ 𝑏 ) ) )
60 56 59 eqtrd ⊢ ( ( 𝑏 ∈ ω ∧ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) → ( 𝐹 ‘ ( { 𝑏 } ∪ 𝑏 ) ) = ( ( card ‘ 𝒫 𝑏 ) +o ( 𝐹 ‘ 𝑏 ) ) )
61 44 60 eqtrid ⊢ ( ( 𝑏 ∈ ω ∧ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) → ( 𝐹 ‘ suc 𝑏 ) = ( ( card ‘ 𝒫 𝑏 ) +o ( 𝐹 ‘ 𝑏 ) ) )
62 suceq ⊢ ( ( 𝐹 ‘ suc 𝑏 ) = ( ( card ‘ 𝒫 𝑏 ) +o ( 𝐹 ‘ 𝑏 ) ) → suc ( 𝐹 ‘ suc 𝑏 ) = suc ( ( card ‘ 𝒫 𝑏 ) +o ( 𝐹 ‘ 𝑏 ) ) )
63 61 62 syl ⊢ ( ( 𝑏 ∈ ω ∧ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) → suc ( 𝐹 ‘ suc 𝑏 ) = suc ( ( card ‘ 𝒫 𝑏 ) +o ( 𝐹 ‘ 𝑏 ) ) )
64 nnfi ⊢ ( 𝑏 ∈ ω → 𝑏 ∈ Fin )
65 pwfi ⊢ ( 𝑏 ∈ Fin ↔ 𝒫 𝑏 ∈ Fin )
66 64 65 sylib ⊢ ( 𝑏 ∈ ω → 𝒫 𝑏 ∈ Fin )
67 66 adantr ⊢ ( ( 𝑏 ∈ ω ∧ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) → 𝒫 𝑏 ∈ Fin )
68 ficardom ⊢ ( 𝒫 𝑏 ∈ Fin → ( card ‘ 𝒫 𝑏 ) ∈ ω )
69 67 68 syl ⊢ ( ( 𝑏 ∈ ω ∧ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) → ( card ‘ 𝒫 𝑏 ) ∈ ω )
70 1 ackbij1lem10 ⊢ 𝐹 : ( 𝒫 ω ∩ Fin ) ⟶ ω
71 70 ffvelcdmi ⊢ ( 𝑏 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ 𝑏 ) ∈ ω )
72 48 71 syl ⊢ ( ( 𝑏 ∈ ω ∧ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ω )
73 nnasuc ⊢ ( ( ( card ‘ 𝒫 𝑏 ) ∈ ω ∧ ( 𝐹 ‘ 𝑏 ) ∈ ω ) → ( ( card ‘ 𝒫 𝑏 ) +o suc ( 𝐹 ‘ 𝑏 ) ) = suc ( ( card ‘ 𝒫 𝑏 ) +o ( 𝐹 ‘ 𝑏 ) ) )
74 69 72 73 syl2anc ⊢ ( ( 𝑏 ∈ ω ∧ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) → ( ( card ‘ 𝒫 𝑏 ) +o suc ( 𝐹 ‘ 𝑏 ) ) = suc ( ( card ‘ 𝒫 𝑏 ) +o ( 𝐹 ‘ 𝑏 ) ) )
75 63 74 eqtr4d ⊢ ( ( 𝑏 ∈ ω ∧ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) → suc ( 𝐹 ‘ suc 𝑏 ) = ( ( card ‘ 𝒫 𝑏 ) +o suc ( 𝐹 ‘ 𝑏 ) ) )
76 39 41 75 3eqtr4d ⊢ ( ( 𝑏 ∈ ω ∧ ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) ) → ( card ‘ 𝒫 suc 𝑏 ) = suc ( 𝐹 ‘ suc 𝑏 ) )
77 76 ex ⊢ ( 𝑏 ∈ ω → ( ( card ‘ 𝒫 𝑏 ) = suc ( 𝐹 ‘ 𝑏 ) → ( card ‘ 𝒫 suc 𝑏 ) = suc ( 𝐹 ‘ suc 𝑏 ) ) )
78 8 14 20 26 37 77 finds ⊢ ( 𝐴 ∈ ω → ( card ‘ 𝒫 𝐴 ) = suc ( 𝐹 ‘ 𝐴 ) )
79 2 78 eqtrd ⊢ ( 𝐴 ∈ ω → ( 𝐹 ‘ { 𝐴 } ) = suc ( 𝐹 ‘ 𝐴 ) )