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

Theorem ackbij2lem2 10249
Description: Lemma for ackbij2 10252. (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 6891 . . 3 (π‘Ž = βˆ… β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) = (rec(𝐺, βˆ…)β€˜βˆ…))
2 fveq2 6891 . . 3 (π‘Ž = βˆ… β†’ (𝑅1β€˜π‘Ž) = (𝑅1β€˜βˆ…))
3 2fveq3 6896 . . 3 (π‘Ž = βˆ… β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) = (cardβ€˜(𝑅1β€˜βˆ…)))
41, 2, 3f1oeq123d 6827 . 2 (π‘Ž = βˆ… β†’ ((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘Ž)) ↔ (rec(𝐺, βˆ…)β€˜βˆ…):(𝑅1β€˜βˆ…)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜βˆ…))))
5 fveq2 6891 . . 3 (π‘Ž = 𝑏 β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) = (rec(𝐺, βˆ…)β€˜π‘))
6 fveq2 6891 . . 3 (π‘Ž = 𝑏 β†’ (𝑅1β€˜π‘Ž) = (𝑅1β€˜π‘))
7 2fveq3 6896 . . 3 (π‘Ž = 𝑏 β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) = (cardβ€˜(𝑅1β€˜π‘)))
85, 6, 7f1oeq123d 6827 . 2 (π‘Ž = 𝑏 β†’ ((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘Ž)) ↔ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))))
9 fveq2 6891 . . 3 (π‘Ž = suc 𝑏 β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) = (rec(𝐺, βˆ…)β€˜suc 𝑏))
10 fveq2 6891 . . 3 (π‘Ž = suc 𝑏 β†’ (𝑅1β€˜π‘Ž) = (𝑅1β€˜suc 𝑏))
11 2fveq3 6896 . . 3 (π‘Ž = suc 𝑏 β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) = (cardβ€˜(𝑅1β€˜suc 𝑏)))
129, 10, 11f1oeq123d 6827 . 2 (π‘Ž = suc 𝑏 β†’ ((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘Ž)) ↔ (rec(𝐺, βˆ…)β€˜suc 𝑏):(𝑅1β€˜suc 𝑏)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜suc 𝑏))))
13 fveq2 6891 . . 3 (π‘Ž = 𝐴 β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) = (rec(𝐺, βˆ…)β€˜π΄))
14 fveq2 6891 . . 3 (π‘Ž = 𝐴 β†’ (𝑅1β€˜π‘Ž) = (𝑅1β€˜π΄))
15 2fveq3 6896 . . 3 (π‘Ž = 𝐴 β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) = (cardβ€˜(𝑅1β€˜π΄)))
1613, 14, 15f1oeq123d 6827 . 2 (π‘Ž = 𝐴 β†’ ((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘Ž)) ↔ (rec(𝐺, βˆ…)β€˜π΄):(𝑅1β€˜π΄)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π΄))))
17 f1o0 6870 . . 3 βˆ…:βˆ…β€“1-1-ontoβ†’βˆ…
18 0ex 5301 . . . . . 6 βˆ… ∈ V
1918rdg0 8433 . . . . 5 (rec(𝐺, βˆ…)β€˜βˆ…) = βˆ…
20 f1oeq1 6821 . . . . 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 9777 . . . . 5 (𝑅1β€˜βˆ…) = βˆ…
2322fveq2i 6894 . . . . . 6 (cardβ€˜(𝑅1β€˜βˆ…)) = (cardβ€˜βˆ…)
24 card0 9967 . . . . . 6 (cardβ€˜βˆ…) = βˆ…
2523, 24eqtri 2755 . . . . 5 (cardβ€˜(𝑅1β€˜βˆ…)) = βˆ…
26 f1oeq23 6824 . . . . 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 10245 . . . . . . . . 9 𝐹:(𝒫 Ο‰ ∩ Fin)–1-1β†’Ο‰
3231a1i 11 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ 𝐹:(𝒫 Ο‰ ∩ Fin)–1-1β†’Ο‰)
33 r1fin 9782 . . . . . . . . . 10 (𝑏 ∈ Ο‰ β†’ (𝑅1β€˜π‘) ∈ Fin)
34 ficardom 9970 . . . . . . . . . 10 ((𝑅1β€˜π‘) ∈ Fin β†’ (cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰)
3533, 34syl 17 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ (cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰)
36 ackbij2lem1 10228 . . . . . . . . 9 ((cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰ β†’ 𝒫 (cardβ€˜(𝑅1β€˜π‘)) βŠ† (𝒫 Ο‰ ∩ Fin))
3735, 36syl 17 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ 𝒫 (cardβ€˜(𝑅1β€˜π‘)) βŠ† (𝒫 Ο‰ ∩ Fin))
38 f1ores 6847 . . . . . . . 8 ((𝐹:(𝒫 Ο‰ ∩ Fin)–1-1β†’Ο‰ ∧ 𝒫 (cardβ€˜(𝑅1β€˜π‘)) βŠ† (𝒫 Ο‰ ∩ Fin)) β†’ (𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))):𝒫 (cardβ€˜(𝑅1β€˜π‘))–1-1-ontoβ†’(𝐹 β€œ 𝒫 (cardβ€˜(𝑅1β€˜π‘))))
3932, 37, 38syl2anc 583 . . . . . . 7 (𝑏 ∈ Ο‰ β†’ (𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))):𝒫 (cardβ€˜(𝑅1β€˜π‘))–1-1-ontoβ†’(𝐹 β€œ 𝒫 (cardβ€˜(𝑅1β€˜π‘))))
4030ackbij1b 10248 . . . . . . . . . 10 ((cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰ β†’ (𝐹 β€œ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) = (cardβ€˜π’« (cardβ€˜(𝑅1β€˜π‘))))
4135, 40syl 17 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ (𝐹 β€œ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) = (cardβ€˜π’« (cardβ€˜(𝑅1β€˜π‘))))
42 ficardid 9971 . . . . . . . . . 10 ((𝑅1β€˜π‘) ∈ Fin β†’ (cardβ€˜(𝑅1β€˜π‘)) β‰ˆ (𝑅1β€˜π‘))
43 pwen 9164 . . . . . . . . . 10 ((cardβ€˜(𝑅1β€˜π‘)) β‰ˆ (𝑅1β€˜π‘) β†’ 𝒫 (cardβ€˜(𝑅1β€˜π‘)) β‰ˆ 𝒫 (𝑅1β€˜π‘))
44 carden2b 9976 . . . . . . . . . 10 (𝒫 (cardβ€˜(𝑅1β€˜π‘)) β‰ˆ 𝒫 (𝑅1β€˜π‘) β†’ (cardβ€˜π’« (cardβ€˜(𝑅1β€˜π‘))) = (cardβ€˜π’« (𝑅1β€˜π‘)))
4533, 42, 43, 444syl 19 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ (cardβ€˜π’« (cardβ€˜(𝑅1β€˜π‘))) = (cardβ€˜π’« (𝑅1β€˜π‘)))
4641, 45eqtrd 2767 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ (𝐹 β€œ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) = (cardβ€˜π’« (𝑅1β€˜π‘)))
4746f1oeq3d 6830 . . . . . . 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 480 . . . . 5 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))):𝒫 (cardβ€˜(𝑅1β€˜π‘))–1-1-ontoβ†’(cardβ€˜π’« (𝑅1β€˜π‘)))
50 f1opw 7669 . . . . . 6 ((rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘)) β†’ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž)):𝒫 (𝑅1β€˜π‘)–1-1-onto→𝒫 (cardβ€˜(𝑅1β€˜π‘)))
5150adantl 481 . . . . 5 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž)):𝒫 (𝑅1β€˜π‘)–1-1-onto→𝒫 (cardβ€˜(𝑅1β€˜π‘)))
52 f1oco 6856 . . . . 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 583 . . . 4 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))):𝒫 (𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜π’« (𝑅1β€˜π‘)))
54 frsuc 8449 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ ((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜suc 𝑏) = (πΊβ€˜((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜π‘)))
55 peano2 7888 . . . . . . . . . 10 (𝑏 ∈ Ο‰ β†’ suc 𝑏 ∈ Ο‰)
5655fvresd 6911 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ ((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜suc 𝑏) = (rec(𝐺, βˆ…)β€˜suc 𝑏))
57 fvres 6910 . . . . . . . . . . 11 (𝑏 ∈ Ο‰ β†’ ((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜π‘) = (rec(𝐺, βˆ…)β€˜π‘))
5857fveq2d 6895 . . . . . . . . . 10 (𝑏 ∈ Ο‰ β†’ (πΊβ€˜((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜π‘)) = (πΊβ€˜(rec(𝐺, βˆ…)β€˜π‘)))
59 fvex 6904 . . . . . . . . . . 11 (rec(𝐺, βˆ…)β€˜π‘) ∈ V
60 dmeq 5900 . . . . . . . . . . . . . 14 (π‘₯ = (rec(𝐺, βˆ…)β€˜π‘) β†’ dom π‘₯ = dom (rec(𝐺, βˆ…)β€˜π‘))
6160pweqd 4615 . . . . . . . . . . . . 13 (π‘₯ = (rec(𝐺, βˆ…)β€˜π‘) β†’ 𝒫 dom π‘₯ = 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘))
62 imaeq1 6052 . . . . . . . . . . . . . 14 (π‘₯ = (rec(𝐺, βˆ…)β€˜π‘) β†’ (π‘₯ β€œ 𝑦) = ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))
6362fveq2d 6895 . . . . . . . . . . . . 13 (π‘₯ = (rec(𝐺, βˆ…)β€˜π‘) β†’ (πΉβ€˜(π‘₯ β€œ 𝑦)) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))
6461, 63mpteq12dv 5233 . . . . . . . . . . . 12 (π‘₯ = (rec(𝐺, βˆ…)β€˜π‘) β†’ (𝑦 ∈ 𝒫 dom π‘₯ ↦ (πΉβ€˜(π‘₯ β€œ 𝑦))) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
65 ackbij.g . . . . . . . . . . . 12 𝐺 = (π‘₯ ∈ V ↦ (𝑦 ∈ 𝒫 dom π‘₯ ↦ (πΉβ€˜(π‘₯ β€œ 𝑦))))
6659dmex 7909 . . . . . . . . . . . . . 14 dom (rec(𝐺, βˆ…)β€˜π‘) ∈ V
6766pwex 5374 . . . . . . . . . . . . 13 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ∈ V
6867mptex 7229 . . . . . . . . . . . 12 (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) ∈ V
6964, 65, 68fvmpt 6999 . . . . . . . . . . 11 ((rec(𝐺, βˆ…)β€˜π‘) ∈ V β†’ (πΊβ€˜(rec(𝐺, βˆ…)β€˜π‘)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
7059, 69ax-mp 5 . . . . . . . . . 10 (πΊβ€˜(rec(𝐺, βˆ…)β€˜π‘)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))
7158, 70eqtrdi 2783 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ (πΊβ€˜((rec(𝐺, βˆ…) β†Ύ Ο‰)β€˜π‘)) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
7254, 56, 713eqtr3d 2775 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
7372adantr 480 . . . . . . 7 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏) = (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
74 f1odm 6837 . . . . . . . . . . 11 ((rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘)) β†’ dom (rec(𝐺, βˆ…)β€˜π‘) = (𝑅1β€˜π‘))
7574adantl 481 . . . . . . . . . 10 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ dom (rec(𝐺, βˆ…)β€˜π‘) = (𝑅1β€˜π‘))
7675pweqd 4615 . . . . . . . . 9 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) = 𝒫 (𝑅1β€˜π‘))
7776mpteq1d 5237 . . . . . . . 8 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) = (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))))
78 fvex 6904 . . . . . . . . . . 11 (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)) ∈ V
79 eqid 2727 . . . . . . . . . . 11 (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) = (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))
8078, 79fnmpti 6692 . . . . . . . . . 10 (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) Fn 𝒫 (𝑅1β€˜π‘)
8180a1i 11 . . . . . . . . 9 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) Fn 𝒫 (𝑅1β€˜π‘))
82 f1ofn 6834 . . . . . . . . . 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 6833 . . . . . . . . . . . . . 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 7088 . . . . . . . . . . . 12 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘) ∈ 𝒫 (cardβ€˜(𝑅1β€˜π‘)))
8786fvresd 6911 . . . . . . . . . . 11 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘)))β€˜((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘)) = (πΉβ€˜((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘)))
88 imaeq2 6053 . . . . . . . . . . . . . 14 (π‘Ž = 𝑐 β†’ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž) = ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐))
89 eqid 2727 . . . . . . . . . . . . . 14 (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž)) = (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))
9059imaex 7914 . . . . . . . . . . . . . 14 ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐) ∈ V
9188, 89, 90fvmpt 6999 . . . . . . . . . . . . 13 (𝑐 ∈ 𝒫 (𝑅1β€˜π‘) β†’ ((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘) = ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐))
9291adantl 481 . . . . . . . . . . . 12 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘) = ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐))
9392fveq2d 6895 . . . . . . . . . . 11 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ (πΉβ€˜((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘)) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)))
9487, 93eqtrd 2767 . . . . . . . . . 10 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘)))β€˜((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘)) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)))
95 fvco3 6991 . . . . . . . . . . 11 (((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž)):𝒫 (𝑅1β€˜π‘)βŸΆπ’« (cardβ€˜(𝑅1β€˜π‘)) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ (((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž)))β€˜π‘) = ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘)))β€˜((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘)))
9685, 95sylan 579 . . . . . . . . . 10 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ (((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž)))β€˜π‘) = ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘)))β€˜((π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))β€˜π‘)))
97 imaeq2 6053 . . . . . . . . . . . . 13 (𝑦 = 𝑐 β†’ ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦) = ((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐))
9897fveq2d 6895 . . . . . . . . . . . 12 (𝑦 = 𝑐 β†’ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)))
99 fvex 6904 . . . . . . . . . . . 12 (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)) ∈ V
10098, 79, 99fvmpt 6999 . . . . . . . . . . 11 (𝑐 ∈ 𝒫 (𝑅1β€˜π‘) β†’ ((𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))β€˜π‘) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)))
101100adantl 481 . . . . . . . . . 10 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))β€˜π‘) = (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑐)))
10294, 96, 1013eqtr4rd 2778 . . . . . . . . 9 (((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) ∧ 𝑐 ∈ 𝒫 (𝑅1β€˜π‘)) β†’ ((𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦)))β€˜π‘) = (((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž)))β€˜π‘))
10381, 83, 102eqfnfvd 7037 . . . . . . . 8 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (𝑦 ∈ 𝒫 (𝑅1β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) = ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))))
10477, 103eqtrd 2767 . . . . . . 7 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (𝑦 ∈ 𝒫 dom (rec(𝐺, βˆ…)β€˜π‘) ↦ (πΉβ€˜((rec(𝐺, βˆ…)β€˜π‘) β€œ 𝑦))) = ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))))
10573, 104eqtrd 2767 . . . . . 6 ((𝑏 ∈ Ο‰ ∧ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘))) β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏) = ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))))
106 f1oeq1 6821 . . . . . 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 7868 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ 𝑏 ∈ On)
109 r1suc 9779 . . . . . . . 8 (𝑏 ∈ On β†’ (𝑅1β€˜suc 𝑏) = 𝒫 (𝑅1β€˜π‘))
110108, 109syl 17 . . . . . . 7 (𝑏 ∈ Ο‰ β†’ (𝑅1β€˜suc 𝑏) = 𝒫 (𝑅1β€˜π‘))
111110fveq2d 6895 . . . . . . 7 (𝑏 ∈ Ο‰ β†’ (cardβ€˜(𝑅1β€˜suc 𝑏)) = (cardβ€˜π’« (𝑅1β€˜π‘)))
112 f1oeq23 6824 . . . . . . 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 583 . . . . . 6 (𝑏 ∈ Ο‰ β†’ (((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))):(𝑅1β€˜suc 𝑏)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜suc 𝑏)) ↔ ((𝐹 β†Ύ 𝒫 (cardβ€˜(𝑅1β€˜π‘))) ∘ (π‘Ž ∈ 𝒫 (𝑅1β€˜π‘) ↦ ((rec(𝐺, βˆ…)β€˜π‘) β€œ π‘Ž))):𝒫 (𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜π’« (𝑅1β€˜π‘))))
114113adantr 480 . . . . 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 412 . 2 (𝑏 ∈ Ο‰ β†’ ((rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘)) β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏):(𝑅1β€˜suc 𝑏)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜suc 𝑏))))
1184, 8, 12, 16, 29, 117finds 7896 1 (𝐴 ∈ Ο‰ β†’ (rec(𝐺, βˆ…)β€˜π΄):(𝑅1β€˜π΄)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π΄)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534   ∈ wcel 2099  Vcvv 3469   ∩ cin 3943   βŠ† wss 3944  βˆ…c0 4318  π’« cpw 4598  {csn 4624  βˆͺ ciun 4991   class class class wbr 5142   ↦ cmpt 5225   Γ— cxp 5670  dom cdm 5672   β†Ύ cres 5674   β€œ cima 5675   ∘ ccom 5676  Oncon0 6363  suc csuc 6365   Fn wfn 6537  βŸΆwf 6538  β€“1-1β†’wf1 6539  β€“1-1-ontoβ†’wf1o 6541  β€˜cfv 6542  Ο‰com 7862  reccrdg 8421   β‰ˆ cen 8950  Fincfn 8953  π‘…1cr1 9771  cardccrd 9944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7732
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7863  df-1st 7985  df-2nd 7986  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-2o 8479  df-oadd 8482  df-er 8716  df-map 8836  df-en 8954  df-dom 8955  df-sdom 8956  df-fin 8957  df-r1 9773  df-dju 9910  df-card 9948
This theorem is referenced by:  ackbij2lem3  10250  ackbij2  10252
  Copyright terms: Public domain W3C validator