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

Theorem ackbij2lem2 10258
Description: Lemma for ackbij2 10261. (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 6890 . . 3 (π‘Ž = βˆ… β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) = (rec(𝐺, βˆ…)β€˜βˆ…))
2 fveq2 6890 . . 3 (π‘Ž = βˆ… β†’ (𝑅1β€˜π‘Ž) = (𝑅1β€˜βˆ…))
3 2fveq3 6895 . . 3 (π‘Ž = βˆ… β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) = (cardβ€˜(𝑅1β€˜βˆ…)))
41, 2, 3f1oeq123d 6826 . 2 (π‘Ž = βˆ… β†’ ((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘Ž)) ↔ (rec(𝐺, βˆ…)β€˜βˆ…):(𝑅1β€˜βˆ…)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜βˆ…))))
5 fveq2 6890 . . 3 (π‘Ž = 𝑏 β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) = (rec(𝐺, βˆ…)β€˜π‘))
6 fveq2 6890 . . 3 (π‘Ž = 𝑏 β†’ (𝑅1β€˜π‘Ž) = (𝑅1β€˜π‘))
7 2fveq3 6895 . . 3 (π‘Ž = 𝑏 β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) = (cardβ€˜(𝑅1β€˜π‘)))
85, 6, 7f1oeq123d 6826 . 2 (π‘Ž = 𝑏 β†’ ((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘Ž)) ↔ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))))
9 fveq2 6890 . . 3 (π‘Ž = suc 𝑏 β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) = (rec(𝐺, βˆ…)β€˜suc 𝑏))
10 fveq2 6890 . . 3 (π‘Ž = suc 𝑏 β†’ (𝑅1β€˜π‘Ž) = (𝑅1β€˜suc 𝑏))
11 2fveq3 6895 . . 3 (π‘Ž = suc 𝑏 β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) = (cardβ€˜(𝑅1β€˜suc 𝑏)))
129, 10, 11f1oeq123d 6826 . 2 (π‘Ž = suc 𝑏 β†’ ((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘Ž)) ↔ (rec(𝐺, βˆ…)β€˜suc 𝑏):(𝑅1β€˜suc 𝑏)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜suc 𝑏))))
13 fveq2 6890 . . 3 (π‘Ž = 𝐴 β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) = (rec(𝐺, βˆ…)β€˜π΄))
14 fveq2 6890 . . 3 (π‘Ž = 𝐴 β†’ (𝑅1β€˜π‘Ž) = (𝑅1β€˜π΄))
15 2fveq3 6895 . . 3 (π‘Ž = 𝐴 β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) = (cardβ€˜(𝑅1β€˜π΄)))
1613, 14, 15f1oeq123d 6826 . 2 (π‘Ž = 𝐴 β†’ ((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘Ž)) ↔ (rec(𝐺, βˆ…)β€˜π΄):(𝑅1β€˜π΄)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π΄))))
17 f1o0 6869 . . 3 βˆ…:βˆ…β€“1-1-ontoβ†’βˆ…
18 0ex 5303 . . . . . 6 βˆ… ∈ V
1918rdg0 8435 . . . . 5 (rec(𝐺, βˆ…)β€˜βˆ…) = βˆ…
20 f1oeq1 6820 . . . . 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 9786 . . . . 5 (𝑅1β€˜βˆ…) = βˆ…
2322fveq2i 6893 . . . . . 6 (cardβ€˜(𝑅1β€˜βˆ…)) = (cardβ€˜βˆ…)
24 card0 9976 . . . . . 6 (cardβ€˜βˆ…) = βˆ…
2523, 24eqtri 2753 . . . . 5 (cardβ€˜(𝑅1β€˜βˆ…)) = βˆ…
26 f1oeq23 6823 . . . . 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 10254 . . . . . . . . 9 𝐹:(𝒫 Ο‰ ∩ Fin)–1-1β†’Ο‰
3231a1i 11 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ 𝐹:(𝒫 Ο‰ ∩ Fin)–1-1β†’Ο‰)
33 r1fin 9791 . . . . . . . . . 10 (𝑏 ∈ Ο‰ β†’ (𝑅1β€˜π‘) ∈ Fin)
34 ficardom 9979 . . . . . . . . . 10 ((𝑅1β€˜π‘) ∈ Fin β†’ (cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰)
3533, 34syl 17 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ (cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰)
36 ackbij2lem1 10237 . . . . . . . . 9 ((cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰ β†’ 𝒫 (cardβ€˜(𝑅1β€˜π‘)) βŠ† (𝒫 Ο‰ ∩ Fin))
3735, 36syl 17 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ 𝒫 (cardβ€˜(𝑅1β€˜π‘)) βŠ† (𝒫 Ο‰ ∩ Fin))
38 f1ores 6846 . . . . . . . 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 10257 . . . . . . . . . 10 ((cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰ β†’ (𝐹 β€œ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) = (cardβ€˜π’« (cardβ€˜(𝑅1β€˜π‘))))
4135, 40syl 17 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ (𝐹 β€œ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) = (cardβ€˜π’« (cardβ€˜(𝑅1β€˜π‘))))
42 ficardid 9980 . . . . . . . . . 10 ((𝑅1β€˜π‘) ∈ Fin β†’ (cardβ€˜(𝑅1β€˜π‘)) β‰ˆ (𝑅1β€˜π‘))
43 pwen 9168 . . . . . . . . . 10 ((cardβ€˜(𝑅1β€˜π‘)) β‰ˆ (𝑅1β€˜π‘) β†’ 𝒫 (cardβ€˜(𝑅1β€˜π‘)) β‰ˆ 𝒫 (𝑅1β€˜π‘))
44 carden2b 9985 . . . . . . . . . 10 (𝒫 (cardβ€˜(𝑅1β€˜π‘)) β‰ˆ 𝒫 (𝑅1β€˜π‘) β†’ (cardβ€˜π’« (cardβ€˜(𝑅1β€˜π‘))) = (cardβ€˜π’« (𝑅1β€˜π‘)))
4533, 42, 43, 444syl 19 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ (cardβ€˜π’« (cardβ€˜(𝑅1β€˜π‘))) = (cardβ€˜π’« (𝑅1β€˜π‘)))
4641, 45eqtrd 2765 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ (𝐹 β€œ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) = (cardβ€˜π’« (𝑅1β€˜π‘)))
4746f1oeq3d 6829 . . . . . . 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 7671 . . . . . 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 6855 . . . . 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 8451 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ ((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜suc 𝑏) = (πΊβ€˜((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜π‘)))
55 peano2 7891 . . . . . . . . . 10 (𝑏 ∈ Ο‰ β†’ suc 𝑏 ∈ Ο‰)
5655fvresd 6910 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ ((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜suc 𝑏) = (rec(𝐺, βˆ…)β€˜suc 𝑏))
57 fvres 6909 . . . . . . . . . . 11 (𝑏 ∈ Ο‰ β†’ ((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜π‘) = (rec(𝐺, βˆ…)β€˜π‘))
5857fveq2d 6894 . . . . . . . . . 10 (𝑏 ∈ Ο‰ β†’ (πΊβ€˜((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜π‘)) = (πΊβ€˜(rec(𝐺, βˆ…)β€˜π‘)))
59 fvex 6903 . . . . . . . . . . 11 (rec(𝐺, βˆ…)β€˜π‘) ∈ V
60 dmeq 5901 . . . . . . . . . . . . . 14 (π‘₯ = (rec(𝐺, βˆ…)β€˜π‘) β†’ dom π‘₯ = dom (rec(𝐺, βˆ…)β€˜π‘))
6160pweqd 4616 . . . . . . . . . . . . 13 (π‘₯ = (rec(𝐺, βˆ…)β€˜π‘) β†’ 𝒫 dom π‘₯ = 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘))
62 imaeq1 6054 . . . . . . . . . . . . . 14 (π‘₯ = (rec(𝐺, βˆ…)β€˜π‘) β†’ (π‘₯ β€œ 𝑦) = ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))
6362fveq2d 6894 . . . . . . . . . . . . 13 (π‘₯ = (rec(𝐺, βˆ…)β€˜π‘) β†’ (πΉβ€˜(π‘₯ β€œ 𝑦)) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))
6461, 63mpteq12dv 5235 . . . . . . . . . . . 12 (π‘₯ = (rec(𝐺, βˆ…)β€˜π‘) β†’ (𝑦 ∈ 𝒫 dom π‘₯ ↦ (πΉβ€˜(π‘₯ β€œ 𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
65 ackbij.g . . . . . . . . . . . 12 𝐺 = (π‘₯ ∈ V ↦ (𝑦 ∈ 𝒫 dom π‘₯ ↦ (πΉβ€˜(π‘₯ β€œ 𝑦))))
6659dmex 7911 . . . . . . . . . . . . . 14 dom (rec(𝐺, βˆ…)β€˜π‘) ∈ V
6766pwex 5375 . . . . . . . . . . . . 13 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ∈ V
6867mptex 7229 . . . . . . . . . . . 12 (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) ∈ V
6964, 65, 68fvmpt 6998 . . . . . . . . . . 11 ((rec(𝐺, βˆ…)β€˜π‘) ∈ V β†’ (πΊβ€˜(rec(𝐺, βˆ…)β€˜π‘)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
7059, 69ax-mp 5 . . . . . . . . . 10 (πΊβ€˜(rec(𝐺, βˆ…)β€˜π‘)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))
7158, 70eqtrdi 2781 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ (πΊβ€˜((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜π‘)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
7254, 56, 713eqtr3d 2773 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
7372adantr 479 . . . . . . 7 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
74 f1odm 6836 . . . . . . . . . . 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 4616 . . . . . . . . 9 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) = 𝒫 (𝑅1β€˜π‘))
7776mpteq1d 5239 . . . . . . . 8 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) = (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
78 fvex 6903 . . . . . . . . . . 11 (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)) ∈ V
79 eqid 2725 . . . . . . . . . . 11 (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) = (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))
8078, 79fnmpti 6693 . . . . . . . . . 10 (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) Fn 𝒫 (𝑅1β€˜π‘)
8180a1i 11 . . . . . . . . 9 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) Fn 𝒫 (𝑅1β€˜π‘))
82 f1ofn 6833 . . . . . . . . . 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 6832 . . . . . . . . . . . . . 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 7087 . . . . . . . . . . . 12 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘) ∈ 𝒫 (cardβ€˜(𝑅1β€˜π‘)))
8786fvresd 6910 . . . . . . . . . . 11 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘)))β€˜((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘)) = (πΉβ€˜((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘)))
88 imaeq2 6055 . . . . . . . . . . . . . 14 (π‘Ž = 𝑐 β†’ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž) = ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐))
89 eqid 2725 . . . . . . . . . . . . . 14 (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž)) = (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))
9059imaex 7916 . . . . . . . . . . . . . 14 ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐) ∈ V
9188, 89, 90fvmpt 6998 . . . . . . . . . . . . 13 (𝑐 ∈ 𝒫 (𝑅1β€˜π‘) β†’ ((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘) = ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐))
9291adantl 480 . . . . . . . . . . . 12 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘) = ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐))
9392fveq2d 6894 . . . . . . . . . . 11 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ (πΉβ€˜((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘)) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)))
9487, 93eqtrd 2765 . . . . . . . . . 10 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘)))β€˜((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘)) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)))
95 fvco3 6990 . . . . . . . . . . 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 6055 . . . . . . . . . . . . 13 (𝑦 = 𝑐 β†’ ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦) = ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐))
9897fveq2d 6894 . . . . . . . . . . . 12 (𝑦 = 𝑐 β†’ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)))
99 fvex 6903 . . . . . . . . . . . 12 (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)) ∈ V
10098, 79, 99fvmpt 6998 . . . . . . . . . . 11 (𝑐 ∈ 𝒫 (𝑅1β€˜π‘) β†’ ((𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))β€˜π‘) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)))
101100adantl 480 . . . . . . . . . 10 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))β€˜π‘) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)))
10294, 96, 1013eqtr4rd 2776 . . . . . . . . 9 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))β€˜π‘) = (((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž)))β€˜π‘))
10381, 83, 102eqfnfvd 7036 . . . . . . . 8 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) = ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))))
10477, 103eqtrd 2765 . . . . . . 7 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) = ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))))
10573, 104eqtrd 2765 . . . . . 6 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏) = ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))))
106 f1oeq1 6820 . . . . . 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 7871 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ 𝑏 ∈ On)
109 r1suc 9788 . . . . . . . 8 (𝑏 ∈ On β†’ (𝑅1β€˜suc 𝑏) = 𝒫 (𝑅1β€˜π‘))
110108, 109syl 17 . . . . . . 7 (𝑏 ∈ Ο‰ β†’ (𝑅1β€˜suc 𝑏) = 𝒫 (𝑅1β€˜π‘))
111110fveq2d 6894 . . . . . . 7 (𝑏 ∈ Ο‰ β†’ (cardβ€˜(𝑅1β€˜suc 𝑏)) = (cardβ€˜π’« (𝑅1β€˜π‘)))
112 f1oeq23 6823 . . . . . . 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 7898 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 3463   ∩ cin 3940   βŠ† wss 3941  βˆ…c0 4319  π’« cpw 4599  {csn 4625  βˆͺ ciun 4992   class class class wbr 5144   ↦ cmpt 5227   Γ— cxp 5671  dom cdm 5673   β†Ύ cres 5675   β€œ cima 5676   ∘ ccom 5677  Oncon0 6365  suc csuc 6367   Fn wfn 6538  βŸΆwf 6539  β€“1-1β†’wf1 6540  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543  Ο‰com 7865  reccrdg 8423   β‰ˆ cen 8954  Fincfn 8957  π‘…1cr1 9780  cardccrd 9953
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 2696  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735
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 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-int 4946  df-iun 4994  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7866  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-oadd 8484  df-er 8718  df-map 8840  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-r1 9782  df-dju 9919  df-card 9957
This theorem is referenced by:  ackbij2lem3  10259  ackbij2  10261
  Copyright terms: Public domain W3C validator