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 ffvelrni ( 𝑏 ∈ ( 𝒫 ω ∩ 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 ( 𝐹𝐴 ) )