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

Theorem ackbij2lem2 10176
Description: Lemma for ackbij2 10179. (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 6842 . . 3 (𝑎 = ∅ → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘∅))
2 fveq2 6842 . . 3 (𝑎 = ∅ → (𝑅1𝑎) = (𝑅1‘∅))
3 2fveq3 6847 . . 3 (𝑎 = ∅ → (card‘(𝑅1𝑎)) = (card‘(𝑅1‘∅)))
41, 2, 3f1oeq123d 6778 . 2 (𝑎 = ∅ → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘∅):(𝑅1‘∅)–1-1-onto→(card‘(𝑅1‘∅))))
5 fveq2 6842 . . 3 (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏))
6 fveq2 6842 . . 3 (𝑎 = 𝑏 → (𝑅1𝑎) = (𝑅1𝑏))
7 2fveq3 6847 . . 3 (𝑎 = 𝑏 → (card‘(𝑅1𝑎)) = (card‘(𝑅1𝑏)))
85, 6, 7f1oeq123d 6778 . 2 (𝑎 = 𝑏 → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))))
9 fveq2 6842 . . 3 (𝑎 = suc 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘suc 𝑏))
10 fveq2 6842 . . 3 (𝑎 = suc 𝑏 → (𝑅1𝑎) = (𝑅1‘suc 𝑏))
11 2fveq3 6847 . . 3 (𝑎 = suc 𝑏 → (card‘(𝑅1𝑎)) = (card‘(𝑅1‘suc 𝑏)))
129, 10, 11f1oeq123d 6778 . 2 (𝑎 = suc 𝑏 → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏))))
13 fveq2 6842 . . 3 (𝑎 = 𝐴 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝐴))
14 fveq2 6842 . . 3 (𝑎 = 𝐴 → (𝑅1𝑎) = (𝑅1𝐴))
15 2fveq3 6847 . . 3 (𝑎 = 𝐴 → (card‘(𝑅1𝑎)) = (card‘(𝑅1𝐴)))
1613, 14, 15f1oeq123d 6778 . 2 (𝑎 = 𝐴 → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)) ↔ (rec(𝐺, ∅)‘𝐴):(𝑅1𝐴)–1-1-onto→(card‘(𝑅1𝐴))))
17 f1o0 6821 . . 3 ∅:∅–1-1-onto→∅
18 0ex 5264 . . . . . 6 ∅ ∈ V
1918rdg0 8367 . . . . 5 (rec(𝐺, ∅)‘∅) = ∅
20 f1oeq1 6772 . . . . 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 9704 . . . . 5 (𝑅1‘∅) = ∅
2322fveq2i 6845 . . . . . 6 (card‘(𝑅1‘∅)) = (card‘∅)
24 card0 9894 . . . . . 6 (card‘∅) = ∅
2523, 24eqtri 2764 . . . . 5 (card‘(𝑅1‘∅)) = ∅
26 f1oeq23 6775 . . . . 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 10172 . . . . . . . . 9 𝐹:(𝒫 ω ∩ Fin)–1-1→ω
3231a1i 11 . . . . . . . 8 (𝑏 ∈ ω → 𝐹:(𝒫 ω ∩ Fin)–1-1→ω)
33 r1fin 9709 . . . . . . . . . 10 (𝑏 ∈ ω → (𝑅1𝑏) ∈ Fin)
34 ficardom 9897 . . . . . . . . . 10 ((𝑅1𝑏) ∈ Fin → (card‘(𝑅1𝑏)) ∈ ω)
3533, 34syl 17 . . . . . . . . 9 (𝑏 ∈ ω → (card‘(𝑅1𝑏)) ∈ ω)
36 ackbij2lem1 10155 . . . . . . . . 9 ((card‘(𝑅1𝑏)) ∈ ω → 𝒫 (card‘(𝑅1𝑏)) ⊆ (𝒫 ω ∩ Fin))
3735, 36syl 17 . . . . . . . 8 (𝑏 ∈ ω → 𝒫 (card‘(𝑅1𝑏)) ⊆ (𝒫 ω ∩ Fin))
38 f1ores 6798 . . . . . . . 8 ((𝐹:(𝒫 ω ∩ Fin)–1-1→ω ∧ 𝒫 (card‘(𝑅1𝑏)) ⊆ (𝒫 ω ∩ Fin)) → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(𝐹 “ 𝒫 (card‘(𝑅1𝑏))))
3932, 37, 38syl2anc 584 . . . . . . 7 (𝑏 ∈ ω → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(𝐹 “ 𝒫 (card‘(𝑅1𝑏))))
4030ackbij1b 10175 . . . . . . . . . 10 ((card‘(𝑅1𝑏)) ∈ ω → (𝐹 “ 𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (card‘(𝑅1𝑏))))
4135, 40syl 17 . . . . . . . . 9 (𝑏 ∈ ω → (𝐹 “ 𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (card‘(𝑅1𝑏))))
42 ficardid 9898 . . . . . . . . . 10 ((𝑅1𝑏) ∈ Fin → (card‘(𝑅1𝑏)) ≈ (𝑅1𝑏))
43 pwen 9094 . . . . . . . . . 10 ((card‘(𝑅1𝑏)) ≈ (𝑅1𝑏) → 𝒫 (card‘(𝑅1𝑏)) ≈ 𝒫 (𝑅1𝑏))
44 carden2b 9903 . . . . . . . . . 10 (𝒫 (card‘(𝑅1𝑏)) ≈ 𝒫 (𝑅1𝑏) → (card‘𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (𝑅1𝑏)))
4533, 42, 43, 444syl 19 . . . . . . . . 9 (𝑏 ∈ ω → (card‘𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (𝑅1𝑏)))
4641, 45eqtrd 2776 . . . . . . . 8 (𝑏 ∈ ω → (𝐹 “ 𝒫 (card‘(𝑅1𝑏))) = (card‘𝒫 (𝑅1𝑏)))
4746f1oeq3d 6781 . . . . . . 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 481 . . . . 5 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))):𝒫 (card‘(𝑅1𝑏))–1-1-onto→(card‘𝒫 (𝑅1𝑏)))
50 f1opw 7609 . . . . . 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 6807 . . . . 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 584 . . . 4 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))):𝒫 (𝑅1𝑏)–1-1-onto→(card‘𝒫 (𝑅1𝑏)))
54 frsuc 8383 . . . . . . . . 9 (𝑏 ∈ ω → ((rec(𝐺, ∅) ↾ ω)‘suc 𝑏) = (𝐺‘((rec(𝐺, ∅) ↾ ω)‘𝑏)))
55 peano2 7827 . . . . . . . . . 10 (𝑏 ∈ ω → suc 𝑏 ∈ ω)
5655fvresd 6862 . . . . . . . . 9 (𝑏 ∈ ω → ((rec(𝐺, ∅) ↾ ω)‘suc 𝑏) = (rec(𝐺, ∅)‘suc 𝑏))
57 fvres 6861 . . . . . . . . . . 11 (𝑏 ∈ ω → ((rec(𝐺, ∅) ↾ ω)‘𝑏) = (rec(𝐺, ∅)‘𝑏))
5857fveq2d 6846 . . . . . . . . . 10 (𝑏 ∈ ω → (𝐺‘((rec(𝐺, ∅) ↾ ω)‘𝑏)) = (𝐺‘(rec(𝐺, ∅)‘𝑏)))
59 fvex 6855 . . . . . . . . . . 11 (rec(𝐺, ∅)‘𝑏) ∈ V
60 dmeq 5859 . . . . . . . . . . . . . 14 (𝑥 = (rec(𝐺, ∅)‘𝑏) → dom 𝑥 = dom (rec(𝐺, ∅)‘𝑏))
6160pweqd 4577 . . . . . . . . . . . . 13 (𝑥 = (rec(𝐺, ∅)‘𝑏) → 𝒫 dom 𝑥 = 𝒫 dom (rec(𝐺, ∅)‘𝑏))
62 imaeq1 6008 . . . . . . . . . . . . . 14 (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝑥𝑦) = ((rec(𝐺, ∅)‘𝑏) “ 𝑦))
6362fveq2d 6846 . . . . . . . . . . . . 13 (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝐹‘(𝑥𝑦)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))
6461, 63mpteq12dv 5196 . . . . . . . . . . . 12 (𝑥 = (rec(𝐺, ∅)‘𝑏) → (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
65 ackbij.g . . . . . . . . . . . 12 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥𝑦))))
6659dmex 7848 . . . . . . . . . . . . . 14 dom (rec(𝐺, ∅)‘𝑏) ∈ V
6766pwex 5335 . . . . . . . . . . . . 13 𝒫 dom (rec(𝐺, ∅)‘𝑏) ∈ V
6867mptex 7173 . . . . . . . . . . . 12 (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) ∈ V
6964, 65, 68fvmpt 6948 . . . . . . . . . . 11 ((rec(𝐺, ∅)‘𝑏) ∈ V → (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
7059, 69ax-mp 5 . . . . . . . . . 10 (𝐺‘(rec(𝐺, ∅)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))
7158, 70eqtrdi 2792 . . . . . . . . 9 (𝑏 ∈ ω → (𝐺‘((rec(𝐺, ∅) ↾ ω)‘𝑏)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
7254, 56, 713eqtr3d 2784 . . . . . . . 8 (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
7372adantr 481 . . . . . . 7 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
74 f1odm 6788 . . . . . . . . . . 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 4577 . . . . . . . . 9 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → 𝒫 dom (rec(𝐺, ∅)‘𝑏) = 𝒫 (𝑅1𝑏))
7776mpteq1d 5200 . . . . . . . 8 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))))
78 fvex 6855 . . . . . . . . . . 11 (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)) ∈ V
79 eqid 2736 . . . . . . . . . . 11 (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))
8078, 79fnmpti 6644 . . . . . . . . . 10 (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) Fn 𝒫 (𝑅1𝑏)
8180a1i 11 . . . . . . . . 9 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) Fn 𝒫 (𝑅1𝑏))
82 f1ofn 6785 . . . . . . . . . 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 6784 . . . . . . . . . . . . . 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 7035 . . . . . . . . . . . 12 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) ∈ 𝒫 (card‘(𝑅1𝑏)))
8786fvresd 6862 . . . . . . . . . . 11 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)))
88 imaeq2 6009 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → ((rec(𝐺, ∅)‘𝑏) “ 𝑎) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
89 eqid 2736 . . . . . . . . . . . . . 14 (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)) = (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))
9059imaex 7853 . . . . . . . . . . . . . 14 ((rec(𝐺, ∅)‘𝑏) “ 𝑐) ∈ V
9188, 89, 90fvmpt 6948 . . . . . . . . . . . . 13 (𝑐 ∈ 𝒫 (𝑅1𝑏) → ((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
9291adantl 482 . . . . . . . . . . . 12 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
9392fveq2d 6846 . . . . . . . . . . 11 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → (𝐹‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
9487, 93eqtrd 2776 . . . . . . . . . 10 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
95 fvco3 6940 . . . . . . . . . . 11 (((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)):𝒫 (𝑅1𝑏)⟶𝒫 (card‘(𝑅1𝑏)) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)))
9685, 95sylan 580 . . . . . . . . . 10 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏)))‘((𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))‘𝑐)))
97 imaeq2 6009 . . . . . . . . . . . . 13 (𝑦 = 𝑐 → ((rec(𝐺, ∅)‘𝑏) “ 𝑦) = ((rec(𝐺, ∅)‘𝑏) “ 𝑐))
9897fveq2d 6846 . . . . . . . . . . . 12 (𝑦 = 𝑐 → (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
99 fvex 6855 . . . . . . . . . . . 12 (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)) ∈ V
10098, 79, 99fvmpt 6948 . . . . . . . . . . 11 (𝑐 ∈ 𝒫 (𝑅1𝑏) → ((𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
101100adantl 482 . . . . . . . . . 10 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑐)))
10294, 96, 1013eqtr4rd 2787 . . . . . . . . 9 (((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) ∧ 𝑐 ∈ 𝒫 (𝑅1𝑏)) → ((𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦)))‘𝑐) = (((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎)))‘𝑐))
10381, 83, 102eqfnfvd 6985 . . . . . . . 8 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 (𝑅1𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))))
10477, 103eqtrd 2776 . . . . . . 7 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (𝑦 ∈ 𝒫 dom (rec(𝐺, ∅)‘𝑏) ↦ (𝐹‘((rec(𝐺, ∅)‘𝑏) “ 𝑦))) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))))
10573, 104eqtrd 2776 . . . . . 6 ((𝑏 ∈ ω ∧ (rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏))) → (rec(𝐺, ∅)‘suc 𝑏) = ((𝐹 ↾ 𝒫 (card‘(𝑅1𝑏))) ∘ (𝑎 ∈ 𝒫 (𝑅1𝑏) ↦ ((rec(𝐺, ∅)‘𝑏) “ 𝑎))))
106 f1oeq1 6772 . . . . . 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 7808 . . . . . . . 8 (𝑏 ∈ ω → 𝑏 ∈ On)
109 r1suc 9706 . . . . . . . 8 (𝑏 ∈ On → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1𝑏))
110108, 109syl 17 . . . . . . 7 (𝑏 ∈ ω → (𝑅1‘suc 𝑏) = 𝒫 (𝑅1𝑏))
111110fveq2d 6846 . . . . . . 7 (𝑏 ∈ ω → (card‘(𝑅1‘suc 𝑏)) = (card‘𝒫 (𝑅1𝑏)))
112 f1oeq23 6775 . . . . . . 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 584 . . . . . 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 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 413 . 2 (𝑏 ∈ ω → ((rec(𝐺, ∅)‘𝑏):(𝑅1𝑏)–1-1-onto→(card‘(𝑅1𝑏)) → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏))))
1184, 8, 12, 16, 29, 117finds 7835 1 (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴):(𝑅1𝐴)–1-1-onto→(card‘(𝑅1𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  Vcvv 3445  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560  {csn 4586   ciun 4954   class class class wbr 5105  cmpt 5188   × cxp 5631  dom cdm 5633  cres 5635  cima 5636  ccom 5637  Oncon0 6317  suc csuc 6319   Fn wfn 6491  wf 6492  1-1wf1 6493  1-1-ontowf1o 6495  cfv 6496  ωcom 7802  reccrdg 8355  cen 8880  Fincfn 8883  𝑅1cr1 9698  cardccrd 9871
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-oadd 8416  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-r1 9700  df-dju 9837  df-card 9875
This theorem is referenced by:  ackbij2lem3  10177  ackbij2  10179
  Copyright terms: Public domain W3C validator