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

Theorem ackbij2 10238
Description: The Ackermann bijection, part 2: hereditarily finite sets can be represented by recursive binary notation. (Contributed by Stefan O'Rear, 18-Nov-2014.)
Hypotheses
Ref Expression
ackbij.f 𝐹 = (π‘₯ ∈ (𝒫 Ο‰ ∩ Fin) ↦ (cardβ€˜βˆͺ 𝑦 ∈ π‘₯ ({𝑦} Γ— 𝒫 𝑦)))
ackbij.g 𝐺 = (π‘₯ ∈ V ↦ (𝑦 ∈ 𝒫 dom π‘₯ ↦ (πΉβ€˜(π‘₯ β€œ 𝑦))))
ackbij.h 𝐻 = βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰)
Assertion
Ref Expression
ackbij2 𝐻:βˆͺ (𝑅1 β€œ Ο‰)–1-1-ontoβ†’Ο‰
Distinct variable groups:   π‘₯,𝐹,𝑦   π‘₯,𝐺,𝑦   π‘₯,𝐻,𝑦

Proof of Theorem ackbij2
Dummy variables π‘Ž 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6892 . . . . . 6 (π‘Ž = 𝑏 β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) = (rec(𝐺, βˆ…)β€˜π‘))
2 fvex 6905 . . . . . 6 (rec(𝐺, βˆ…)β€˜π‘Ž) ∈ V
31, 2f1iun 7930 . . . . 5 (βˆ€π‘Ž ∈ Ο‰ ((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1β†’Ο‰ ∧ βˆ€π‘ ∈ Ο‰ ((rec(𝐺, βˆ…)β€˜π‘Ž) βŠ† (rec(𝐺, βˆ…)β€˜π‘) ∨ (rec(𝐺, βˆ…)β€˜π‘) βŠ† (rec(𝐺, βˆ…)β€˜π‘Ž))) β†’ βˆͺ π‘Ž ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘Ž):βˆͺ π‘Ž ∈ Ο‰ (𝑅1β€˜π‘Ž)–1-1β†’Ο‰)
4 ackbij.f . . . . . . . . 9 𝐹 = (π‘₯ ∈ (𝒫 Ο‰ ∩ Fin) ↦ (cardβ€˜βˆͺ 𝑦 ∈ π‘₯ ({𝑦} Γ— 𝒫 𝑦)))
5 ackbij.g . . . . . . . . 9 𝐺 = (π‘₯ ∈ V ↦ (𝑦 ∈ 𝒫 dom π‘₯ ↦ (πΉβ€˜(π‘₯ β€œ 𝑦))))
64, 5ackbij2lem2 10235 . . . . . . . 8 (π‘Ž ∈ Ο‰ β†’ (rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘Ž)))
7 f1of1 6833 . . . . . . . 8 ((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘Ž)) β†’ (rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1β†’(cardβ€˜(𝑅1β€˜π‘Ž)))
86, 7syl 17 . . . . . . 7 (π‘Ž ∈ Ο‰ β†’ (rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1β†’(cardβ€˜(𝑅1β€˜π‘Ž)))
9 ordom 7865 . . . . . . . 8 Ord Ο‰
10 r1fin 9768 . . . . . . . . 9 (π‘Ž ∈ Ο‰ β†’ (𝑅1β€˜π‘Ž) ∈ Fin)
11 ficardom 9956 . . . . . . . . 9 ((𝑅1β€˜π‘Ž) ∈ Fin β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) ∈ Ο‰)
1210, 11syl 17 . . . . . . . 8 (π‘Ž ∈ Ο‰ β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) ∈ Ο‰)
13 ordelss 6381 . . . . . . . 8 ((Ord Ο‰ ∧ (cardβ€˜(𝑅1β€˜π‘Ž)) ∈ Ο‰) β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) βŠ† Ο‰)
149, 12, 13sylancr 588 . . . . . . 7 (π‘Ž ∈ Ο‰ β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) βŠ† Ο‰)
15 f1ss 6794 . . . . . . 7 (((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1β†’(cardβ€˜(𝑅1β€˜π‘Ž)) ∧ (cardβ€˜(𝑅1β€˜π‘Ž)) βŠ† Ο‰) β†’ (rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1β†’Ο‰)
168, 14, 15syl2anc 585 . . . . . 6 (π‘Ž ∈ Ο‰ β†’ (rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1β†’Ο‰)
17 nnord 7863 . . . . . . . . 9 (π‘Ž ∈ Ο‰ β†’ Ord π‘Ž)
18 nnord 7863 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ Ord 𝑏)
19 ordtri2or2 6464 . . . . . . . . 9 ((Ord π‘Ž ∧ Ord 𝑏) β†’ (π‘Ž βŠ† 𝑏 ∨ 𝑏 βŠ† π‘Ž))
2017, 18, 19syl2an 597 . . . . . . . 8 ((π‘Ž ∈ Ο‰ ∧ 𝑏 ∈ Ο‰) β†’ (π‘Ž βŠ† 𝑏 ∨ 𝑏 βŠ† π‘Ž))
214, 5ackbij2lem4 10237 . . . . . . . . . . 11 (((𝑏 ∈ Ο‰ ∧ π‘Ž ∈ Ο‰) ∧ π‘Ž βŠ† 𝑏) β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) βŠ† (rec(𝐺, βˆ…)β€˜π‘))
2221ex 414 . . . . . . . . . 10 ((𝑏 ∈ Ο‰ ∧ π‘Ž ∈ Ο‰) β†’ (π‘Ž βŠ† 𝑏 β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) βŠ† (rec(𝐺, βˆ…)β€˜π‘)))
2322ancoms 460 . . . . . . . . 9 ((π‘Ž ∈ Ο‰ ∧ 𝑏 ∈ Ο‰) β†’ (π‘Ž βŠ† 𝑏 β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) βŠ† (rec(𝐺, βˆ…)β€˜π‘)))
244, 5ackbij2lem4 10237 . . . . . . . . . 10 (((π‘Ž ∈ Ο‰ ∧ 𝑏 ∈ Ο‰) ∧ 𝑏 βŠ† π‘Ž) β†’ (rec(𝐺, βˆ…)β€˜π‘) βŠ† (rec(𝐺, βˆ…)β€˜π‘Ž))
2524ex 414 . . . . . . . . 9 ((π‘Ž ∈ Ο‰ ∧ 𝑏 ∈ Ο‰) β†’ (𝑏 βŠ† π‘Ž β†’ (rec(𝐺, βˆ…)β€˜π‘) βŠ† (rec(𝐺, βˆ…)β€˜π‘Ž)))
2623, 25orim12d 964 . . . . . . . 8 ((π‘Ž ∈ Ο‰ ∧ 𝑏 ∈ Ο‰) β†’ ((π‘Ž βŠ† 𝑏 ∨ 𝑏 βŠ† π‘Ž) β†’ ((rec(𝐺, βˆ…)β€˜π‘Ž) βŠ† (rec(𝐺, βˆ…)β€˜π‘) ∨ (rec(𝐺, βˆ…)β€˜π‘) βŠ† (rec(𝐺, βˆ…)β€˜π‘Ž))))
2720, 26mpd 15 . . . . . . 7 ((π‘Ž ∈ Ο‰ ∧ 𝑏 ∈ Ο‰) β†’ ((rec(𝐺, βˆ…)β€˜π‘Ž) βŠ† (rec(𝐺, βˆ…)β€˜π‘) ∨ (rec(𝐺, βˆ…)β€˜π‘) βŠ† (rec(𝐺, βˆ…)β€˜π‘Ž)))
2827ralrimiva 3147 . . . . . 6 (π‘Ž ∈ Ο‰ β†’ βˆ€π‘ ∈ Ο‰ ((rec(𝐺, βˆ…)β€˜π‘Ž) βŠ† (rec(𝐺, βˆ…)β€˜π‘) ∨ (rec(𝐺, βˆ…)β€˜π‘) βŠ† (rec(𝐺, βˆ…)β€˜π‘Ž)))
2916, 28jca 513 . . . . 5 (π‘Ž ∈ Ο‰ β†’ ((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1β†’Ο‰ ∧ βˆ€π‘ ∈ Ο‰ ((rec(𝐺, βˆ…)β€˜π‘Ž) βŠ† (rec(𝐺, βˆ…)β€˜π‘) ∨ (rec(𝐺, βˆ…)β€˜π‘) βŠ† (rec(𝐺, βˆ…)β€˜π‘Ž))))
303, 29mprg 3068 . . . 4 βˆͺ π‘Ž ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘Ž):βˆͺ π‘Ž ∈ Ο‰ (𝑅1β€˜π‘Ž)–1-1β†’Ο‰
31 rdgfun 8416 . . . . . 6 Fun rec(𝐺, βˆ…)
32 funiunfv 7247 . . . . . . 7 (Fun rec(𝐺, βˆ…) β†’ βˆͺ π‘Ž ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘Ž) = βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰))
3332eqcomd 2739 . . . . . 6 (Fun rec(𝐺, βˆ…) β†’ βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰) = βˆͺ π‘Ž ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘Ž))
34 f1eq1 6783 . . . . . 6 (βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰) = βˆͺ π‘Ž ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘Ž) β†’ (βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰):βˆͺ (𝑅1 β€œ Ο‰)–1-1β†’Ο‰ ↔ βˆͺ π‘Ž ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘Ž):βˆͺ (𝑅1 β€œ Ο‰)–1-1β†’Ο‰))
3531, 33, 34mp2b 10 . . . . 5 (βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰):βˆͺ (𝑅1 β€œ Ο‰)–1-1β†’Ο‰ ↔ βˆͺ π‘Ž ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘Ž):βˆͺ (𝑅1 β€œ Ο‰)–1-1β†’Ο‰)
36 r1funlim 9761 . . . . . . 7 (Fun 𝑅1 ∧ Lim dom 𝑅1)
3736simpli 485 . . . . . 6 Fun 𝑅1
38 funiunfv 7247 . . . . . 6 (Fun 𝑅1 β†’ βˆͺ π‘Ž ∈ Ο‰ (𝑅1β€˜π‘Ž) = βˆͺ (𝑅1 β€œ Ο‰))
39 f1eq2 6784 . . . . . 6 (βˆͺ π‘Ž ∈ Ο‰ (𝑅1β€˜π‘Ž) = βˆͺ (𝑅1 β€œ Ο‰) β†’ (βˆͺ π‘Ž ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘Ž):βˆͺ π‘Ž ∈ Ο‰ (𝑅1β€˜π‘Ž)–1-1β†’Ο‰ ↔ βˆͺ π‘Ž ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘Ž):βˆͺ (𝑅1 β€œ Ο‰)–1-1β†’Ο‰))
4037, 38, 39mp2b 10 . . . . 5 (βˆͺ π‘Ž ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘Ž):βˆͺ π‘Ž ∈ Ο‰ (𝑅1β€˜π‘Ž)–1-1β†’Ο‰ ↔ βˆͺ π‘Ž ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘Ž):βˆͺ (𝑅1 β€œ Ο‰)–1-1β†’Ο‰)
4135, 40bitr4i 278 . . . 4 (βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰):βˆͺ (𝑅1 β€œ Ο‰)–1-1β†’Ο‰ ↔ βˆͺ π‘Ž ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘Ž):βˆͺ π‘Ž ∈ Ο‰ (𝑅1β€˜π‘Ž)–1-1β†’Ο‰)
4230, 41mpbir 230 . . 3 βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰):βˆͺ (𝑅1 β€œ Ο‰)–1-1β†’Ο‰
43 rnuni 6149 . . . 4 ran βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰) = βˆͺ π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰)ran π‘Ž
44 eliun 5002 . . . . . 6 (𝑏 ∈ βˆͺ π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰)ran π‘Ž ↔ βˆƒπ‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰)𝑏 ∈ ran π‘Ž)
45 df-rex 3072 . . . . . 6 (βˆƒπ‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰)𝑏 ∈ ran π‘Ž ↔ βˆƒπ‘Ž(π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ∧ 𝑏 ∈ ran π‘Ž))
46 funfn 6579 . . . . . . . . . . . 12 (Fun rec(𝐺, βˆ…) ↔ rec(𝐺, βˆ…) Fn dom rec(𝐺, βˆ…))
4731, 46mpbi 229 . . . . . . . . . . 11 rec(𝐺, βˆ…) Fn dom rec(𝐺, βˆ…)
48 rdgdmlim 8417 . . . . . . . . . . . 12 Lim dom rec(𝐺, βˆ…)
49 limomss 7860 . . . . . . . . . . . 12 (Lim dom rec(𝐺, βˆ…) β†’ Ο‰ βŠ† dom rec(𝐺, βˆ…))
5048, 49ax-mp 5 . . . . . . . . . . 11 Ο‰ βŠ† dom rec(𝐺, βˆ…)
51 fvelimab 6965 . . . . . . . . . . 11 ((rec(𝐺, βˆ…) Fn dom rec(𝐺, βˆ…) ∧ Ο‰ βŠ† dom rec(𝐺, βˆ…)) β†’ (π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ↔ βˆƒπ‘ ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘) = π‘Ž))
5247, 50, 51mp2an 691 . . . . . . . . . 10 (π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ↔ βˆƒπ‘ ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘) = π‘Ž)
534, 5ackbij2lem2 10235 . . . . . . . . . . . . . 14 (𝑐 ∈ Ο‰ β†’ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘)))
54 f1ofo 6841 . . . . . . . . . . . . . 14 ((rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘)) β†’ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–ontoβ†’(cardβ€˜(𝑅1β€˜π‘)))
55 forn 6809 . . . . . . . . . . . . . 14 ((rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–ontoβ†’(cardβ€˜(𝑅1β€˜π‘)) β†’ ran (rec(𝐺, βˆ…)β€˜π‘) = (cardβ€˜(𝑅1β€˜π‘)))
5653, 54, 553syl 18 . . . . . . . . . . . . 13 (𝑐 ∈ Ο‰ β†’ ran (rec(𝐺, βˆ…)β€˜π‘) = (cardβ€˜(𝑅1β€˜π‘)))
57 r1fin 9768 . . . . . . . . . . . . . . 15 (𝑐 ∈ Ο‰ β†’ (𝑅1β€˜π‘) ∈ Fin)
58 ficardom 9956 . . . . . . . . . . . . . . 15 ((𝑅1β€˜π‘) ∈ Fin β†’ (cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰)
5957, 58syl 17 . . . . . . . . . . . . . 14 (𝑐 ∈ Ο‰ β†’ (cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰)
60 ordelss 6381 . . . . . . . . . . . . . 14 ((Ord Ο‰ ∧ (cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰) β†’ (cardβ€˜(𝑅1β€˜π‘)) βŠ† Ο‰)
619, 59, 60sylancr 588 . . . . . . . . . . . . 13 (𝑐 ∈ Ο‰ β†’ (cardβ€˜(𝑅1β€˜π‘)) βŠ† Ο‰)
6256, 61eqsstrd 4021 . . . . . . . . . . . 12 (𝑐 ∈ Ο‰ β†’ ran (rec(𝐺, βˆ…)β€˜π‘) βŠ† Ο‰)
63 rneq 5936 . . . . . . . . . . . . 13 ((rec(𝐺, βˆ…)β€˜π‘) = π‘Ž β†’ ran (rec(𝐺, βˆ…)β€˜π‘) = ran π‘Ž)
6463sseq1d 4014 . . . . . . . . . . . 12 ((rec(𝐺, βˆ…)β€˜π‘) = π‘Ž β†’ (ran (rec(𝐺, βˆ…)β€˜π‘) βŠ† Ο‰ ↔ ran π‘Ž βŠ† Ο‰))
6562, 64syl5ibcom 244 . . . . . . . . . . 11 (𝑐 ∈ Ο‰ β†’ ((rec(𝐺, βˆ…)β€˜π‘) = π‘Ž β†’ ran π‘Ž βŠ† Ο‰))
6665rexlimiv 3149 . . . . . . . . . 10 (βˆƒπ‘ ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘) = π‘Ž β†’ ran π‘Ž βŠ† Ο‰)
6752, 66sylbi 216 . . . . . . . . 9 (π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) β†’ ran π‘Ž βŠ† Ο‰)
6867sselda 3983 . . . . . . . 8 ((π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ∧ 𝑏 ∈ ran π‘Ž) β†’ 𝑏 ∈ Ο‰)
6968exlimiv 1934 . . . . . . 7 (βˆƒπ‘Ž(π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ∧ 𝑏 ∈ ran π‘Ž) β†’ 𝑏 ∈ Ο‰)
70 peano2 7881 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ suc 𝑏 ∈ Ο‰)
71 fnfvima 7235 . . . . . . . . 9 ((rec(𝐺, βˆ…) Fn dom rec(𝐺, βˆ…) ∧ Ο‰ βŠ† dom rec(𝐺, βˆ…) ∧ suc 𝑏 ∈ Ο‰) β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏) ∈ (rec(𝐺, βˆ…) β€œ Ο‰))
7247, 50, 70, 71mp3an12i 1466 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏) ∈ (rec(𝐺, βˆ…) β€œ Ο‰))
73 vex 3479 . . . . . . . . . 10 𝑏 ∈ V
74 cardnn 9958 . . . . . . . . . . . 12 (suc 𝑏 ∈ Ο‰ β†’ (cardβ€˜suc 𝑏) = suc 𝑏)
75 fvex 6905 . . . . . . . . . . . . . 14 (𝑅1β€˜suc 𝑏) ∈ V
7636simpri 487 . . . . . . . . . . . . . . . . 17 Lim dom 𝑅1
77 limomss 7860 . . . . . . . . . . . . . . . . 17 (Lim dom 𝑅1 β†’ Ο‰ βŠ† dom 𝑅1)
7876, 77ax-mp 5 . . . . . . . . . . . . . . . 16 Ο‰ βŠ† dom 𝑅1
7978sseli 3979 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ Ο‰ β†’ suc 𝑏 ∈ dom 𝑅1)
80 onssr1 9826 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ dom 𝑅1 β†’ suc 𝑏 βŠ† (𝑅1β€˜suc 𝑏))
8179, 80syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ Ο‰ β†’ suc 𝑏 βŠ† (𝑅1β€˜suc 𝑏))
82 ssdomg 8996 . . . . . . . . . . . . . 14 ((𝑅1β€˜suc 𝑏) ∈ V β†’ (suc 𝑏 βŠ† (𝑅1β€˜suc 𝑏) β†’ suc 𝑏 β‰Ό (𝑅1β€˜suc 𝑏)))
8375, 81, 82mpsyl 68 . . . . . . . . . . . . 13 (suc 𝑏 ∈ Ο‰ β†’ suc 𝑏 β‰Ό (𝑅1β€˜suc 𝑏))
84 nnon 7861 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ Ο‰ β†’ suc 𝑏 ∈ On)
85 onenon 9944 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ On β†’ suc 𝑏 ∈ dom card)
8684, 85syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ Ο‰ β†’ suc 𝑏 ∈ dom card)
87 r1fin 9768 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ Ο‰ β†’ (𝑅1β€˜suc 𝑏) ∈ Fin)
88 finnum 9943 . . . . . . . . . . . . . . 15 ((𝑅1β€˜suc 𝑏) ∈ Fin β†’ (𝑅1β€˜suc 𝑏) ∈ dom card)
8987, 88syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ Ο‰ β†’ (𝑅1β€˜suc 𝑏) ∈ dom card)
90 carddom2 9972 . . . . . . . . . . . . . 14 ((suc 𝑏 ∈ dom card ∧ (𝑅1β€˜suc 𝑏) ∈ dom card) β†’ ((cardβ€˜suc 𝑏) βŠ† (cardβ€˜(𝑅1β€˜suc 𝑏)) ↔ suc 𝑏 β‰Ό (𝑅1β€˜suc 𝑏)))
9186, 89, 90syl2anc 585 . . . . . . . . . . . . 13 (suc 𝑏 ∈ Ο‰ β†’ ((cardβ€˜suc 𝑏) βŠ† (cardβ€˜(𝑅1β€˜suc 𝑏)) ↔ suc 𝑏 β‰Ό (𝑅1β€˜suc 𝑏)))
9283, 91mpbird 257 . . . . . . . . . . . 12 (suc 𝑏 ∈ Ο‰ β†’ (cardβ€˜suc 𝑏) βŠ† (cardβ€˜(𝑅1β€˜suc 𝑏)))
9374, 92eqsstrrd 4022 . . . . . . . . . . 11 (suc 𝑏 ∈ Ο‰ β†’ suc 𝑏 βŠ† (cardβ€˜(𝑅1β€˜suc 𝑏)))
9470, 93syl 17 . . . . . . . . . 10 (𝑏 ∈ Ο‰ β†’ suc 𝑏 βŠ† (cardβ€˜(𝑅1β€˜suc 𝑏)))
95 sucssel 6460 . . . . . . . . . 10 (𝑏 ∈ V β†’ (suc 𝑏 βŠ† (cardβ€˜(𝑅1β€˜suc 𝑏)) β†’ 𝑏 ∈ (cardβ€˜(𝑅1β€˜suc 𝑏))))
9673, 94, 95mpsyl 68 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ 𝑏 ∈ (cardβ€˜(𝑅1β€˜suc 𝑏)))
974, 5ackbij2lem2 10235 . . . . . . . . . 10 (suc 𝑏 ∈ Ο‰ β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏):(𝑅1β€˜suc 𝑏)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜suc 𝑏)))
98 f1ofo 6841 . . . . . . . . . 10 ((rec(𝐺, βˆ…)β€˜suc 𝑏):(𝑅1β€˜suc 𝑏)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜suc 𝑏)) β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏):(𝑅1β€˜suc 𝑏)–ontoβ†’(cardβ€˜(𝑅1β€˜suc 𝑏)))
99 forn 6809 . . . . . . . . . 10 ((rec(𝐺, βˆ…)β€˜suc 𝑏):(𝑅1β€˜suc 𝑏)–ontoβ†’(cardβ€˜(𝑅1β€˜suc 𝑏)) β†’ ran (rec(𝐺, βˆ…)β€˜suc 𝑏) = (cardβ€˜(𝑅1β€˜suc 𝑏)))
10070, 97, 98, 994syl 19 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ ran (rec(𝐺, βˆ…)β€˜suc 𝑏) = (cardβ€˜(𝑅1β€˜suc 𝑏)))
10196, 100eleqtrrd 2837 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ 𝑏 ∈ ran (rec(𝐺, βˆ…)β€˜suc 𝑏))
102 fvex 6905 . . . . . . . . 9 (rec(𝐺, βˆ…)β€˜suc 𝑏) ∈ V
103 eleq1 2822 . . . . . . . . . 10 (π‘Ž = (rec(𝐺, βˆ…)β€˜suc 𝑏) β†’ (π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ↔ (rec(𝐺, βˆ…)β€˜suc 𝑏) ∈ (rec(𝐺, βˆ…) β€œ Ο‰)))
104 rneq 5936 . . . . . . . . . . 11 (π‘Ž = (rec(𝐺, βˆ…)β€˜suc 𝑏) β†’ ran π‘Ž = ran (rec(𝐺, βˆ…)β€˜suc 𝑏))
105104eleq2d 2820 . . . . . . . . . 10 (π‘Ž = (rec(𝐺, βˆ…)β€˜suc 𝑏) β†’ (𝑏 ∈ ran π‘Ž ↔ 𝑏 ∈ ran (rec(𝐺, βˆ…)β€˜suc 𝑏)))
106103, 105anbi12d 632 . . . . . . . . 9 (π‘Ž = (rec(𝐺, βˆ…)β€˜suc 𝑏) β†’ ((π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ∧ 𝑏 ∈ ran π‘Ž) ↔ ((rec(𝐺, βˆ…)β€˜suc 𝑏) ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ∧ 𝑏 ∈ ran (rec(𝐺, βˆ…)β€˜suc 𝑏))))
107102, 106spcev 3597 . . . . . . . 8 (((rec(𝐺, βˆ…)β€˜suc 𝑏) ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ∧ 𝑏 ∈ ran (rec(𝐺, βˆ…)β€˜suc 𝑏)) β†’ βˆƒπ‘Ž(π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ∧ 𝑏 ∈ ran π‘Ž))
10872, 101, 107syl2anc 585 . . . . . . 7 (𝑏 ∈ Ο‰ β†’ βˆƒπ‘Ž(π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ∧ 𝑏 ∈ ran π‘Ž))
10969, 108impbii 208 . . . . . 6 (βˆƒπ‘Ž(π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ∧ 𝑏 ∈ ran π‘Ž) ↔ 𝑏 ∈ Ο‰)
11044, 45, 1093bitri 297 . . . . 5 (𝑏 ∈ βˆͺ π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰)ran π‘Ž ↔ 𝑏 ∈ Ο‰)
111110eqriv 2730 . . . 4 βˆͺ π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰)ran π‘Ž = Ο‰
11243, 111eqtri 2761 . . 3 ran βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰) = Ο‰
113 dff1o5 6843 . . 3 (βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰):βˆͺ (𝑅1 β€œ Ο‰)–1-1-ontoβ†’Ο‰ ↔ (βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰):βˆͺ (𝑅1 β€œ Ο‰)–1-1β†’Ο‰ ∧ ran βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰) = Ο‰))
11442, 112, 113mpbir2an 710 . 2 βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰):βˆͺ (𝑅1 β€œ Ο‰)–1-1-ontoβ†’Ο‰
115 ackbij.h . . 3 𝐻 = βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰)
116 f1oeq1 6822 . . 3 (𝐻 = βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰) β†’ (𝐻:βˆͺ (𝑅1 β€œ Ο‰)–1-1-ontoβ†’Ο‰ ↔ βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰):βˆͺ (𝑅1 β€œ Ο‰)–1-1-ontoβ†’Ο‰))
117115, 116ax-mp 5 . 2 (𝐻:βˆͺ (𝑅1 β€œ Ο‰)–1-1-ontoβ†’Ο‰ ↔ βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰):βˆͺ (𝑅1 β€œ Ο‰)–1-1-ontoβ†’Ο‰)
118114, 117mpbir 230 1 𝐻:βˆͺ (𝑅1 β€œ Ο‰)–1-1-ontoβ†’Ο‰
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  π’« cpw 4603  {csn 4629  βˆͺ cuni 4909  βˆͺ ciun 4998   class class class wbr 5149   ↦ cmpt 5232   Γ— cxp 5675  dom cdm 5677  ran crn 5678   β€œ cima 5680  Ord word 6364  Oncon0 6365  Lim wlim 6366  suc csuc 6367  Fun wfun 6538   Fn wfn 6539  β€“1-1β†’wf1 6541  β€“ontoβ†’wfo 6542  β€“1-1-ontoβ†’wf1o 6543  β€˜cfv 6544  Ο‰com 7855  reccrdg 8409   β‰Ό cdom 8937  Fincfn 8939  π‘…1cr1 9757  cardccrd 9930
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 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
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 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-oadd 8470  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-r1 9759  df-rank 9760  df-dju 9896  df-card 9934
This theorem is referenced by:  r1om  10239
  Copyright terms: Public domain W3C validator