MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ackbij2lem2 Structured version   Visualization version   GIF version

Theorem ackbij2lem2 9661
Description: Lemma for ackbij2 9664. (Contributed by Stefan O'Rear, 18-Nov-2014.)
Hypotheses
Ref Expression
ackbij.f 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘ 𝑦𝑥 ({𝑦} × 𝒫 𝑦)))
ackbij.g 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥𝑦))))
Assertion
Ref Expression
ackbij2lem2 (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴):(𝑅1𝐴)–1-1-onto→(card‘(𝑅1𝐴)))
Distinct variable groups:   𝑥,𝐹,𝑦   𝑥,𝐺,𝑦   𝑥,𝐴,𝑦

Proof of Theorem ackbij2lem2
Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6669 . . 3 (𝑎 = ∅ → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘∅))
2 fveq2 6669 . . 3 (𝑎 = ∅ → (𝑅1𝑎) = (𝑅1‘∅))
3 2fveq3 6674 . . 3 (𝑎 = ∅ → (card‘(𝑅1𝑎)) = (card‘(𝑅1‘∅)))
41, 2, 3f1oeq123d 6609 . 2 (𝑎 = ∅ → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅))))
5 fveq2 6669 . . 3 (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏))
6 fveq2 6669 . . 3 (𝑎 = 𝑏 → (𝑅1𝑎) = (𝑅1𝑏))
7 2fveq3 6674 . . 3 (𝑎 = 𝑏 → (card‘(𝑅1𝑎)) = (card‘(𝑅1𝑏)))
85, 6, 7f1oeq123d 6609 . 2 (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))))
9 fveq2 6669 . . 3 (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘suc 𝑏))
10 fveq2 6669 . . 3 (𝑎 = suc 𝑏 → (𝑅1𝑎) = (𝑅1‘suc 𝑏))
11 2fveq3 6674 . . 3 (𝑎 = suc 𝑏 → (card‘(𝑅1𝑎)) = (card‘(𝑅1‘suc 𝑏)))
129, 10, 11f1oeq123d 6609 . 2 (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏))))
13 fveq2 6669 . . 3 (𝑎 = 𝐴 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝐴))
14 fveq2 6669 . . 3 (𝑎 = 𝐴 → (𝑅1𝑎) = (𝑅1𝐴))
15 2fveq3 6674 . . 3 (𝑎 = 𝐴 → (card‘(𝑅1𝑎)) = (card‘(𝑅1𝐴)))
1613, 14, 15f1oeq123d 6609 . 2 (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘𝐴):(𝑅1𝐴)–1-1-onto→(card‘(𝑅1𝐴))))
17 f1o0 6650 . . 3 ∅:∅–1-1-onto→∅
18 0ex 5210 . . . . . 6 ∅ ∈ V
1918rdg0 8056 . . . . 5 (rec(𝐺, ∅)‘∅) = ∅
20 f1oeq1 6603 . . . . 5 ((rec(𝐺, ∅)‘∅) = ∅ → ((rec(𝐺, ∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅)) ↔ ∅:(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅))))
2119, 20ax-mp 5 . . . 4 ((rec(𝐺, ∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅)) ↔ ∅:(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅)))
22 r10 9196 . . . . 5 (𝑅1‘∅) = ∅
2322fveq2i 6672 . . . . . 6 (card‘(𝑅1‘∅)) = (card‘∅)
24 card0 9386 . . . . . 6 (card‘∅) = ∅
2523, 24eqtri 2844 . . . . 5 (card‘(𝑅1‘∅)) = ∅
26 f1oeq23 6606 . . . . 5 (((𝑅1‘∅) = ∅ ∧ (card‘(𝑅1‘∅)) = ∅) → (∅:(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅)) ↔ ∅:∅–1-1-onto→∅))
2722, 25, 26mp2an 690 . . . 4 (∅:(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅)) ↔ ∅:∅–1-1-onto→∅)
2821, 27bitri 277 . . 3 ((rec(𝐺, ∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅)) ↔ ∅:∅–1-1-onto→∅)
2917, 28mpbir 233 . 2 (rec(𝐺, ∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅))
30 ackbij.f . . . . . . . . . 10 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘ 𝑦𝑥 ({𝑦} × 𝒫 𝑦)))
3130ackbij1lem17 9657 . . . . . . . . 9 𝐹:(𝒫 ω ∩ Fin)–1-1→ω
3231a1i 11 . . . . . . . 8 (𝑏 ∈ ω → 𝐹:(𝒫 ω ∩ Fin)–1-1→ω)
33 r1fin 9201 . . . . . . . . . 10 (𝑏 ∈ ω → (𝑅1𝑏) ∈ Fin)
34 ficardom 9389 . . . . . . . . . 10 ((𝑅1𝑏) ∈ Fin → (card‘(𝑅1𝑏)) ∈ ω)
3533, 34syl 17 . . . . . . . . 9 (𝑏 ∈ ω → (card‘(𝑅1𝑏)) ∈ ω)
36 ackbij2lem1 9640 . . . . . . . . 9 ((card‘(𝑅1𝑏)) ∈ ω → 𝒫 (card‘(𝑅1𝑏)) ⊆ (𝒫 ω ∩ Fin))
3735, 36syl 17 . . . . . . . 8 (𝑏 ∈ ω → 𝒫 (card‘(𝑅1𝑏)) ⊆ (𝒫 ω ∩ Fin))
38 f1ores 6628 . . . . . . . 8 ((𝐹:(𝒫 ω ∩ Fin)–1-1→ω ∧ 𝒫 (card‘(𝑅1𝑏)) ⊆ (𝒫 ω ∩ Fin)) → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(𝐹 “ 𝒫 (card‘(𝑅1𝑏))))
3932, 37, 38syl2anc 586 . . . . . . 7 (𝑏 ∈ ω → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(𝐹 “ 𝒫 (card‘(𝑅1𝑏))))
4030ackbij1b 9660 . . . . . . . . . 10 ((card‘(𝑅1𝑏)) ∈ ω → (𝐹 “ 𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (card‘(𝑅1𝑏))))
4135, 40syl 17 . . . . . . . . 9 (𝑏 ∈ ω → (𝐹 “ 𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (card‘(𝑅1𝑏))))
42 ficardid 9390 . . . . . . . . . 10 ((𝑅1𝑏) ∈ Fin → (card‘(𝑅1𝑏)) ≈ (𝑅1𝑏))
43 pwen 8689 . . . . . . . . . 10 ((card‘(𝑅1𝑏)) ≈ (𝑅1𝑏) → 𝒫 (card‘(𝑅1𝑏)) ≈ 𝒫 (𝑅1𝑏))
44 carden2b 9395 . . . . . . . . . 10 (𝒫 (card‘(𝑅1𝑏)) ≈ 𝒫 (𝑅1𝑏) → (card‘𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (𝑅1𝑏)))
4533, 42, 43, 444syl 19 . . . . . . . . 9 (𝑏 ∈ ω → (card‘𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (𝑅1𝑏)))
4641, 45eqtrd 2856 . . . . . . . 8 (𝑏 ∈ ω → (𝐹 “ 𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (𝑅1𝑏)))
4746f1oeq3d 6611 . . . . . . 7 (𝑏 ∈ ω → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(𝐹 “ 𝒫 (card‘(𝑅1𝑏))) ↔ (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(card‘𝒫 (𝑅1𝑏))))
4839, 47mpbid 234 . . . . . 6 (𝑏 ∈ ω → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(card‘𝒫 (𝑅1𝑏)))
4948adantr 483 . . . . 5 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(card‘𝒫 (𝑅1𝑏)))
50 f1opw 7400 . . . . . 6 ((rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏)) → (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫 (𝑅1𝑏)–1-1-onto→𝒫 (card‘(𝑅1𝑏)))
5150adantl 484 . . . . 5 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫 (𝑅1𝑏)–1-1-onto→𝒫 (card‘(𝑅1𝑏)))
52 f1oco 6636 . . . . 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𝑏)))
5349, 51, 52syl2anc 586 . . . 4 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):𝒫 (𝑅1𝑏)–1-1-onto→(card‘𝒫 (𝑅1𝑏)))
54 frsuc 8071 . . . . . . . . 9 (𝑏 ∈ ω → ((rec(𝐺, ∅) ↾ ω)‘suc 𝑏) = (𝐺‘((rec(𝐺, ∅) ↾ ω)‘𝑏)))
55 peano2 7601 . . . . . . . . . 10 (𝑏 ∈ ω → suc 𝑏 ∈ ω)
5655fvresd 6689 . . . . . . . . 9 (𝑏 ∈ ω → ((rec(𝐺, ∅) ↾ ω)‘suc 𝑏) = (rec(𝐺, ∅)‘suc 𝑏))
57 fvres 6688 . . . . . . . . . . 11 (𝑏 ∈ ω → ((rec(𝐺, ∅) ↾ ω)‘𝑏) = (rec(𝐺, ∅)‘𝑏))
5857fveq2d 6673 . . . . . . . . . 10 (𝑏 ∈ ω → (𝐺‘((rec(𝐺, ∅) ↾ ω)‘𝑏)) = (𝐺‘(rec(𝐺, ∅)‘𝑏)))
59 fvex 6682 . . . . . . . . . . 11 (rec(𝐺, ∅)‘𝑏) ∈ V
60 dmeq 5771 . . . . . . . . . . . . . 14 (𝑥 = (rec(𝐺, ∅)‘𝑏) → dom 𝑥 = dom (rec(𝐺, ∅)‘𝑏))
6160pweqd 4557 . . . . . . . . . . . . 13 (𝑥 = (rec(𝐺, ∅)‘𝑏) → 𝒫 dom 𝑥 = 𝒫 dom (rec(𝐺, ∅)‘𝑏))
62 imaeq1 5923 . . . . . . . . . . . . . 14 (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝑥𝑦) = ((rec(𝐺, ∅)‘𝑏) “ 𝑦))
6362fveq2d 6673 . . . . . . . . . . . . 13 (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝐹‘(𝑥𝑦)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))
6461, 63mpteq12dv 5150 . . . . . . . . . . . 12 (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
65 ackbij.g . . . . . . . . . . . 12 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥𝑦))))
6659dmex 7615 . . . . . . . . . . . . . 14 dom (rec(𝐺, ∅)‘𝑏) ∈ V
6766pwex 5280 . . . . . . . . . . . . 13 𝒫 dom (rec(𝐺, ∅)‘𝑏) ∈ V
6867mptex 6985 . . . . . . . . . . . 12 (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) ∈ V
6964, 65, 68fvmpt 6767 . . . . . . . . . . 11 ((rec(𝐺, ∅)‘𝑏) ∈ V → (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
7059, 69ax-mp 5 . . . . . . . . . 10 (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))
7158, 70syl6eq 2872 . . . . . . . . 9 (𝑏 ∈ ω → (𝐺‘((rec(𝐺, ∅) ↾ ω)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
7254, 56, 713eqtr3d 2864 . . . . . . . 8 (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
7372adantr 483 . . . . . . 7 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
74 f1odm 6618 . . . . . . . . . . 11 ((rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏)) → dom (rec(𝐺, ∅)‘𝑏) = (𝑅1𝑏))
7574adantl 484 . . . . . . . . . 10 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → dom (rec(𝐺, ∅)‘𝑏) = (𝑅1𝑏))
7675pweqd 4557 . . . . . . . . 9 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → 𝒫 dom (rec(𝐺, ∅)‘𝑏) = 𝒫 (𝑅1𝑏))
7776mpteq1d 5154 . . . . . . . 8 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
78 fvex 6682 . . . . . . . . . . 11 (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)) ∈ V
79 eqid 2821 . . . . . . . . . . 11 (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))
8078, 79fnmpti 6490 . . . . . . . . . 10 (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) Fn 𝒫 (𝑅1𝑏)
8180a1i 11 . . . . . . . . 9 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) Fn 𝒫 (𝑅1𝑏))
82 f1ofn 6615 . . . . . . . . . 10 (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):𝒫 (𝑅1𝑏)–1-1-onto→(card‘𝒫 (𝑅1𝑏)) → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))) Fn 𝒫 (𝑅1𝑏))
8353, 82syl 17 . . . . . . . . 9 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))) Fn 𝒫 (𝑅1𝑏))
84 f1of 6614 . . . . . . . . . . . . . 14 ((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫 (𝑅1𝑏)–1-1-onto→𝒫 (card‘(𝑅1𝑏)) → (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫 (𝑅1𝑏)⟶𝒫 (card‘(𝑅1𝑏)))
8551, 84syl 17 . . . . . . . . . . . . 13 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫 (𝑅1𝑏)⟶𝒫 (card‘(𝑅1𝑏)))
8685ffvelrnda 6850 . . . . . . . . . . . 12 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) ∈ 𝒫 (card‘(𝑅1𝑏)))
8786fvresd 6689 . . . . . . . . . . 11 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)))
88 imaeq2 5924 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → ((rec(𝐺, ∅)‘𝑏) “ 𝑎) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
89 eqid 2821 . . . . . . . . . . . . . 14 (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)) = (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))
9059imaex 7620 . . . . . . . . . . . . . 14 ((rec(𝐺, ∅)‘𝑏) “ 𝑐) ∈ V
9188, 89, 90fvmpt 6767 . . . . . . . . . . . . 13 (𝑐 ∈ 𝒫 (𝑅1𝑏) → ((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
9291adantl 484 . . . . . . . . . . . 12 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
9392fveq2d 6673 . . . . . . . . . . 11 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → (𝐹‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
9487, 93eqtrd 2856 . . . . . . . . . 10 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
95 fvco3 6759 . . . . . . . . . . 11 (((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫 (𝑅1𝑏)⟶𝒫 (card‘(𝑅1𝑏)) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)))
9685, 95sylan 582 . . . . . . . . . 10 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)))
97 imaeq2 5924 . . . . . . . . . . . . 13 (𝑦 = 𝑐 → ((rec(𝐺, ∅)‘𝑏) “ 𝑦) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
9897fveq2d 6673 . . . . . . . . . . . 12 (𝑦 = 𝑐 → (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
99 fvex 6682 . . . . . . . . . . . 12 (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)) ∈ V
10098, 79, 99fvmpt 6767 . . . . . . . . . . 11 (𝑐 ∈ 𝒫 (𝑅1𝑏) → ((𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
101100adantl 484 . . . . . . . . . 10 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
10294, 96, 1013eqtr4rd 2867 . . . . . . . . 9 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐))
10381, 83, 102eqfnfvd 6804 . . . . . . . 8 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))))
10477, 103eqtrd 2856 . . . . . . 7 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))))
10573, 104eqtrd 2856 . . . . . 6 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))))
106 f1oeq1 6603 . . . . . 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 𝑏))))
107105, 106syl 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 7585 . . . . . . . 8 (𝑏 ∈ ω → 𝑏 ∈ On)
109 r1suc 9198 . . . . . . . 8 (𝑏 ∈ On → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1𝑏))
110108, 109syl 17 . . . . . . 7 (𝑏 ∈ ω → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1𝑏))
111110fveq2d 6673 . . . . . . 7 (𝑏 ∈ ω → (card‘(𝑅1‘suc 𝑏)) = (card‘𝒫 (𝑅1𝑏)))
112 f1oeq23 6606 . . . . . . 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𝑏))))
113110, 111, 112syl2anc 586 . . . . . 6 (𝑏 ∈ ω → (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)) ↔ ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):𝒫 (𝑅1𝑏)–1-1-onto→(card‘𝒫 (𝑅1𝑏))))
114113adantr 483 . . . . 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𝑏))))
115107, 114bitrd 281 . . . 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𝑏))))
11653, 115mpbird 259 . . 3 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)))
117116ex 415 . 2 (𝑏 ∈ ω → ((rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏)) → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏))))
1184, 8, 12, 16, 29, 117finds 7607 1 (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴):(𝑅1𝐴)–1-1-onto→(card‘(𝑅1𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398   = wceq 1533  wcel 2110  Vcvv 3494  cin 3934  wss 3935  c0 4290  𝒫 cpw 4538  {csn 4566   ciun 4918   class class class wbr 5065  cmpt 5145   × cxp 5552  dom cdm 5554  cres 5556  cima 5557  ccom 5558  Oncon0 6190  suc csuc 6192   Fn wfn 6349  wf 6350  1-1wf1 6351  1-1-ontowf1o 6353  cfv 6354  ωcom 7579  reccrdg 8044  cen 8505  Fincfn 8508  𝑅1cr1 9190  cardccrd 9363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5189  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4838  df-int 4876  df-iun 4920  df-br 5066  df-opab 5128  df-mpt 5146  df-tr 5172  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-ov 7158  df-oprab 7159  df-mpo 7160  df-om 7580  df-1st 7688  df-2nd 7689  df-wrecs 7946  df-recs 8007  df-rdg 8045  df-1o 8101  df-2o 8102  df-oadd 8105  df-er 8288  df-map 8407  df-en 8509  df-dom 8510  df-sdom 8511  df-fin 8512  df-r1 9192  df-dju 9329  df-card 9367
This theorem is referenced by:  ackbij2lem3  9662  ackbij2  9664
  Copyright terms: Public domain W3C validator