Step | Hyp | Ref
| Expression |
1 | | fveq2 6674 |
. . 3
⊢ (𝑎 = ∅ → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘∅)) |
2 | | fveq2 6674 |
. . 3
⊢ (𝑎 = ∅ →
(𝑅1‘𝑎) =
(𝑅1‘∅)) |
3 | | 2fveq3 6679 |
. . 3
⊢ (𝑎 = ∅ →
(card‘(𝑅1‘𝑎)) =
(card‘(𝑅1‘∅))) |
4 | 1, 2, 3 | f1oeq123d 6612 |
. 2
⊢ (𝑎 = ∅ → ((rec(𝐺, ∅)‘𝑎):(𝑅1‘𝑎)–1-1-onto→(card‘(𝑅1‘𝑎)) ↔ (rec(𝐺,
∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅)))) |
5 | | fveq2 6674 |
. . 3
⊢ (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏)) |
6 | | fveq2 6674 |
. . 3
⊢ (𝑎 = 𝑏 → (𝑅1‘𝑎) =
(𝑅1‘𝑏)) |
7 | | 2fveq3 6679 |
. . 3
⊢ (𝑎 = 𝑏 →
(card‘(𝑅1‘𝑎)) =
(card‘(𝑅1‘𝑏))) |
8 | 5, 6, 7 | f1oeq123d 6612 |
. 2
⊢ (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘𝑎):(𝑅1‘𝑎)–1-1-onto→(card‘(𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏)))) |
9 | | fveq2 6674 |
. . 3
⊢ (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘suc 𝑏)) |
10 | | fveq2 6674 |
. . 3
⊢ (𝑎 = suc 𝑏 → (𝑅1‘𝑎) =
(𝑅1‘suc 𝑏)) |
11 | | 2fveq3 6679 |
. . 3
⊢ (𝑎 = suc 𝑏 →
(card‘(𝑅1‘𝑎)) =
(card‘(𝑅1‘suc 𝑏))) |
12 | 9, 10, 11 | f1oeq123d 6612 |
. 2
⊢ (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘𝑎):(𝑅1‘𝑎)–1-1-onto→(card‘(𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
𝑏)))) |
13 | | fveq2 6674 |
. . 3
⊢ (𝑎 = 𝐴 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝐴)) |
14 | | fveq2 6674 |
. . 3
⊢ (𝑎 = 𝐴 → (𝑅1‘𝑎) =
(𝑅1‘𝐴)) |
15 | | 2fveq3 6679 |
. . 3
⊢ (𝑎 = 𝐴 →
(card‘(𝑅1‘𝑎)) =
(card‘(𝑅1‘𝐴))) |
16 | 13, 14, 15 | f1oeq123d 6612 |
. 2
⊢ (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘𝑎):(𝑅1‘𝑎)–1-1-onto→(card‘(𝑅1‘𝑎)) ↔ (rec(𝐺, ∅)‘𝐴):(𝑅1‘𝐴)–1-1-onto→(card‘(𝑅1‘𝐴)))) |
17 | | f1o0 6654 |
. . 3
⊢
∅:∅–1-1-onto→∅ |
18 | | 0ex 5175 |
. . . . . 6
⊢ ∅
∈ V |
19 | 18 | rdg0 8086 |
. . . . 5
⊢
(rec(𝐺,
∅)‘∅) = ∅ |
20 | | f1oeq1 6606 |
. . . . 5
⊢
((rec(𝐺,
∅)‘∅) = ∅ → ((rec(𝐺,
∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅))
↔ ∅:(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅)))) |
21 | 19, 20 | ax-mp 5 |
. . . 4
⊢
((rec(𝐺,
∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅))
↔ ∅:(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅))) |
22 | | r10 9270 |
. . . . 5
⊢
(𝑅1‘∅) = ∅ |
23 | 22 | fveq2i 6677 |
. . . . . 6
⊢
(card‘(𝑅1‘∅)) =
(card‘∅) |
24 | | card0 9460 |
. . . . . 6
⊢
(card‘∅) = ∅ |
25 | 23, 24 | eqtri 2761 |
. . . . 5
⊢
(card‘(𝑅1‘∅)) =
∅ |
26 | | f1oeq23 6609 |
. . . . 5
⊢
(((𝑅1‘∅) = ∅ ∧
(card‘(𝑅1‘∅)) = ∅) →
(∅:(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅))
↔ ∅:∅–1-1-onto→∅)) |
27 | 22, 25, 26 | mp2an 692 |
. . . 4
⊢
(∅:(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅))
↔ ∅:∅–1-1-onto→∅) |
28 | 21, 27 | bitri 278 |
. . 3
⊢
((rec(𝐺,
∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅))
↔ ∅:∅–1-1-onto→∅) |
29 | 17, 28 | mpbir 234 |
. 2
⊢
(rec(𝐺,
∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅)) |
30 | | ackbij.f |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) |
31 | 30 | ackbij1lem17 9736 |
. . . . . . . . 9
⊢ 𝐹:(𝒫 ω ∩
Fin)–1-1→ω |
32 | 31 | a1i 11 |
. . . . . . . 8
⊢ (𝑏 ∈ ω → 𝐹:(𝒫 ω ∩
Fin)–1-1→ω) |
33 | | r1fin 9275 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ω →
(𝑅1‘𝑏) ∈ Fin) |
34 | | ficardom 9463 |
. . . . . . . . . 10
⊢
((𝑅1‘𝑏) ∈ Fin →
(card‘(𝑅1‘𝑏)) ∈ ω) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ (𝑏 ∈ ω →
(card‘(𝑅1‘𝑏)) ∈ ω) |
36 | | ackbij2lem1 9719 |
. . . . . . . . 9
⊢
((card‘(𝑅1‘𝑏)) ∈ ω → 𝒫
(card‘(𝑅1‘𝑏)) ⊆ (𝒫 ω ∩
Fin)) |
37 | 35, 36 | syl 17 |
. . . . . . . 8
⊢ (𝑏 ∈ ω → 𝒫
(card‘(𝑅1‘𝑏)) ⊆ (𝒫 ω ∩
Fin)) |
38 | | f1ores 6632 |
. . . . . . . 8
⊢ ((𝐹:(𝒫 ω ∩
Fin)–1-1→ω ∧
𝒫 (card‘(𝑅1‘𝑏)) ⊆ (𝒫 ω ∩ Fin))
→ (𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))):𝒫
(card‘(𝑅1‘𝑏))–1-1-onto→(𝐹 “ 𝒫
(card‘(𝑅1‘𝑏)))) |
39 | 32, 37, 38 | syl2anc 587 |
. . . . . . 7
⊢ (𝑏 ∈ ω → (𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))):𝒫
(card‘(𝑅1‘𝑏))–1-1-onto→(𝐹 “ 𝒫
(card‘(𝑅1‘𝑏)))) |
40 | 30 | ackbij1b 9739 |
. . . . . . . . . 10
⊢
((card‘(𝑅1‘𝑏)) ∈ ω → (𝐹 “ 𝒫
(card‘(𝑅1‘𝑏))) = (card‘𝒫
(card‘(𝑅1‘𝑏)))) |
41 | 35, 40 | syl 17 |
. . . . . . . . 9
⊢ (𝑏 ∈ ω → (𝐹 “ 𝒫
(card‘(𝑅1‘𝑏))) = (card‘𝒫
(card‘(𝑅1‘𝑏)))) |
42 | | ficardid 9464 |
. . . . . . . . . 10
⊢
((𝑅1‘𝑏) ∈ Fin →
(card‘(𝑅1‘𝑏)) ≈ (𝑅1‘𝑏)) |
43 | | pwen 8740 |
. . . . . . . . . 10
⊢
((card‘(𝑅1‘𝑏)) ≈ (𝑅1‘𝑏) → 𝒫
(card‘(𝑅1‘𝑏)) ≈ 𝒫
(𝑅1‘𝑏)) |
44 | | carden2b 9469 |
. . . . . . . . . 10
⊢
(𝒫 (card‘(𝑅1‘𝑏)) ≈ 𝒫
(𝑅1‘𝑏) → (card‘𝒫
(card‘(𝑅1‘𝑏))) = (card‘𝒫
(𝑅1‘𝑏))) |
45 | 33, 42, 43, 44 | 4syl 19 |
. . . . . . . . 9
⊢ (𝑏 ∈ ω →
(card‘𝒫 (card‘(𝑅1‘𝑏))) = (card‘𝒫
(𝑅1‘𝑏))) |
46 | 41, 45 | eqtrd 2773 |
. . . . . . . 8
⊢ (𝑏 ∈ ω → (𝐹 “ 𝒫
(card‘(𝑅1‘𝑏))) = (card‘𝒫
(𝑅1‘𝑏))) |
47 | 46 | f1oeq3d 6615 |
. . . . . . 7
⊢ (𝑏 ∈ ω → ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))):𝒫
(card‘(𝑅1‘𝑏))–1-1-onto→(𝐹 “ 𝒫
(card‘(𝑅1‘𝑏))) ↔ (𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))):𝒫
(card‘(𝑅1‘𝑏))–1-1-onto→(card‘𝒫
(𝑅1‘𝑏)))) |
48 | 39, 47 | mpbid 235 |
. . . . . 6
⊢ (𝑏 ∈ ω → (𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))):𝒫
(card‘(𝑅1‘𝑏))–1-1-onto→(card‘𝒫
(𝑅1‘𝑏))) |
49 | 48 | adantr 484 |
. . . . 5
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) → (𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))):𝒫
(card‘(𝑅1‘𝑏))–1-1-onto→(card‘𝒫
(𝑅1‘𝑏))) |
50 | | f1opw 7417 |
. . . . . 6
⊢
((rec(𝐺,
∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏)) → (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫
(𝑅1‘𝑏)–1-1-onto→𝒫
(card‘(𝑅1‘𝑏))) |
51 | 50 | adantl 485 |
. . . . 5
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) → (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫
(𝑅1‘𝑏)–1-1-onto→𝒫
(card‘(𝑅1‘𝑏))) |
52 | | f1oco 6640 |
. . . . 5
⊢ (((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))):𝒫
(card‘(𝑅1‘𝑏))–1-1-onto→(card‘𝒫
(𝑅1‘𝑏)) ∧ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫
(𝑅1‘𝑏)–1-1-onto→𝒫
(card‘(𝑅1‘𝑏))) → ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):𝒫
(𝑅1‘𝑏)–1-1-onto→(card‘𝒫
(𝑅1‘𝑏))) |
53 | 49, 51, 52 | syl2anc 587 |
. . . 4
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) → ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):𝒫
(𝑅1‘𝑏)–1-1-onto→(card‘𝒫
(𝑅1‘𝑏))) |
54 | | frsuc 8101 |
. . . . . . . . 9
⊢ (𝑏 ∈ ω →
((rec(𝐺, ∅) ↾
ω)‘suc 𝑏) =
(𝐺‘((rec(𝐺, ∅) ↾
ω)‘𝑏))) |
55 | | peano2 7621 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ω → suc 𝑏 ∈
ω) |
56 | 55 | fvresd 6694 |
. . . . . . . . 9
⊢ (𝑏 ∈ ω →
((rec(𝐺, ∅) ↾
ω)‘suc 𝑏) =
(rec(𝐺, ∅)‘suc
𝑏)) |
57 | | fvres 6693 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ω →
((rec(𝐺, ∅) ↾
ω)‘𝑏) =
(rec(𝐺,
∅)‘𝑏)) |
58 | 57 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ω → (𝐺‘((rec(𝐺, ∅) ↾ ω)‘𝑏)) = (𝐺‘(rec(𝐺, ∅)‘𝑏))) |
59 | | fvex 6687 |
. . . . . . . . . . 11
⊢
(rec(𝐺,
∅)‘𝑏) ∈
V |
60 | | dmeq 5746 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (rec(𝐺, ∅)‘𝑏) → dom 𝑥 = dom (rec(𝐺, ∅)‘𝑏)) |
61 | 60 | pweqd 4507 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (rec(𝐺, ∅)‘𝑏) → 𝒫 dom 𝑥 = 𝒫 dom (rec(𝐺, ∅)‘𝑏)) |
62 | | imaeq1 5898 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝑥 “ 𝑦) = ((rec(𝐺, ∅)‘𝑏) “ 𝑦)) |
63 | 62 | fveq2d 6678 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝐹‘(𝑥 “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) |
64 | 61, 63 | mpteq12dv 5115 |
. . . . . . . . . . . 12
⊢ (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))) |
65 | | ackbij.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦)))) |
66 | 59 | dmex 7642 |
. . . . . . . . . . . . . 14
⊢ dom
(rec(𝐺,
∅)‘𝑏) ∈
V |
67 | 66 | pwex 5247 |
. . . . . . . . . . . . 13
⊢ 𝒫
dom (rec(𝐺,
∅)‘𝑏) ∈
V |
68 | 67 | mptex 6996 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) ∈ V |
69 | 64, 65, 68 | fvmpt 6775 |
. . . . . . . . . . 11
⊢
((rec(𝐺,
∅)‘𝑏) ∈ V
→ (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))) |
70 | 59, 69 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) |
71 | 58, 70 | eqtrdi 2789 |
. . . . . . . . 9
⊢ (𝑏 ∈ ω → (𝐺‘((rec(𝐺, ∅) ↾ ω)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))) |
72 | 54, 56, 71 | 3eqtr3d 2781 |
. . . . . . . 8
⊢ (𝑏 ∈ ω →
(rec(𝐺, ∅)‘suc
𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))) |
73 | 72 | adantr 484 |
. . . . . . 7
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))) |
74 | | f1odm 6622 |
. . . . . . . . . . 11
⊢
((rec(𝐺,
∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏)) → dom (rec(𝐺, ∅)‘𝑏) =
(𝑅1‘𝑏)) |
75 | 74 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) → dom (rec(𝐺, ∅)‘𝑏) =
(𝑅1‘𝑏)) |
76 | 75 | pweqd 4507 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) → 𝒫 dom
(rec(𝐺,
∅)‘𝑏) =
𝒫 (𝑅1‘𝑏)) |
77 | 76 | mpteq1d 5119 |
. . . . . . . 8
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) → (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫
(𝑅1‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))) |
78 | | fvex 6687 |
. . . . . . . . . . 11
⊢ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)) ∈ V |
79 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝒫
(𝑅1‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫
(𝑅1‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) |
80 | 78, 79 | fnmpti 6480 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝒫
(𝑅1‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) Fn 𝒫
(𝑅1‘𝑏) |
81 | 80 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) → (𝑦 ∈ 𝒫
(𝑅1‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) Fn 𝒫
(𝑅1‘𝑏)) |
82 | | f1ofn 6619 |
. . . . . . . . . 10
⊢ (((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):𝒫
(𝑅1‘𝑏)–1-1-onto→(card‘𝒫
(𝑅1‘𝑏)) → ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))) Fn 𝒫
(𝑅1‘𝑏)) |
83 | 53, 82 | syl 17 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) → ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))) Fn 𝒫
(𝑅1‘𝑏)) |
84 | | f1of 6618 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫
(𝑅1‘𝑏)–1-1-onto→𝒫
(card‘(𝑅1‘𝑏)) → (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫
(𝑅1‘𝑏)⟶𝒫
(card‘(𝑅1‘𝑏))) |
85 | 51, 84 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) → (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫
(𝑅1‘𝑏)⟶𝒫
(card‘(𝑅1‘𝑏))) |
86 | 85 | ffvelrnda 6861 |
. . . . . . . . . . . 12
⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) ∧ 𝑐 ∈ 𝒫
(𝑅1‘𝑏)) → ((𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) ∈ 𝒫
(card‘(𝑅1‘𝑏))) |
87 | 86 | fvresd 6694 |
. . . . . . . . . . 11
⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) ∧ 𝑐 ∈ 𝒫
(𝑅1‘𝑏)) → ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏)))‘((𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐))) |
88 | | imaeq2 5899 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑐 → ((rec(𝐺, ∅)‘𝑏) “ 𝑎) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐)) |
89 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)) = (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)) |
90 | 59 | imaex 7647 |
. . . . . . . . . . . . . 14
⊢
((rec(𝐺,
∅)‘𝑏) “
𝑐) ∈
V |
91 | 88, 89, 90 | fvmpt 6775 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ 𝒫
(𝑅1‘𝑏) → ((𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐)) |
92 | 91 | adantl 485 |
. . . . . . . . . . . 12
⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) ∧ 𝑐 ∈ 𝒫
(𝑅1‘𝑏)) → ((𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐)) |
93 | 92 | fveq2d 6678 |
. . . . . . . . . . 11
⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) ∧ 𝑐 ∈ 𝒫
(𝑅1‘𝑏)) → (𝐹‘((𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐))) |
94 | 87, 93 | eqtrd 2773 |
. . . . . . . . . 10
⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) ∧ 𝑐 ∈ 𝒫
(𝑅1‘𝑏)) → ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏)))‘((𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐))) |
95 | | fvco3 6767 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫
(𝑅1‘𝑏)⟶𝒫
(card‘(𝑅1‘𝑏)) ∧ 𝑐 ∈ 𝒫
(𝑅1‘𝑏)) → (((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐) = ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏)))‘((𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐))) |
96 | 85, 95 | sylan 583 |
. . . . . . . . . 10
⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) ∧ 𝑐 ∈ 𝒫
(𝑅1‘𝑏)) → (((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐) = ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏)))‘((𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐))) |
97 | | imaeq2 5899 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑐 → ((rec(𝐺, ∅)‘𝑏) “ 𝑦) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐)) |
98 | 97 | fveq2d 6678 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑐 → (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐))) |
99 | | fvex 6687 |
. . . . . . . . . . . 12
⊢ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)) ∈ V |
100 | 98, 79, 99 | fvmpt 6775 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ 𝒫
(𝑅1‘𝑏) → ((𝑦 ∈ 𝒫
(𝑅1‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐))) |
101 | 100 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) ∧ 𝑐 ∈ 𝒫
(𝑅1‘𝑏)) → ((𝑦 ∈ 𝒫
(𝑅1‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐))) |
102 | 94, 96, 101 | 3eqtr4rd 2784 |
. . . . . . . . 9
⊢ (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) ∧ 𝑐 ∈ 𝒫
(𝑅1‘𝑏)) → ((𝑦 ∈ 𝒫
(𝑅1‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐)) |
103 | 81, 83, 102 | eqfnfvd 6812 |
. . . . . . . 8
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) → (𝑦 ∈ 𝒫
(𝑅1‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))) |
104 | 77, 103 | eqtrd 2773 |
. . . . . . 7
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) → (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))) |
105 | 73, 104 | eqtrd 2773 |
. . . . . 6
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) = ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))) |
106 | | f1oeq1 6606 |
. . . . . 6
⊢
((rec(𝐺,
∅)‘suc 𝑏) =
((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))) → ((rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
𝑏)) ↔ ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
𝑏)))) |
107 | 105, 106 | syl 17 |
. . . . 5
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) → ((rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
𝑏)) ↔ ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
𝑏)))) |
108 | | nnon 7605 |
. . . . . . . 8
⊢ (𝑏 ∈ ω → 𝑏 ∈ On) |
109 | | r1suc 9272 |
. . . . . . . 8
⊢ (𝑏 ∈ On →
(𝑅1‘suc 𝑏) = 𝒫
(𝑅1‘𝑏)) |
110 | 108, 109 | syl 17 |
. . . . . . 7
⊢ (𝑏 ∈ ω →
(𝑅1‘suc 𝑏) = 𝒫
(𝑅1‘𝑏)) |
111 | 110 | fveq2d 6678 |
. . . . . . 7
⊢ (𝑏 ∈ ω →
(card‘(𝑅1‘suc 𝑏)) = (card‘𝒫
(𝑅1‘𝑏))) |
112 | | f1oeq23 6609 |
. . . . . . 7
⊢
(((𝑅1‘suc 𝑏) = 𝒫
(𝑅1‘𝑏) ∧
(card‘(𝑅1‘suc 𝑏)) = (card‘𝒫
(𝑅1‘𝑏))) → (((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
𝑏)) ↔ ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):𝒫
(𝑅1‘𝑏)–1-1-onto→(card‘𝒫
(𝑅1‘𝑏)))) |
113 | 110, 111,
112 | syl2anc 587 |
. . . . . 6
⊢ (𝑏 ∈ ω → (((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
𝑏)) ↔ ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):𝒫
(𝑅1‘𝑏)–1-1-onto→(card‘𝒫
(𝑅1‘𝑏)))) |
114 | 113 | adantr 484 |
. . . . 5
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) → (((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
𝑏)) ↔ ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):𝒫
(𝑅1‘𝑏)–1-1-onto→(card‘𝒫
(𝑅1‘𝑏)))) |
115 | 107, 114 | bitrd 282 |
. . . 4
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) → ((rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
𝑏)) ↔ ((𝐹 ↾ 𝒫
(card‘(𝑅1‘𝑏))) ∘ (𝑎 ∈ 𝒫
(𝑅1‘𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):𝒫
(𝑅1‘𝑏)–1-1-onto→(card‘𝒫
(𝑅1‘𝑏)))) |
116 | 53, 115 | mpbird 260 |
. . 3
⊢ ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏))) → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
𝑏))) |
117 | 116 | ex 416 |
. 2
⊢ (𝑏 ∈ ω →
((rec(𝐺,
∅)‘𝑏):(𝑅1‘𝑏)–1-1-onto→(card‘(𝑅1‘𝑏)) → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
𝑏)))) |
118 | 4, 8, 12, 16, 29, 117 | finds 7629 |
1
⊢ (𝐴 ∈ ω →
(rec(𝐺,
∅)‘𝐴):(𝑅1‘𝐴)–1-1-onto→(card‘(𝑅1‘𝐴))) |