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

Theorem ackbij2lem2 10181
Description: Lemma for ackbij2 10184. (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 6843 . . 3 (π‘Ž = βˆ… β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) = (rec(𝐺, βˆ…)β€˜βˆ…))
2 fveq2 6843 . . 3 (π‘Ž = βˆ… β†’ (𝑅1β€˜π‘Ž) = (𝑅1β€˜βˆ…))
3 2fveq3 6848 . . 3 (π‘Ž = βˆ… β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) = (cardβ€˜(𝑅1β€˜βˆ…)))
41, 2, 3f1oeq123d 6779 . 2 (π‘Ž = βˆ… β†’ ((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘Ž)) ↔ (rec(𝐺, βˆ…)β€˜βˆ…):(𝑅1β€˜βˆ…)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜βˆ…))))
5 fveq2 6843 . . 3 (π‘Ž = 𝑏 β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) = (rec(𝐺, βˆ…)β€˜π‘))
6 fveq2 6843 . . 3 (π‘Ž = 𝑏 β†’ (𝑅1β€˜π‘Ž) = (𝑅1β€˜π‘))
7 2fveq3 6848 . . 3 (π‘Ž = 𝑏 β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) = (cardβ€˜(𝑅1β€˜π‘)))
85, 6, 7f1oeq123d 6779 . 2 (π‘Ž = 𝑏 β†’ ((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘Ž)) ↔ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))))
9 fveq2 6843 . . 3 (π‘Ž = suc 𝑏 β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) = (rec(𝐺, βˆ…)β€˜suc 𝑏))
10 fveq2 6843 . . 3 (π‘Ž = suc 𝑏 β†’ (𝑅1β€˜π‘Ž) = (𝑅1β€˜suc 𝑏))
11 2fveq3 6848 . . 3 (π‘Ž = suc 𝑏 β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) = (cardβ€˜(𝑅1β€˜suc 𝑏)))
129, 10, 11f1oeq123d 6779 . 2 (π‘Ž = suc 𝑏 β†’ ((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘Ž)) ↔ (rec(𝐺, βˆ…)β€˜suc 𝑏):(𝑅1β€˜suc 𝑏)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜suc 𝑏))))
13 fveq2 6843 . . 3 (π‘Ž = 𝐴 β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) = (rec(𝐺, βˆ…)β€˜π΄))
14 fveq2 6843 . . 3 (π‘Ž = 𝐴 β†’ (𝑅1β€˜π‘Ž) = (𝑅1β€˜π΄))
15 2fveq3 6848 . . 3 (π‘Ž = 𝐴 β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) = (cardβ€˜(𝑅1β€˜π΄)))
1613, 14, 15f1oeq123d 6779 . 2 (π‘Ž = 𝐴 β†’ ((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘Ž)) ↔ (rec(𝐺, βˆ…)β€˜π΄):(𝑅1β€˜π΄)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π΄))))
17 f1o0 6822 . . 3 βˆ…:βˆ…β€“1-1-ontoβ†’βˆ…
18 0ex 5265 . . . . . 6 βˆ… ∈ V
1918rdg0 8368 . . . . 5 (rec(𝐺, βˆ…)β€˜βˆ…) = βˆ…
20 f1oeq1 6773 . . . . 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 9709 . . . . 5 (𝑅1β€˜βˆ…) = βˆ…
2322fveq2i 6846 . . . . . 6 (cardβ€˜(𝑅1β€˜βˆ…)) = (cardβ€˜βˆ…)
24 card0 9899 . . . . . 6 (cardβ€˜βˆ…) = βˆ…
2523, 24eqtri 2761 . . . . 5 (cardβ€˜(𝑅1β€˜βˆ…)) = βˆ…
26 f1oeq23 6776 . . . . 5 (((𝑅1β€˜βˆ…) = βˆ… ∧ (cardβ€˜(𝑅1β€˜βˆ…)) = βˆ…) β†’ (βˆ…:(𝑅1β€˜βˆ…)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜βˆ…)) ↔ βˆ…:βˆ…β€“1-1-ontoβ†’βˆ…))
2722, 25, 26mp2an 691 . . . 4 (βˆ…:(𝑅1β€˜βˆ…)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜βˆ…)) ↔ βˆ…:βˆ…β€“1-1-ontoβ†’βˆ…)
2821, 27bitri 275 . . 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 10177 . . . . . . . . 9 𝐹:(𝒫 Ο‰ ∩ Fin)–1-1β†’Ο‰
3231a1i 11 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ 𝐹:(𝒫 Ο‰ ∩ Fin)–1-1β†’Ο‰)
33 r1fin 9714 . . . . . . . . . 10 (𝑏 ∈ Ο‰ β†’ (𝑅1β€˜π‘) ∈ Fin)
34 ficardom 9902 . . . . . . . . . 10 ((𝑅1β€˜π‘) ∈ Fin β†’ (cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰)
3533, 34syl 17 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ (cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰)
36 ackbij2lem1 10160 . . . . . . . . 9 ((cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰ β†’ 𝒫 (cardβ€˜(𝑅1β€˜π‘)) βŠ† (𝒫 Ο‰ ∩ Fin))
3735, 36syl 17 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ 𝒫 (cardβ€˜(𝑅1β€˜π‘)) βŠ† (𝒫 Ο‰ ∩ Fin))
38 f1ores 6799 . . . . . . . 8 ((𝐹:(𝒫 Ο‰ ∩ Fin)–1-1β†’Ο‰ ∧ 𝒫 (cardβ€˜(𝑅1β€˜π‘)) βŠ† (𝒫 Ο‰ ∩ Fin)) β†’ (𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))):𝒫 (cardβ€˜(𝑅1β€˜π‘))–1-1-ontoβ†’(𝐹 β€œ 𝒫 (cardβ€˜(𝑅1β€˜π‘))))
3932, 37, 38syl2anc 585 . . . . . . 7 (𝑏 ∈ Ο‰ β†’ (𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))):𝒫 (cardβ€˜(𝑅1β€˜π‘))–1-1-ontoβ†’(𝐹 β€œ 𝒫 (cardβ€˜(𝑅1β€˜π‘))))
4030ackbij1b 10180 . . . . . . . . . 10 ((cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰ β†’ (𝐹 β€œ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) = (cardβ€˜π’« (cardβ€˜(𝑅1β€˜π‘))))
4135, 40syl 17 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ (𝐹 β€œ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) = (cardβ€˜π’« (cardβ€˜(𝑅1β€˜π‘))))
42 ficardid 9903 . . . . . . . . . 10 ((𝑅1β€˜π‘) ∈ Fin β†’ (cardβ€˜(𝑅1β€˜π‘)) β‰ˆ (𝑅1β€˜π‘))
43 pwen 9097 . . . . . . . . . 10 ((cardβ€˜(𝑅1β€˜π‘)) β‰ˆ (𝑅1β€˜π‘) β†’ 𝒫 (cardβ€˜(𝑅1β€˜π‘)) β‰ˆ 𝒫 (𝑅1β€˜π‘))
44 carden2b 9908 . . . . . . . . . 10 (𝒫 (cardβ€˜(𝑅1β€˜π‘)) β‰ˆ 𝒫 (𝑅1β€˜π‘) β†’ (cardβ€˜π’« (cardβ€˜(𝑅1β€˜π‘))) = (cardβ€˜π’« (𝑅1β€˜π‘)))
4533, 42, 43, 444syl 19 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ (cardβ€˜π’« (cardβ€˜(𝑅1β€˜π‘))) = (cardβ€˜π’« (𝑅1β€˜π‘)))
4641, 45eqtrd 2773 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ (𝐹 β€œ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) = (cardβ€˜π’« (𝑅1β€˜π‘)))
4746f1oeq3d 6782 . . . . . . 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 482 . . . . 5 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))):𝒫 (cardβ€˜(𝑅1β€˜π‘))–1-1-ontoβ†’(cardβ€˜π’« (𝑅1β€˜π‘)))
50 f1opw 7610 . . . . . 6 ((rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘)) β†’ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž)):𝒫 (𝑅1β€˜π‘)–1-1-onto→𝒫 (cardβ€˜(𝑅1β€˜π‘)))
5150adantl 483 . . . . 5 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž)):𝒫 (𝑅1β€˜π‘)–1-1-onto→𝒫 (cardβ€˜(𝑅1β€˜π‘)))
52 f1oco 6808 . . . . 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 585 . . . 4 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))):𝒫 (𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜π’« (𝑅1β€˜π‘)))
54 frsuc 8384 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ ((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜suc 𝑏) = (πΊβ€˜((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜π‘)))
55 peano2 7828 . . . . . . . . . 10 (𝑏 ∈ Ο‰ β†’ suc 𝑏 ∈ Ο‰)
5655fvresd 6863 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ ((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜suc 𝑏) = (rec(𝐺, βˆ…)β€˜suc 𝑏))
57 fvres 6862 . . . . . . . . . . 11 (𝑏 ∈ Ο‰ β†’ ((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜π‘) = (rec(𝐺, βˆ…)β€˜π‘))
5857fveq2d 6847 . . . . . . . . . 10 (𝑏 ∈ Ο‰ β†’ (πΊβ€˜((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜π‘)) = (πΊβ€˜(rec(𝐺, βˆ…)β€˜π‘)))
59 fvex 6856 . . . . . . . . . . 11 (rec(𝐺, βˆ…)β€˜π‘) ∈ V
60 dmeq 5860 . . . . . . . . . . . . . 14 (π‘₯ = (rec(𝐺, βˆ…)β€˜π‘) β†’ dom π‘₯ = dom (rec(𝐺, βˆ…)β€˜π‘))
6160pweqd 4578 . . . . . . . . . . . . 13 (π‘₯ = (rec(𝐺, βˆ…)β€˜π‘) β†’ 𝒫 dom π‘₯ = 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘))
62 imaeq1 6009 . . . . . . . . . . . . . 14 (π‘₯ = (rec(𝐺, βˆ…)β€˜π‘) β†’ (π‘₯ β€œ 𝑦) = ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))
6362fveq2d 6847 . . . . . . . . . . . . 13 (π‘₯ = (rec(𝐺, βˆ…)β€˜π‘) β†’ (πΉβ€˜(π‘₯ β€œ 𝑦)) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))
6461, 63mpteq12dv 5197 . . . . . . . . . . . 12 (π‘₯ = (rec(𝐺, βˆ…)β€˜π‘) β†’ (𝑦 ∈ 𝒫 dom π‘₯ ↦ (πΉβ€˜(π‘₯ β€œ 𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
65 ackbij.g . . . . . . . . . . . 12 𝐺 = (π‘₯ ∈ V ↦ (𝑦 ∈ 𝒫 dom π‘₯ ↦ (πΉβ€˜(π‘₯ β€œ 𝑦))))
6659dmex 7849 . . . . . . . . . . . . . 14 dom (rec(𝐺, βˆ…)β€˜π‘) ∈ V
6766pwex 5336 . . . . . . . . . . . . 13 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ∈ V
6867mptex 7174 . . . . . . . . . . . 12 (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) ∈ V
6964, 65, 68fvmpt 6949 . . . . . . . . . . 11 ((rec(𝐺, βˆ…)β€˜π‘) ∈ V β†’ (πΊβ€˜(rec(𝐺, βˆ…)β€˜π‘)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
7059, 69ax-mp 5 . . . . . . . . . 10 (πΊβ€˜(rec(𝐺, βˆ…)β€˜π‘)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))
7158, 70eqtrdi 2789 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ (πΊβ€˜((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜π‘)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
7254, 56, 713eqtr3d 2781 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
7372adantr 482 . . . . . . 7 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
74 f1odm 6789 . . . . . . . . . . 11 ((rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘)) β†’ dom (rec(𝐺, βˆ…)β€˜π‘) = (𝑅1β€˜π‘))
7574adantl 483 . . . . . . . . . 10 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ dom (rec(𝐺, βˆ…)β€˜π‘) = (𝑅1β€˜π‘))
7675pweqd 4578 . . . . . . . . 9 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) = 𝒫 (𝑅1β€˜π‘))
7776mpteq1d 5201 . . . . . . . 8 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) = (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
78 fvex 6856 . . . . . . . . . . 11 (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)) ∈ V
79 eqid 2733 . . . . . . . . . . 11 (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) = (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))
8078, 79fnmpti 6645 . . . . . . . . . 10 (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) Fn 𝒫 (𝑅1β€˜π‘)
8180a1i 11 . . . . . . . . 9 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) Fn 𝒫 (𝑅1β€˜π‘))
82 f1ofn 6786 . . . . . . . . . 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 6785 . . . . . . . . . . . . . 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 7036 . . . . . . . . . . . 12 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘) ∈ 𝒫 (cardβ€˜(𝑅1β€˜π‘)))
8786fvresd 6863 . . . . . . . . . . 11 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘)))β€˜((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘)) = (πΉβ€˜((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘)))
88 imaeq2 6010 . . . . . . . . . . . . . 14 (π‘Ž = 𝑐 β†’ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž) = ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐))
89 eqid 2733 . . . . . . . . . . . . . 14 (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž)) = (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))
9059imaex 7854 . . . . . . . . . . . . . 14 ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐) ∈ V
9188, 89, 90fvmpt 6949 . . . . . . . . . . . . 13 (𝑐 ∈ 𝒫 (𝑅1β€˜π‘) β†’ ((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘) = ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐))
9291adantl 483 . . . . . . . . . . . 12 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘) = ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐))
9392fveq2d 6847 . . . . . . . . . . 11 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ (πΉβ€˜((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘)) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)))
9487, 93eqtrd 2773 . . . . . . . . . 10 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘)))β€˜((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘)) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)))
95 fvco3 6941 . . . . . . . . . . 11 (((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž)):𝒫 (𝑅1β€˜π‘)βŸΆπ’« (cardβ€˜(𝑅1β€˜π‘)) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ (((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž)))β€˜π‘) = ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘)))β€˜((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘)))
9685, 95sylan 581 . . . . . . . . . 10 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ (((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž)))β€˜π‘) = ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘)))β€˜((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘)))
97 imaeq2 6010 . . . . . . . . . . . . 13 (𝑦 = 𝑐 β†’ ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦) = ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐))
9897fveq2d 6847 . . . . . . . . . . . 12 (𝑦 = 𝑐 β†’ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)))
99 fvex 6856 . . . . . . . . . . . 12 (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)) ∈ V
10098, 79, 99fvmpt 6949 . . . . . . . . . . 11 (𝑐 ∈ 𝒫 (𝑅1β€˜π‘) β†’ ((𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))β€˜π‘) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)))
101100adantl 483 . . . . . . . . . 10 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))β€˜π‘) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)))
10294, 96, 1013eqtr4rd 2784 . . . . . . . . 9 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))β€˜π‘) = (((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž)))β€˜π‘))
10381, 83, 102eqfnfvd 6986 . . . . . . . 8 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) = ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))))
10477, 103eqtrd 2773 . . . . . . 7 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) = ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))))
10573, 104eqtrd 2773 . . . . . 6 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏) = ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))))
106 f1oeq1 6773 . . . . . 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 7809 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ 𝑏 ∈ On)
109 r1suc 9711 . . . . . . . 8 (𝑏 ∈ On β†’ (𝑅1β€˜suc 𝑏) = 𝒫 (𝑅1β€˜π‘))
110108, 109syl 17 . . . . . . 7 (𝑏 ∈ Ο‰ β†’ (𝑅1β€˜suc 𝑏) = 𝒫 (𝑅1β€˜π‘))
111110fveq2d 6847 . . . . . . 7 (𝑏 ∈ Ο‰ β†’ (cardβ€˜(𝑅1β€˜suc 𝑏)) = (cardβ€˜π’« (𝑅1β€˜π‘)))
112 f1oeq23 6776 . . . . . . 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 585 . . . . . 6 (𝑏 ∈ Ο‰ β†’ (((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))):(𝑅1β€˜suc 𝑏)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜suc 𝑏)) ↔ ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))):𝒫 (𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜π’« (𝑅1β€˜π‘))))
114113adantr 482 . . . . 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 279 . . . 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 257 . . 3 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏):(𝑅1β€˜suc 𝑏)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜suc 𝑏)))
117116ex 414 . 2 (𝑏 ∈ Ο‰ β†’ ((rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘)) β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏):(𝑅1β€˜suc 𝑏)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜suc 𝑏))))
1184, 8, 12, 16, 29, 117finds 7836 1 (𝐴 ∈ Ο‰ β†’ (rec(𝐺, βˆ…)β€˜π΄):(𝑅1β€˜π΄)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π΄)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3444   ∩ cin 3910   βŠ† wss 3911  βˆ…c0 4283  π’« cpw 4561  {csn 4587  βˆͺ ciun 4955   class class class wbr 5106   ↦ cmpt 5189   Γ— cxp 5632  dom cdm 5634   β†Ύ cres 5636   β€œ cima 5637   ∘ ccom 5638  Oncon0 6318  suc csuc 6320   Fn wfn 6492  βŸΆwf 6493  β€“1-1β†’wf1 6494  β€“1-1-ontoβ†’wf1o 6496  β€˜cfv 6497  Ο‰com 7803  reccrdg 8356   β‰ˆ cen 8883  Fincfn 8886  π‘…1cr1 9703  cardccrd 9876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-oadd 8417  df-er 8651  df-map 8770  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-r1 9705  df-dju 9842  df-card 9880
This theorem is referenced by:  ackbij2lem3  10182  ackbij2  10184
  Copyright terms: Public domain W3C validator