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

Theorem ackbij2lem2 10271
Description: Lemma for ackbij2 10274. (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 6902 . . 3 (𝑎 = ∅ → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘∅))
2 fveq2 6902 . . 3 (𝑎 = ∅ → (𝑅1𝑎) = (𝑅1‘∅))
3 2fveq3 6907 . . 3 (𝑎 = ∅ → (card‘(𝑅1𝑎)) = (card‘(𝑅1‘∅)))
41, 2, 3f1oeq123d 6838 . 2 (𝑎 = ∅ → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅))))
5 fveq2 6902 . . 3 (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏))
6 fveq2 6902 . . 3 (𝑎 = 𝑏 → (𝑅1𝑎) = (𝑅1𝑏))
7 2fveq3 6907 . . 3 (𝑎 = 𝑏 → (card‘(𝑅1𝑎)) = (card‘(𝑅1𝑏)))
85, 6, 7f1oeq123d 6838 . 2 (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))))
9 fveq2 6902 . . 3 (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘suc 𝑏))
10 fveq2 6902 . . 3 (𝑎 = suc 𝑏 → (𝑅1𝑎) = (𝑅1‘suc 𝑏))
11 2fveq3 6907 . . 3 (𝑎 = suc 𝑏 → (card‘(𝑅1𝑎)) = (card‘(𝑅1‘suc 𝑏)))
129, 10, 11f1oeq123d 6838 . 2 (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏))))
13 fveq2 6902 . . 3 (𝑎 = 𝐴 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝐴))
14 fveq2 6902 . . 3 (𝑎 = 𝐴 → (𝑅1𝑎) = (𝑅1𝐴))
15 2fveq3 6907 . . 3 (𝑎 = 𝐴 → (card‘(𝑅1𝑎)) = (card‘(𝑅1𝐴)))
1613, 14, 15f1oeq123d 6838 . 2 (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘𝐴):(𝑅1𝐴)–1-1-onto→(card‘(𝑅1𝐴))))
17 f1o0 6881 . . 3 ∅:∅–1-1-onto→∅
18 0ex 5311 . . . . . 6 ∅ ∈ V
1918rdg0 8448 . . . . 5 (rec(𝐺, ∅)‘∅) = ∅
20 f1oeq1 6832 . . . . 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 9799 . . . . 5 (𝑅1‘∅) = ∅
2322fveq2i 6905 . . . . . 6 (card‘(𝑅1‘∅)) = (card‘∅)
24 card0 9989 . . . . . 6 (card‘∅) = ∅
2523, 24eqtri 2756 . . . . 5 (card‘(𝑅1‘∅)) = ∅
26 f1oeq23 6835 . . . . 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 274 . . 3 ((rec(𝐺, ∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅)) ↔ ∅:∅–1-1-onto→∅)
2917, 28mpbir 230 . 2 (rec(𝐺, ∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅))
30 ackbij.f . . . . . . . . . 10 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘ 𝑦𝑥 ({𝑦} × 𝒫 𝑦)))
3130ackbij1lem17 10267 . . . . . . . . 9 𝐹:(𝒫 ω ∩ Fin)–1-1→ω
3231a1i 11 . . . . . . . 8 (𝑏 ∈ ω → 𝐹:(𝒫 ω ∩ Fin)–1-1→ω)
33 r1fin 9804 . . . . . . . . . 10 (𝑏 ∈ ω → (𝑅1𝑏) ∈ Fin)
34 ficardom 9992 . . . . . . . . . 10 ((𝑅1𝑏) ∈ Fin → (card‘(𝑅1𝑏)) ∈ ω)
3533, 34syl 17 . . . . . . . . 9 (𝑏 ∈ ω → (card‘(𝑅1𝑏)) ∈ ω)
36 ackbij2lem1 10250 . . . . . . . . 9 ((card‘(𝑅1𝑏)) ∈ ω → 𝒫 (card‘(𝑅1𝑏)) ⊆ (𝒫 ω ∩ Fin))
3735, 36syl 17 . . . . . . . 8 (𝑏 ∈ ω → 𝒫 (card‘(𝑅1𝑏)) ⊆ (𝒫 ω ∩ Fin))
38 f1ores 6858 . . . . . . . 8 ((𝐹:(𝒫 ω ∩ Fin)–1-1→ω ∧ 𝒫 (card‘(𝑅1𝑏)) ⊆ (𝒫 ω ∩ Fin)) → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(𝐹 “ 𝒫 (card‘(𝑅1𝑏))))
3932, 37, 38syl2anc 582 . . . . . . 7 (𝑏 ∈ ω → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(𝐹 “ 𝒫 (card‘(𝑅1𝑏))))
4030ackbij1b 10270 . . . . . . . . . 10 ((card‘(𝑅1𝑏)) ∈ ω → (𝐹 “ 𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (card‘(𝑅1𝑏))))
4135, 40syl 17 . . . . . . . . 9 (𝑏 ∈ ω → (𝐹 “ 𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (card‘(𝑅1𝑏))))
42 ficardid 9993 . . . . . . . . . 10 ((𝑅1𝑏) ∈ Fin → (card‘(𝑅1𝑏)) ≈ (𝑅1𝑏))
43 pwen 9181 . . . . . . . . . 10 ((card‘(𝑅1𝑏)) ≈ (𝑅1𝑏) → 𝒫 (card‘(𝑅1𝑏)) ≈ 𝒫 (𝑅1𝑏))
44 carden2b 9998 . . . . . . . . . 10 (𝒫 (card‘(𝑅1𝑏)) ≈ 𝒫 (𝑅1𝑏) → (card‘𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (𝑅1𝑏)))
4533, 42, 43, 444syl 19 . . . . . . . . 9 (𝑏 ∈ ω → (card‘𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (𝑅1𝑏)))
4641, 45eqtrd 2768 . . . . . . . 8 (𝑏 ∈ ω → (𝐹 “ 𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (𝑅1𝑏)))
4746f1oeq3d 6841 . . . . . . 7 (𝑏 ∈ ω → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(𝐹 “ 𝒫 (card‘(𝑅1𝑏))) ↔ (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(card‘𝒫 (𝑅1𝑏))))
4839, 47mpbid 231 . . . . . 6 (𝑏 ∈ ω → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(card‘𝒫 (𝑅1𝑏)))
4948adantr 479 . . . . 5 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(card‘𝒫 (𝑅1𝑏)))
50 f1opw 7683 . . . . . 6 ((rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏)) → (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫 (𝑅1𝑏)–1-1-onto→𝒫 (card‘(𝑅1𝑏)))
5150adantl 480 . . . . 5 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫 (𝑅1𝑏)–1-1-onto→𝒫 (card‘(𝑅1𝑏)))
52 f1oco 6867 . . . . 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 582 . . . 4 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):𝒫 (𝑅1𝑏)–1-1-onto→(card‘𝒫 (𝑅1𝑏)))
54 frsuc 8464 . . . . . . . . 9 (𝑏 ∈ ω → ((rec(𝐺, ∅) ↾ ω)‘suc 𝑏) = (𝐺‘((rec(𝐺, ∅) ↾ ω)‘𝑏)))
55 peano2 7902 . . . . . . . . . 10 (𝑏 ∈ ω → suc 𝑏 ∈ ω)
5655fvresd 6922 . . . . . . . . 9 (𝑏 ∈ ω → ((rec(𝐺, ∅) ↾ ω)‘suc 𝑏) = (rec(𝐺, ∅)‘suc 𝑏))
57 fvres 6921 . . . . . . . . . . 11 (𝑏 ∈ ω → ((rec(𝐺, ∅) ↾ ω)‘𝑏) = (rec(𝐺, ∅)‘𝑏))
5857fveq2d 6906 . . . . . . . . . 10 (𝑏 ∈ ω → (𝐺‘((rec(𝐺, ∅) ↾ ω)‘𝑏)) = (𝐺‘(rec(𝐺, ∅)‘𝑏)))
59 fvex 6915 . . . . . . . . . . 11 (rec(𝐺, ∅)‘𝑏) ∈ V
60 dmeq 5910 . . . . . . . . . . . . . 14 (𝑥 = (rec(𝐺, ∅)‘𝑏) → dom 𝑥 = dom (rec(𝐺, ∅)‘𝑏))
6160pweqd 4623 . . . . . . . . . . . . 13 (𝑥 = (rec(𝐺, ∅)‘𝑏) → 𝒫 dom 𝑥 = 𝒫 dom (rec(𝐺, ∅)‘𝑏))
62 imaeq1 6063 . . . . . . . . . . . . . 14 (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝑥𝑦) = ((rec(𝐺, ∅)‘𝑏) “ 𝑦))
6362fveq2d 6906 . . . . . . . . . . . . 13 (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝐹‘(𝑥𝑦)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))
6461, 63mpteq12dv 5243 . . . . . . . . . . . 12 (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
65 ackbij.g . . . . . . . . . . . 12 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥𝑦))))
6659dmex 7923 . . . . . . . . . . . . . 14 dom (rec(𝐺, ∅)‘𝑏) ∈ V
6766pwex 5384 . . . . . . . . . . . . 13 𝒫 dom (rec(𝐺, ∅)‘𝑏) ∈ V
6867mptex 7241 . . . . . . . . . . . 12 (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) ∈ V
6964, 65, 68fvmpt 7010 . . . . . . . . . . 11 ((rec(𝐺, ∅)‘𝑏) ∈ V → (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
7059, 69ax-mp 5 . . . . . . . . . 10 (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))
7158, 70eqtrdi 2784 . . . . . . . . 9 (𝑏 ∈ ω → (𝐺‘((rec(𝐺, ∅) ↾ ω)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
7254, 56, 713eqtr3d 2776 . . . . . . . 8 (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
7372adantr 479 . . . . . . 7 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
74 f1odm 6848 . . . . . . . . . . 11 ((rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏)) → dom (rec(𝐺, ∅)‘𝑏) = (𝑅1𝑏))
7574adantl 480 . . . . . . . . . 10 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → dom (rec(𝐺, ∅)‘𝑏) = (𝑅1𝑏))
7675pweqd 4623 . . . . . . . . 9 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → 𝒫 dom (rec(𝐺, ∅)‘𝑏) = 𝒫 (𝑅1𝑏))
7776mpteq1d 5247 . . . . . . . 8 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
78 fvex 6915 . . . . . . . . . . 11 (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)) ∈ V
79 eqid 2728 . . . . . . . . . . 11 (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))
8078, 79fnmpti 6703 . . . . . . . . . 10 (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) Fn 𝒫 (𝑅1𝑏)
8180a1i 11 . . . . . . . . 9 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) Fn 𝒫 (𝑅1𝑏))
82 f1ofn 6845 . . . . . . . . . 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 6844 . . . . . . . . . . . . . 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𝑏)))
8685ffvelcdmda 7099 . . . . . . . . . . . 12 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) ∈ 𝒫 (card‘(𝑅1𝑏)))
8786fvresd 6922 . . . . . . . . . . 11 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)))
88 imaeq2 6064 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → ((rec(𝐺, ∅)‘𝑏) “ 𝑎) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
89 eqid 2728 . . . . . . . . . . . . . 14 (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)) = (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))
9059imaex 7928 . . . . . . . . . . . . . 14 ((rec(𝐺, ∅)‘𝑏) “ 𝑐) ∈ V
9188, 89, 90fvmpt 7010 . . . . . . . . . . . . 13 (𝑐 ∈ 𝒫 (𝑅1𝑏) → ((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
9291adantl 480 . . . . . . . . . . . 12 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
9392fveq2d 6906 . . . . . . . . . . 11 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → (𝐹‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
9487, 93eqtrd 2768 . . . . . . . . . 10 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
95 fvco3 7002 . . . . . . . . . . 11 (((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫 (𝑅1𝑏)⟶𝒫 (card‘(𝑅1𝑏)) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)))
9685, 95sylan 578 . . . . . . . . . 10 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)))
97 imaeq2 6064 . . . . . . . . . . . . 13 (𝑦 = 𝑐 → ((rec(𝐺, ∅)‘𝑏) “ 𝑦) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
9897fveq2d 6906 . . . . . . . . . . . 12 (𝑦 = 𝑐 → (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
99 fvex 6915 . . . . . . . . . . . 12 (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)) ∈ V
10098, 79, 99fvmpt 7010 . . . . . . . . . . 11 (𝑐 ∈ 𝒫 (𝑅1𝑏) → ((𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
101100adantl 480 . . . . . . . . . 10 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
10294, 96, 1013eqtr4rd 2779 . . . . . . . . 9 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐))
10381, 83, 102eqfnfvd 7048 . . . . . . . 8 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))))
10477, 103eqtrd 2768 . . . . . . 7 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))))
10573, 104eqtrd 2768 . . . . . 6 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))))
106 f1oeq1 6832 . . . . . 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 7882 . . . . . . . 8 (𝑏 ∈ ω → 𝑏 ∈ On)
109 r1suc 9801 . . . . . . . 8 (𝑏 ∈ On → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1𝑏))
110108, 109syl 17 . . . . . . 7 (𝑏 ∈ ω → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1𝑏))
111110fveq2d 6906 . . . . . . 7 (𝑏 ∈ ω → (card‘(𝑅1‘suc 𝑏)) = (card‘𝒫 (𝑅1𝑏)))
112 f1oeq23 6835 . . . . . . 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 582 . . . . . 6 (𝑏 ∈ ω → (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)) ↔ ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):𝒫 (𝑅1𝑏)–1-1-onto→(card‘𝒫 (𝑅1𝑏))))
114113adantr 479 . . . . 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 278 . . . 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 256 . . 3 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)))
117116ex 411 . 2 (𝑏 ∈ ω → ((rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏)) → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏))))
1184, 8, 12, 16, 29, 117finds 7910 1 (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴):(𝑅1𝐴)–1-1-onto→(card‘(𝑅1𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  Vcvv 3473  cin 3948  wss 3949  c0 4326  𝒫 cpw 4606  {csn 4632   ciun 5000   class class class wbr 5152  cmpt 5235   × cxp 5680  dom cdm 5682  cres 5684  cima 5685  ccom 5686  Oncon0 6374  suc csuc 6376   Fn wfn 6548  wf 6549  1-1wf1 6550  1-1-ontowf1o 6552  cfv 6553  ωcom 7876  reccrdg 8436  cen 8967  Fincfn 8970  𝑅1cr1 9793  cardccrd 9966
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-1st 7999  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-1o 8493  df-2o 8494  df-oadd 8497  df-er 8731  df-map 8853  df-en 8971  df-dom 8972  df-sdom 8973  df-fin 8974  df-r1 9795  df-dju 9932  df-card 9970
This theorem is referenced by:  ackbij2lem3  10272  ackbij2  10274
  Copyright terms: Public domain W3C validator