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

Theorem ackbij2lem2 9047
Description: Lemma for ackbij2 9050. (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 6178 . . 3 (𝑎 = ∅ → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘∅))
2 fveq2 6178 . . 3 (𝑎 = ∅ → (𝑅1𝑎) = (𝑅1‘∅))
32fveq2d 6182 . . 3 (𝑎 = ∅ → (card‘(𝑅1𝑎)) = (card‘(𝑅1‘∅)))
41, 2, 3f1oeq123d 6120 . 2 (𝑎 = ∅ → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅))))
5 fveq2 6178 . . 3 (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏))
6 fveq2 6178 . . 3 (𝑎 = 𝑏 → (𝑅1𝑎) = (𝑅1𝑏))
76fveq2d 6182 . . 3 (𝑎 = 𝑏 → (card‘(𝑅1𝑎)) = (card‘(𝑅1𝑏)))
85, 6, 7f1oeq123d 6120 . 2 (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))))
9 fveq2 6178 . . 3 (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘suc 𝑏))
10 fveq2 6178 . . 3 (𝑎 = suc 𝑏 → (𝑅1𝑎) = (𝑅1‘suc 𝑏))
1110fveq2d 6182 . . 3 (𝑎 = suc 𝑏 → (card‘(𝑅1𝑎)) = (card‘(𝑅1‘suc 𝑏)))
129, 10, 11f1oeq123d 6120 . 2 (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏))))
13 fveq2 6178 . . 3 (𝑎 = 𝐴 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝐴))
14 fveq2 6178 . . 3 (𝑎 = 𝐴 → (𝑅1𝑎) = (𝑅1𝐴))
1514fveq2d 6182 . . 3 (𝑎 = 𝐴 → (card‘(𝑅1𝑎)) = (card‘(𝑅1𝐴)))
1613, 14, 15f1oeq123d 6120 . 2 (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘𝐴):(𝑅1𝐴)–1-1-onto→(card‘(𝑅1𝐴))))
17 f1o0 6160 . . 3 ∅:∅–1-1-onto→∅
18 0ex 4781 . . . . . 6 ∅ ∈ V
1918rdg0 7502 . . . . 5 (rec(𝐺, ∅)‘∅) = ∅
20 f1oeq1 6114 . . . . 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 8616 . . . . 5 (𝑅1‘∅) = ∅
2322fveq2i 6181 . . . . . 6 (card‘(𝑅1‘∅)) = (card‘∅)
24 card0 8769 . . . . . 6 (card‘∅) = ∅
2523, 24eqtri 2642 . . . . 5 (card‘(𝑅1‘∅)) = ∅
26 f1oeq23 6117 . . . . 5 (((𝑅1‘∅) = ∅ ∧ (card‘(𝑅1‘∅)) = ∅) → (∅:(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅)) ↔ ∅:∅–1-1-onto→∅))
2722, 25, 26mp2an 707 . . . 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 9043 . . . . . . . . 9 𝐹:(𝒫 ω ∩ Fin)–1-1→ω
3231a1i 11 . . . . . . . 8 (𝑏 ∈ ω → 𝐹:(𝒫 ω ∩ Fin)–1-1→ω)
33 r1fin 8621 . . . . . . . . . 10 (𝑏 ∈ ω → (𝑅1𝑏) ∈ Fin)
34 ficardom 8772 . . . . . . . . . 10 ((𝑅1𝑏) ∈ Fin → (card‘(𝑅1𝑏)) ∈ ω)
3533, 34syl 17 . . . . . . . . 9 (𝑏 ∈ ω → (card‘(𝑅1𝑏)) ∈ ω)
36 ackbij2lem1 9026 . . . . . . . . 9 ((card‘(𝑅1𝑏)) ∈ ω → 𝒫 (card‘(𝑅1𝑏)) ⊆ (𝒫 ω ∩ Fin))
3735, 36syl 17 . . . . . . . 8 (𝑏 ∈ ω → 𝒫 (card‘(𝑅1𝑏)) ⊆ (𝒫 ω ∩ Fin))
38 f1ores 6138 . . . . . . . 8 ((𝐹:(𝒫 ω ∩ Fin)–1-1→ω ∧ 𝒫 (card‘(𝑅1𝑏)) ⊆ (𝒫 ω ∩ Fin)) → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(𝐹 “ 𝒫 (card‘(𝑅1𝑏))))
3932, 37, 38syl2anc 692 . . . . . . 7 (𝑏 ∈ ω → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(𝐹 “ 𝒫 (card‘(𝑅1𝑏))))
4030ackbij1b 9046 . . . . . . . . . 10 ((card‘(𝑅1𝑏)) ∈ ω → (𝐹 “ 𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (card‘(𝑅1𝑏))))
4135, 40syl 17 . . . . . . . . 9 (𝑏 ∈ ω → (𝐹 “ 𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (card‘(𝑅1𝑏))))
42 ficardid 8773 . . . . . . . . . 10 ((𝑅1𝑏) ∈ Fin → (card‘(𝑅1𝑏)) ≈ (𝑅1𝑏))
43 pwen 8118 . . . . . . . . . 10 ((card‘(𝑅1𝑏)) ≈ (𝑅1𝑏) → 𝒫 (card‘(𝑅1𝑏)) ≈ 𝒫 (𝑅1𝑏))
44 carden2b 8778 . . . . . . . . . 10 (𝒫 (card‘(𝑅1𝑏)) ≈ 𝒫 (𝑅1𝑏) → (card‘𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (𝑅1𝑏)))
4533, 42, 43, 444syl 19 . . . . . . . . 9 (𝑏 ∈ ω → (card‘𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (𝑅1𝑏)))
4641, 45eqtrd 2654 . . . . . . . 8 (𝑏 ∈ ω → (𝐹 “ 𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (𝑅1𝑏)))
4746f1oeq3d 6121 . . . . . . 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 481 . . . . 5 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(card‘𝒫 (𝑅1𝑏)))
50 f1opw 6874 . . . . . 6 ((rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏)) → (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫 (𝑅1𝑏)–1-1-onto→𝒫 (card‘(𝑅1𝑏)))
5150adantl 482 . . . . 5 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫 (𝑅1𝑏)–1-1-onto→𝒫 (card‘(𝑅1𝑏)))
52 f1oco 6146 . . . . 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 692 . . . 4 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):𝒫 (𝑅1𝑏)–1-1-onto→(card‘𝒫 (𝑅1𝑏)))
54 frsuc 7517 . . . . . . . . 9 (𝑏 ∈ ω → ((rec(𝐺, ∅) ↾ ω)‘suc 𝑏) = (𝐺‘((rec(𝐺, ∅) ↾ ω)‘𝑏)))
55 peano2 7071 . . . . . . . . . 10 (𝑏 ∈ ω → suc 𝑏 ∈ ω)
5655fvresd 6195 . . . . . . . . 9 (𝑏 ∈ ω → ((rec(𝐺, ∅) ↾ ω)‘suc 𝑏) = (rec(𝐺, ∅)‘suc 𝑏))
57 fvres 6194 . . . . . . . . . . 11 (𝑏 ∈ ω → ((rec(𝐺, ∅) ↾ ω)‘𝑏) = (rec(𝐺, ∅)‘𝑏))
5857fveq2d 6182 . . . . . . . . . 10 (𝑏 ∈ ω → (𝐺‘((rec(𝐺, ∅) ↾ ω)‘𝑏)) = (𝐺‘(rec(𝐺, ∅)‘𝑏)))
59 fvex 6188 . . . . . . . . . . 11 (rec(𝐺, ∅)‘𝑏) ∈ V
60 dmeq 5313 . . . . . . . . . . . . . 14 (𝑥 = (rec(𝐺, ∅)‘𝑏) → dom 𝑥 = dom (rec(𝐺, ∅)‘𝑏))
6160pweqd 4154 . . . . . . . . . . . . 13 (𝑥 = (rec(𝐺, ∅)‘𝑏) → 𝒫 dom 𝑥 = 𝒫 dom (rec(𝐺, ∅)‘𝑏))
62 imaeq1 5449 . . . . . . . . . . . . . 14 (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝑥𝑦) = ((rec(𝐺, ∅)‘𝑏) “ 𝑦))
6362fveq2d 6182 . . . . . . . . . . . . 13 (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝐹‘(𝑥𝑦)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))
6461, 63mpteq12dv 4724 . . . . . . . . . . . 12 (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
65 ackbij.g . . . . . . . . . . . 12 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥𝑦))))
6659dmex 7084 . . . . . . . . . . . . . 14 dom (rec(𝐺, ∅)‘𝑏) ∈ V
6766pwex 4839 . . . . . . . . . . . . 13 𝒫 dom (rec(𝐺, ∅)‘𝑏) ∈ V
6867mptex 6471 . . . . . . . . . . . 12 (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) ∈ V
6964, 65, 68fvmpt 6269 . . . . . . . . . . 11 ((rec(𝐺, ∅)‘𝑏) ∈ V → (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
7059, 69ax-mp 5 . . . . . . . . . 10 (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))
7158, 70syl6eq 2670 . . . . . . . . 9 (𝑏 ∈ ω → (𝐺‘((rec(𝐺, ∅) ↾ ω)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
7254, 56, 713eqtr3d 2662 . . . . . . . 8 (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
7372adantr 481 . . . . . . 7 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
74 f1odm 6128 . . . . . . . . . . 11 ((rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏)) → dom (rec(𝐺, ∅)‘𝑏) = (𝑅1𝑏))
7574adantl 482 . . . . . . . . . 10 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → dom (rec(𝐺, ∅)‘𝑏) = (𝑅1𝑏))
7675pweqd 4154 . . . . . . . . 9 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → 𝒫 dom (rec(𝐺, ∅)‘𝑏) = 𝒫 (𝑅1𝑏))
7776mpteq1d 4729 . . . . . . . 8 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
78 fvex 6188 . . . . . . . . . . 11 (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)) ∈ V
79 eqid 2620 . . . . . . . . . . 11 (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))
8078, 79fnmpti 6009 . . . . . . . . . 10 (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) Fn 𝒫 (𝑅1𝑏)
8180a1i 11 . . . . . . . . 9 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) Fn 𝒫 (𝑅1𝑏))
82 f1ofn 6125 . . . . . . . . . 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 6124 . . . . . . . . . . . . . 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 6345 . . . . . . . . . . . 12 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) ∈ 𝒫 (card‘(𝑅1𝑏)))
8786fvresd 6195 . . . . . . . . . . 11 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)))
88 imaeq2 5450 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → ((rec(𝐺, ∅)‘𝑏) “ 𝑎) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
89 eqid 2620 . . . . . . . . . . . . . 14 (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)) = (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))
9059imaex 7089 . . . . . . . . . . . . . 14 ((rec(𝐺, ∅)‘𝑏) “ 𝑐) ∈ V
9188, 89, 90fvmpt 6269 . . . . . . . . . . . . 13 (𝑐 ∈ 𝒫 (𝑅1𝑏) → ((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
9291adantl 482 . . . . . . . . . . . 12 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
9392fveq2d 6182 . . . . . . . . . . 11 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → (𝐹‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
9487, 93eqtrd 2654 . . . . . . . . . 10 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
95 fvco3 6262 . . . . . . . . . . 11 (((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫 (𝑅1𝑏)⟶𝒫 (card‘(𝑅1𝑏)) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)))
9685, 95sylan 488 . . . . . . . . . 10 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)))
97 imaeq2 5450 . . . . . . . . . . . . 13 (𝑦 = 𝑐 → ((rec(𝐺, ∅)‘𝑏) “ 𝑦) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
9897fveq2d 6182 . . . . . . . . . . . 12 (𝑦 = 𝑐 → (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
99 fvex 6188 . . . . . . . . . . . 12 (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)) ∈ V
10098, 79, 99fvmpt 6269 . . . . . . . . . . 11 (𝑐 ∈ 𝒫 (𝑅1𝑏) → ((𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
101100adantl 482 . . . . . . . . . 10 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
10294, 96, 1013eqtr4rd 2665 . . . . . . . . 9 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐))
10381, 83, 102eqfnfvd 6300 . . . . . . . 8 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))))
10477, 103eqtrd 2654 . . . . . . 7 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))))
10573, 104eqtrd 2654 . . . . . 6 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))))
106 f1oeq1 6114 . . . . . 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 7056 . . . . . . . 8 (𝑏 ∈ ω → 𝑏 ∈ On)
109 r1suc 8618 . . . . . . . 8 (𝑏 ∈ On → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1𝑏))
110108, 109syl 17 . . . . . . 7 (𝑏 ∈ ω → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1𝑏))
111110fveq2d 6182 . . . . . . 7 (𝑏 ∈ ω → (card‘(𝑅1‘suc 𝑏)) = (card‘𝒫 (𝑅1𝑏)))
112 f1oeq23 6117 . . . . . . 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 692 . . . . . 6 (𝑏 ∈ ω → (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)) ↔ ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):𝒫 (𝑅1𝑏)–1-1-onto→(card‘𝒫 (𝑅1𝑏))))
114113adantr 481 . . . . 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 450 . 2 (𝑏 ∈ ω → ((rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏)) → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏))))
1184, 8, 12, 16, 29, 117finds 7077 1 (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴):(𝑅1𝐴)–1-1-onto→(card‘(𝑅1𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1481  wcel 1988  Vcvv 3195  cin 3566  wss 3567  c0 3907  𝒫 cpw 4149  {csn 4168   ciun 4511   class class class wbr 4644  cmpt 4720   × cxp 5102  dom cdm 5104  cres 5106  cima 5107  ccom 5108  Oncon0 5711  suc csuc 5713   Fn wfn 5871  wf 5872  1-1wf1 5873  1-1-ontowf1o 5875  cfv 5876  ωcom 7050  reccrdg 7490  cen 7937  Fincfn 7940  𝑅1cr1 8610  cardccrd 8746
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-2o 7546  df-oadd 7549  df-er 7727  df-map 7844  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-r1 8612  df-card 8750  df-cda 8975
This theorem is referenced by:  ackbij2lem3  9048  ackbij2  9050
  Copyright terms: Public domain W3C validator