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

Theorem ackbij2lem2 9225
Description: Lemma for ackbij2 9228. (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 6340 . . 3 (𝑎 = ∅ → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘∅))
2 fveq2 6340 . . 3 (𝑎 = ∅ → (𝑅1𝑎) = (𝑅1‘∅))
32fveq2d 6344 . . 3 (𝑎 = ∅ → (card‘(𝑅1𝑎)) = (card‘(𝑅1‘∅)))
41, 2, 3f1oeq123d 6282 . 2 (𝑎 = ∅ → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅))))
5 fveq2 6340 . . 3 (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏))
6 fveq2 6340 . . 3 (𝑎 = 𝑏 → (𝑅1𝑎) = (𝑅1𝑏))
76fveq2d 6344 . . 3 (𝑎 = 𝑏 → (card‘(𝑅1𝑎)) = (card‘(𝑅1𝑏)))
85, 6, 7f1oeq123d 6282 . 2 (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))))
9 fveq2 6340 . . 3 (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘suc 𝑏))
10 fveq2 6340 . . 3 (𝑎 = suc 𝑏 → (𝑅1𝑎) = (𝑅1‘suc 𝑏))
1110fveq2d 6344 . . 3 (𝑎 = suc 𝑏 → (card‘(𝑅1𝑎)) = (card‘(𝑅1‘suc 𝑏)))
129, 10, 11f1oeq123d 6282 . 2 (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏))))
13 fveq2 6340 . . 3 (𝑎 = 𝐴 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝐴))
14 fveq2 6340 . . 3 (𝑎 = 𝐴 → (𝑅1𝑎) = (𝑅1𝐴))
1514fveq2d 6344 . . 3 (𝑎 = 𝐴 → (card‘(𝑅1𝑎)) = (card‘(𝑅1𝐴)))
1613, 14, 15f1oeq123d 6282 . 2 (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘𝐴):(𝑅1𝐴)–1-1-onto→(card‘(𝑅1𝐴))))
17 f1o0 6322 . . 3 ∅:∅–1-1-onto→∅
18 0ex 4930 . . . . . 6 ∅ ∈ V
1918rdg0 7674 . . . . 5 (rec(𝐺, ∅)‘∅) = ∅
20 f1oeq1 6276 . . . . 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 8792 . . . . 5 (𝑅1‘∅) = ∅
2322fveq2i 6343 . . . . . 6 (card‘(𝑅1‘∅)) = (card‘∅)
24 card0 8945 . . . . . 6 (card‘∅) = ∅
2523, 24eqtri 2770 . . . . 5 (card‘(𝑅1‘∅)) = ∅
26 f1oeq23 6279 . . . . 5 (((𝑅1‘∅) = ∅ ∧ (card‘(𝑅1‘∅)) = ∅) → (∅:(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅)) ↔ ∅:∅–1-1-onto→∅))
2722, 25, 26mp2an 710 . . . 4 (∅:(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅)) ↔ ∅:∅–1-1-onto→∅)
2821, 27bitri 264 . . 3 ((rec(𝐺, ∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅)) ↔ ∅:∅–1-1-onto→∅)
2917, 28mpbir 221 . 2 (rec(𝐺, ∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅))
30 ackbij.f . . . . . . . . . 10 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘ 𝑦𝑥 ({𝑦} × 𝒫 𝑦)))
3130ackbij1lem17 9221 . . . . . . . . 9 𝐹:(𝒫 ω ∩ Fin)–1-1→ω
3231a1i 11 . . . . . . . 8 (𝑏 ∈ ω → 𝐹:(𝒫 ω ∩ Fin)–1-1→ω)
33 r1fin 8797 . . . . . . . . . 10 (𝑏 ∈ ω → (𝑅1𝑏) ∈ Fin)
34 ficardom 8948 . . . . . . . . . 10 ((𝑅1𝑏) ∈ Fin → (card‘(𝑅1𝑏)) ∈ ω)
3533, 34syl 17 . . . . . . . . 9 (𝑏 ∈ ω → (card‘(𝑅1𝑏)) ∈ ω)
36 ackbij2lem1 9204 . . . . . . . . 9 ((card‘(𝑅1𝑏)) ∈ ω → 𝒫 (card‘(𝑅1𝑏)) ⊆ (𝒫 ω ∩ Fin))
3735, 36syl 17 . . . . . . . 8 (𝑏 ∈ ω → 𝒫 (card‘(𝑅1𝑏)) ⊆ (𝒫 ω ∩ Fin))
38 f1ores 6300 . . . . . . . 8 ((𝐹:(𝒫 ω ∩ Fin)–1-1→ω ∧ 𝒫 (card‘(𝑅1𝑏)) ⊆ (𝒫 ω ∩ Fin)) → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(𝐹 “ 𝒫 (card‘(𝑅1𝑏))))
3932, 37, 38syl2anc 696 . . . . . . 7 (𝑏 ∈ ω → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(𝐹 “ 𝒫 (card‘(𝑅1𝑏))))
4030ackbij1b 9224 . . . . . . . . . 10 ((card‘(𝑅1𝑏)) ∈ ω → (𝐹 “ 𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (card‘(𝑅1𝑏))))
4135, 40syl 17 . . . . . . . . 9 (𝑏 ∈ ω → (𝐹 “ 𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (card‘(𝑅1𝑏))))
42 ficardid 8949 . . . . . . . . . 10 ((𝑅1𝑏) ∈ Fin → (card‘(𝑅1𝑏)) ≈ (𝑅1𝑏))
43 pwen 8286 . . . . . . . . . 10 ((card‘(𝑅1𝑏)) ≈ (𝑅1𝑏) → 𝒫 (card‘(𝑅1𝑏)) ≈ 𝒫 (𝑅1𝑏))
44 carden2b 8954 . . . . . . . . . 10 (𝒫 (card‘(𝑅1𝑏)) ≈ 𝒫 (𝑅1𝑏) → (card‘𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (𝑅1𝑏)))
4533, 42, 43, 444syl 19 . . . . . . . . 9 (𝑏 ∈ ω → (card‘𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (𝑅1𝑏)))
4641, 45eqtrd 2782 . . . . . . . 8 (𝑏 ∈ ω → (𝐹 “ 𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (𝑅1𝑏)))
4746f1oeq3d 6283 . . . . . . 7 (𝑏 ∈ ω → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(𝐹 “ 𝒫 (card‘(𝑅1𝑏))) ↔ (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(card‘𝒫 (𝑅1𝑏))))
4839, 47mpbid 222 . . . . . 6 (𝑏 ∈ ω → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(card‘𝒫 (𝑅1𝑏)))
4948adantr 472 . . . . 5 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(card‘𝒫 (𝑅1𝑏)))
50 f1opw 7042 . . . . . 6 ((rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏)) → (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫 (𝑅1𝑏)–1-1-onto→𝒫 (card‘(𝑅1𝑏)))
5150adantl 473 . . . . 5 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫 (𝑅1𝑏)–1-1-onto→𝒫 (card‘(𝑅1𝑏)))
52 f1oco 6308 . . . . 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 696 . . . 4 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):𝒫 (𝑅1𝑏)–1-1-onto→(card‘𝒫 (𝑅1𝑏)))
54 frsuc 7689 . . . . . . . . 9 (𝑏 ∈ ω → ((rec(𝐺, ∅) ↾ ω)‘suc 𝑏) = (𝐺‘((rec(𝐺, ∅) ↾ ω)‘𝑏)))
55 peano2 7239 . . . . . . . . . 10 (𝑏 ∈ ω → suc 𝑏 ∈ ω)
5655fvresd 6357 . . . . . . . . 9 (𝑏 ∈ ω → ((rec(𝐺, ∅) ↾ ω)‘suc 𝑏) = (rec(𝐺, ∅)‘suc 𝑏))
57 fvres 6356 . . . . . . . . . . 11 (𝑏 ∈ ω → ((rec(𝐺, ∅) ↾ ω)‘𝑏) = (rec(𝐺, ∅)‘𝑏))
5857fveq2d 6344 . . . . . . . . . 10 (𝑏 ∈ ω → (𝐺‘((rec(𝐺, ∅) ↾ ω)‘𝑏)) = (𝐺‘(rec(𝐺, ∅)‘𝑏)))
59 fvex 6350 . . . . . . . . . . 11 (rec(𝐺, ∅)‘𝑏) ∈ V
60 dmeq 5467 . . . . . . . . . . . . . 14 (𝑥 = (rec(𝐺, ∅)‘𝑏) → dom 𝑥 = dom (rec(𝐺, ∅)‘𝑏))
6160pweqd 4295 . . . . . . . . . . . . 13 (𝑥 = (rec(𝐺, ∅)‘𝑏) → 𝒫 dom 𝑥 = 𝒫 dom (rec(𝐺, ∅)‘𝑏))
62 imaeq1 5607 . . . . . . . . . . . . . 14 (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝑥𝑦) = ((rec(𝐺, ∅)‘𝑏) “ 𝑦))
6362fveq2d 6344 . . . . . . . . . . . . 13 (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝐹‘(𝑥𝑦)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))
6461, 63mpteq12dv 4873 . . . . . . . . . . . 12 (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
65 ackbij.g . . . . . . . . . . . 12 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥𝑦))))
6659dmex 7252 . . . . . . . . . . . . . 14 dom (rec(𝐺, ∅)‘𝑏) ∈ V
6766pwex 4985 . . . . . . . . . . . . 13 𝒫 dom (rec(𝐺, ∅)‘𝑏) ∈ V
6867mptex 6638 . . . . . . . . . . . 12 (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) ∈ V
6964, 65, 68fvmpt 6432 . . . . . . . . . . 11 ((rec(𝐺, ∅)‘𝑏) ∈ V → (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
7059, 69ax-mp 5 . . . . . . . . . 10 (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))
7158, 70syl6eq 2798 . . . . . . . . 9 (𝑏 ∈ ω → (𝐺‘((rec(𝐺, ∅) ↾ ω)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
7254, 56, 713eqtr3d 2790 . . . . . . . 8 (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
7372adantr 472 . . . . . . 7 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
74 f1odm 6290 . . . . . . . . . . 11 ((rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏)) → dom (rec(𝐺, ∅)‘𝑏) = (𝑅1𝑏))
7574adantl 473 . . . . . . . . . 10 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → dom (rec(𝐺, ∅)‘𝑏) = (𝑅1𝑏))
7675pweqd 4295 . . . . . . . . 9 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → 𝒫 dom (rec(𝐺, ∅)‘𝑏) = 𝒫 (𝑅1𝑏))
7776mpteq1d 4878 . . . . . . . 8 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
78 fvex 6350 . . . . . . . . . . 11 (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)) ∈ V
79 eqid 2748 . . . . . . . . . . 11 (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))
8078, 79fnmpti 6171 . . . . . . . . . 10 (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) Fn 𝒫 (𝑅1𝑏)
8180a1i 11 . . . . . . . . 9 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) Fn 𝒫 (𝑅1𝑏))
82 f1ofn 6287 . . . . . . . . . 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 6286 . . . . . . . . . . . . . 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 6510 . . . . . . . . . . . 12 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) ∈ 𝒫 (card‘(𝑅1𝑏)))
8786fvresd 6357 . . . . . . . . . . 11 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)))
88 imaeq2 5608 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → ((rec(𝐺, ∅)‘𝑏) “ 𝑎) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
89 eqid 2748 . . . . . . . . . . . . . 14 (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)) = (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))
9059imaex 7257 . . . . . . . . . . . . . 14 ((rec(𝐺, ∅)‘𝑏) “ 𝑐) ∈ V
9188, 89, 90fvmpt 6432 . . . . . . . . . . . . 13 (𝑐 ∈ 𝒫 (𝑅1𝑏) → ((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
9291adantl 473 . . . . . . . . . . . 12 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
9392fveq2d 6344 . . . . . . . . . . 11 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → (𝐹‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
9487, 93eqtrd 2782 . . . . . . . . . 10 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
95 fvco3 6425 . . . . . . . . . . 11 (((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫 (𝑅1𝑏)⟶𝒫 (card‘(𝑅1𝑏)) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)))
9685, 95sylan 489 . . . . . . . . . 10 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)))
97 imaeq2 5608 . . . . . . . . . . . . 13 (𝑦 = 𝑐 → ((rec(𝐺, ∅)‘𝑏) “ 𝑦) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
9897fveq2d 6344 . . . . . . . . . . . 12 (𝑦 = 𝑐 → (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
99 fvex 6350 . . . . . . . . . . . 12 (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)) ∈ V
10098, 79, 99fvmpt 6432 . . . . . . . . . . 11 (𝑐 ∈ 𝒫 (𝑅1𝑏) → ((𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
101100adantl 473 . . . . . . . . . 10 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
10294, 96, 1013eqtr4rd 2793 . . . . . . . . 9 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐))
10381, 83, 102eqfnfvd 6465 . . . . . . . 8 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))))
10477, 103eqtrd 2782 . . . . . . 7 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))))
10573, 104eqtrd 2782 . . . . . 6 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))))
106 f1oeq1 6276 . . . . . 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 7224 . . . . . . . 8 (𝑏 ∈ ω → 𝑏 ∈ On)
109 r1suc 8794 . . . . . . . 8 (𝑏 ∈ On → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1𝑏))
110108, 109syl 17 . . . . . . 7 (𝑏 ∈ ω → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1𝑏))
111110fveq2d 6344 . . . . . . 7 (𝑏 ∈ ω → (card‘(𝑅1‘suc 𝑏)) = (card‘𝒫 (𝑅1𝑏)))
112 f1oeq23 6279 . . . . . . 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 696 . . . . . 6 (𝑏 ∈ ω → (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)) ↔ ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):𝒫 (𝑅1𝑏)–1-1-onto→(card‘𝒫 (𝑅1𝑏))))
114113adantr 472 . . . . 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 268 . . . 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 247 . . 3 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)))
117116ex 449 . 2 (𝑏 ∈ ω → ((rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏)) → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏))))
1184, 8, 12, 16, 29, 117finds 7245 1 (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴):(𝑅1𝐴)–1-1-onto→(card‘(𝑅1𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1620  wcel 2127  Vcvv 3328  cin 3702  wss 3703  c0 4046  𝒫 cpw 4290  {csn 4309   ciun 4660   class class class wbr 4792  cmpt 4869   × cxp 5252  dom cdm 5254  cres 5256  cima 5257  ccom 5258  Oncon0 5872  suc csuc 5874   Fn wfn 6032  wf 6033  1-1wf1 6034  1-1-ontowf1o 6036  cfv 6037  ωcom 7218  reccrdg 7662  cen 8106  Fincfn 8109  𝑅1cr1 8786  cardccrd 8922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-rep 4911  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-reu 3045  df-rmo 3046  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-pss 3719  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-tp 4314  df-op 4316  df-uni 4577  df-int 4616  df-iun 4662  df-br 4793  df-opab 4853  df-mpt 4870  df-tr 4893  df-id 5162  df-eprel 5167  df-po 5175  df-so 5176  df-fr 5213  df-we 5215  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-pred 5829  df-ord 5875  df-on 5876  df-lim 5877  df-suc 5878  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-ov 6804  df-oprab 6805  df-mpt2 6806  df-om 7219  df-1st 7321  df-2nd 7322  df-wrecs 7564  df-recs 7625  df-rdg 7663  df-1o 7717  df-2o 7718  df-oadd 7721  df-er 7899  df-map 8013  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-r1 8788  df-card 8926  df-cda 9153
This theorem is referenced by:  ackbij2lem3  9226  ackbij2  9228
  Copyright terms: Public domain W3C validator