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

Theorem ackbij2 10184
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 6843 . . . . . 6 (π‘Ž = 𝑏 β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) = (rec(𝐺, βˆ…)β€˜π‘))
2 fvex 6856 . . . . . 6 (rec(𝐺, βˆ…)β€˜π‘Ž) ∈ V
31, 2f1iun 7877 . . . . 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 10181 . . . . . . . 8 (π‘Ž ∈ Ο‰ β†’ (rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘Ž)))
7 f1of1 6784 . . . . . . . 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 7813 . . . . . . . 8 Ord Ο‰
10 r1fin 9714 . . . . . . . . 9 (π‘Ž ∈ Ο‰ β†’ (𝑅1β€˜π‘Ž) ∈ Fin)
11 ficardom 9902 . . . . . . . . 9 ((𝑅1β€˜π‘Ž) ∈ Fin β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) ∈ Ο‰)
1210, 11syl 17 . . . . . . . 8 (π‘Ž ∈ Ο‰ β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) ∈ Ο‰)
13 ordelss 6334 . . . . . . . 8 ((Ord Ο‰ ∧ (cardβ€˜(𝑅1β€˜π‘Ž)) ∈ Ο‰) β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) βŠ† Ο‰)
149, 12, 13sylancr 588 . . . . . . 7 (π‘Ž ∈ Ο‰ β†’ (cardβ€˜(𝑅1β€˜π‘Ž)) βŠ† Ο‰)
15 f1ss 6745 . . . . . . 7 (((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1β†’(cardβ€˜(𝑅1β€˜π‘Ž)) ∧ (cardβ€˜(𝑅1β€˜π‘Ž)) βŠ† Ο‰) β†’ (rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1β†’Ο‰)
168, 14, 15syl2anc 585 . . . . . 6 (π‘Ž ∈ Ο‰ β†’ (rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1β†’Ο‰)
17 nnord 7811 . . . . . . . . 9 (π‘Ž ∈ Ο‰ β†’ Ord π‘Ž)
18 nnord 7811 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ Ord 𝑏)
19 ordtri2or2 6417 . . . . . . . . 9 ((Ord π‘Ž ∧ Ord 𝑏) β†’ (π‘Ž βŠ† 𝑏 ∨ 𝑏 βŠ† π‘Ž))
2017, 18, 19syl2an 597 . . . . . . . 8 ((π‘Ž ∈ Ο‰ ∧ 𝑏 ∈ Ο‰) β†’ (π‘Ž βŠ† 𝑏 ∨ 𝑏 βŠ† π‘Ž))
214, 5ackbij2lem4 10183 . . . . . . . . . . 11 (((𝑏 ∈ Ο‰ ∧ π‘Ž ∈ Ο‰) ∧ π‘Ž βŠ† 𝑏) β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) βŠ† (rec(𝐺, βˆ…)β€˜π‘))
2221ex 414 . . . . . . . . . 10 ((𝑏 ∈ Ο‰ ∧ π‘Ž ∈ Ο‰) β†’ (π‘Ž βŠ† 𝑏 β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) βŠ† (rec(𝐺, βˆ…)β€˜π‘)))
2322ancoms 460 . . . . . . . . 9 ((π‘Ž ∈ Ο‰ ∧ 𝑏 ∈ Ο‰) β†’ (π‘Ž βŠ† 𝑏 β†’ (rec(𝐺, βˆ…)β€˜π‘Ž) βŠ† (rec(𝐺, βˆ…)β€˜π‘)))
244, 5ackbij2lem4 10183 . . . . . . . . . 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 3140 . . . . . 6 (π‘Ž ∈ Ο‰ β†’ βˆ€π‘ ∈ Ο‰ ((rec(𝐺, βˆ…)β€˜π‘Ž) βŠ† (rec(𝐺, βˆ…)β€˜π‘) ∨ (rec(𝐺, βˆ…)β€˜π‘) βŠ† (rec(𝐺, βˆ…)β€˜π‘Ž)))
2916, 28jca 513 . . . . 5 (π‘Ž ∈ Ο‰ β†’ ((rec(𝐺, βˆ…)β€˜π‘Ž):(𝑅1β€˜π‘Ž)–1-1β†’Ο‰ ∧ βˆ€π‘ ∈ Ο‰ ((rec(𝐺, βˆ…)β€˜π‘Ž) βŠ† (rec(𝐺, βˆ…)β€˜π‘) ∨ (rec(𝐺, βˆ…)β€˜π‘) βŠ† (rec(𝐺, βˆ…)β€˜π‘Ž))))
303, 29mprg 3067 . . . 4 βˆͺ π‘Ž ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘Ž):βˆͺ π‘Ž ∈ Ο‰ (𝑅1β€˜π‘Ž)–1-1β†’Ο‰
31 rdgfun 8363 . . . . . 6 Fun rec(𝐺, βˆ…)
32 funiunfv 7196 . . . . . . 7 (Fun rec(𝐺, βˆ…) β†’ βˆͺ π‘Ž ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘Ž) = βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰))
3332eqcomd 2739 . . . . . 6 (Fun rec(𝐺, βˆ…) β†’ βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰) = βˆͺ π‘Ž ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘Ž))
34 f1eq1 6734 . . . . . 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 9707 . . . . . . 7 (Fun 𝑅1 ∧ Lim dom 𝑅1)
3736simpli 485 . . . . . 6 Fun 𝑅1
38 funiunfv 7196 . . . . . 6 (Fun 𝑅1 β†’ βˆͺ π‘Ž ∈ Ο‰ (𝑅1β€˜π‘Ž) = βˆͺ (𝑅1 β€œ Ο‰))
39 f1eq2 6735 . . . . . 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 6102 . . . 4 ran βˆͺ (rec(𝐺, βˆ…) β€œ Ο‰) = βˆͺ π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰)ran π‘Ž
44 eliun 4959 . . . . . 6 (𝑏 ∈ βˆͺ π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰)ran π‘Ž ↔ βˆƒπ‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰)𝑏 ∈ ran π‘Ž)
45 df-rex 3071 . . . . . 6 (βˆƒπ‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰)𝑏 ∈ ran π‘Ž ↔ βˆƒπ‘Ž(π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ∧ 𝑏 ∈ ran π‘Ž))
46 funfn 6532 . . . . . . . . . . . 12 (Fun rec(𝐺, βˆ…) ↔ rec(𝐺, βˆ…) Fn dom rec(𝐺, βˆ…))
4731, 46mpbi 229 . . . . . . . . . . 11 rec(𝐺, βˆ…) Fn dom rec(𝐺, βˆ…)
48 rdgdmlim 8364 . . . . . . . . . . . 12 Lim dom rec(𝐺, βˆ…)
49 limomss 7808 . . . . . . . . . . . 12 (Lim dom rec(𝐺, βˆ…) β†’ Ο‰ βŠ† dom rec(𝐺, βˆ…))
5048, 49ax-mp 5 . . . . . . . . . . 11 Ο‰ βŠ† dom rec(𝐺, βˆ…)
51 fvelimab 6915 . . . . . . . . . . 11 ((rec(𝐺, βˆ…) Fn dom rec(𝐺, βˆ…) ∧ Ο‰ βŠ† dom rec(𝐺, βˆ…)) β†’ (π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ↔ βˆƒπ‘ ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘) = π‘Ž))
5247, 50, 51mp2an 691 . . . . . . . . . 10 (π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ↔ βˆƒπ‘ ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘) = π‘Ž)
534, 5ackbij2lem2 10181 . . . . . . . . . . . . . 14 (𝑐 ∈ Ο‰ β†’ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘)))
54 f1ofo 6792 . . . . . . . . . . . . . 14 ((rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜π‘)) β†’ (rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–ontoβ†’(cardβ€˜(𝑅1β€˜π‘)))
55 forn 6760 . . . . . . . . . . . . . 14 ((rec(𝐺, βˆ…)β€˜π‘):(𝑅1β€˜π‘)–ontoβ†’(cardβ€˜(𝑅1β€˜π‘)) β†’ ran (rec(𝐺, βˆ…)β€˜π‘) = (cardβ€˜(𝑅1β€˜π‘)))
5653, 54, 553syl 18 . . . . . . . . . . . . 13 (𝑐 ∈ Ο‰ β†’ ran (rec(𝐺, βˆ…)β€˜π‘) = (cardβ€˜(𝑅1β€˜π‘)))
57 r1fin 9714 . . . . . . . . . . . . . . 15 (𝑐 ∈ Ο‰ β†’ (𝑅1β€˜π‘) ∈ Fin)
58 ficardom 9902 . . . . . . . . . . . . . . 15 ((𝑅1β€˜π‘) ∈ Fin β†’ (cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰)
5957, 58syl 17 . . . . . . . . . . . . . 14 (𝑐 ∈ Ο‰ β†’ (cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰)
60 ordelss 6334 . . . . . . . . . . . . . 14 ((Ord Ο‰ ∧ (cardβ€˜(𝑅1β€˜π‘)) ∈ Ο‰) β†’ (cardβ€˜(𝑅1β€˜π‘)) βŠ† Ο‰)
619, 59, 60sylancr 588 . . . . . . . . . . . . 13 (𝑐 ∈ Ο‰ β†’ (cardβ€˜(𝑅1β€˜π‘)) βŠ† Ο‰)
6256, 61eqsstrd 3983 . . . . . . . . . . . 12 (𝑐 ∈ Ο‰ β†’ ran (rec(𝐺, βˆ…)β€˜π‘) βŠ† Ο‰)
63 rneq 5892 . . . . . . . . . . . . 13 ((rec(𝐺, βˆ…)β€˜π‘) = π‘Ž β†’ ran (rec(𝐺, βˆ…)β€˜π‘) = ran π‘Ž)
6463sseq1d 3976 . . . . . . . . . . . 12 ((rec(𝐺, βˆ…)β€˜π‘) = π‘Ž β†’ (ran (rec(𝐺, βˆ…)β€˜π‘) βŠ† Ο‰ ↔ ran π‘Ž βŠ† Ο‰))
6562, 64syl5ibcom 244 . . . . . . . . . . 11 (𝑐 ∈ Ο‰ β†’ ((rec(𝐺, βˆ…)β€˜π‘) = π‘Ž β†’ ran π‘Ž βŠ† Ο‰))
6665rexlimiv 3142 . . . . . . . . . 10 (βˆƒπ‘ ∈ Ο‰ (rec(𝐺, βˆ…)β€˜π‘) = π‘Ž β†’ ran π‘Ž βŠ† Ο‰)
6752, 66sylbi 216 . . . . . . . . 9 (π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) β†’ ran π‘Ž βŠ† Ο‰)
6867sselda 3945 . . . . . . . 8 ((π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ∧ 𝑏 ∈ ran π‘Ž) β†’ 𝑏 ∈ Ο‰)
6968exlimiv 1934 . . . . . . 7 (βˆƒπ‘Ž(π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ∧ 𝑏 ∈ ran π‘Ž) β†’ 𝑏 ∈ Ο‰)
70 peano2 7828 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ suc 𝑏 ∈ Ο‰)
71 fnfvima 7184 . . . . . . . . 9 ((rec(𝐺, βˆ…) Fn dom rec(𝐺, βˆ…) ∧ Ο‰ βŠ† dom rec(𝐺, βˆ…) ∧ suc 𝑏 ∈ Ο‰) β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏) ∈ (rec(𝐺, βˆ…) β€œ Ο‰))
7247, 50, 70, 71mp3an12i 1466 . . . . . . . 8 (𝑏 ∈ Ο‰ β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏) ∈ (rec(𝐺, βˆ…) β€œ Ο‰))
73 vex 3448 . . . . . . . . . 10 𝑏 ∈ V
74 cardnn 9904 . . . . . . . . . . . 12 (suc 𝑏 ∈ Ο‰ β†’ (cardβ€˜suc 𝑏) = suc 𝑏)
75 fvex 6856 . . . . . . . . . . . . . 14 (𝑅1β€˜suc 𝑏) ∈ V
7636simpri 487 . . . . . . . . . . . . . . . . 17 Lim dom 𝑅1
77 limomss 7808 . . . . . . . . . . . . . . . . 17 (Lim dom 𝑅1 β†’ Ο‰ βŠ† dom 𝑅1)
7876, 77ax-mp 5 . . . . . . . . . . . . . . . 16 Ο‰ βŠ† dom 𝑅1
7978sseli 3941 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ Ο‰ β†’ suc 𝑏 ∈ dom 𝑅1)
80 onssr1 9772 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ dom 𝑅1 β†’ suc 𝑏 βŠ† (𝑅1β€˜suc 𝑏))
8179, 80syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ Ο‰ β†’ suc 𝑏 βŠ† (𝑅1β€˜suc 𝑏))
82 ssdomg 8943 . . . . . . . . . . . . . 14 ((𝑅1β€˜suc 𝑏) ∈ V β†’ (suc 𝑏 βŠ† (𝑅1β€˜suc 𝑏) β†’ suc 𝑏 β‰Ό (𝑅1β€˜suc 𝑏)))
8375, 81, 82mpsyl 68 . . . . . . . . . . . . 13 (suc 𝑏 ∈ Ο‰ β†’ suc 𝑏 β‰Ό (𝑅1β€˜suc 𝑏))
84 nnon 7809 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ Ο‰ β†’ suc 𝑏 ∈ On)
85 onenon 9890 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ On β†’ suc 𝑏 ∈ dom card)
8684, 85syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ Ο‰ β†’ suc 𝑏 ∈ dom card)
87 r1fin 9714 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ Ο‰ β†’ (𝑅1β€˜suc 𝑏) ∈ Fin)
88 finnum 9889 . . . . . . . . . . . . . . 15 ((𝑅1β€˜suc 𝑏) ∈ Fin β†’ (𝑅1β€˜suc 𝑏) ∈ dom card)
8987, 88syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ Ο‰ β†’ (𝑅1β€˜suc 𝑏) ∈ dom card)
90 carddom2 9918 . . . . . . . . . . . . . 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 3984 . . . . . . . . . . 11 (suc 𝑏 ∈ Ο‰ β†’ suc 𝑏 βŠ† (cardβ€˜(𝑅1β€˜suc 𝑏)))
9470, 93syl 17 . . . . . . . . . 10 (𝑏 ∈ Ο‰ β†’ suc 𝑏 βŠ† (cardβ€˜(𝑅1β€˜suc 𝑏)))
95 sucssel 6413 . . . . . . . . . 10 (𝑏 ∈ V β†’ (suc 𝑏 βŠ† (cardβ€˜(𝑅1β€˜suc 𝑏)) β†’ 𝑏 ∈ (cardβ€˜(𝑅1β€˜suc 𝑏))))
9673, 94, 95mpsyl 68 . . . . . . . . 9 (𝑏 ∈ Ο‰ β†’ 𝑏 ∈ (cardβ€˜(𝑅1β€˜suc 𝑏)))
974, 5ackbij2lem2 10181 . . . . . . . . . 10 (suc 𝑏 ∈ Ο‰ β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏):(𝑅1β€˜suc 𝑏)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜suc 𝑏)))
98 f1ofo 6792 . . . . . . . . . 10 ((rec(𝐺, βˆ…)β€˜suc 𝑏):(𝑅1β€˜suc 𝑏)–1-1-ontoβ†’(cardβ€˜(𝑅1β€˜suc 𝑏)) β†’ (rec(𝐺, βˆ…)β€˜suc 𝑏):(𝑅1β€˜suc 𝑏)–ontoβ†’(cardβ€˜(𝑅1β€˜suc 𝑏)))
99 forn 6760 . . . . . . . . . 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 6856 . . . . . . . . 9 (rec(𝐺, βˆ…)β€˜suc 𝑏) ∈ V
103 eleq1 2822 . . . . . . . . . 10 (π‘Ž = (rec(𝐺, βˆ…)β€˜suc 𝑏) β†’ (π‘Ž ∈ (rec(𝐺, βˆ…) β€œ Ο‰) ↔ (rec(𝐺, βˆ…)β€˜suc 𝑏) ∈ (rec(𝐺, βˆ…) β€œ Ο‰)))
104 rneq 5892 . . . . . . . . . . 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 3564 . . . . . . . 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 6794 . . 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 6773 . . 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 3061  βˆƒwrex 3070  Vcvv 3444   ∩ cin 3910   βŠ† wss 3911  βˆ…c0 4283  π’« cpw 4561  {csn 4587  βˆͺ cuni 4866  βˆͺ ciun 4955   class class class wbr 5106   ↦ cmpt 5189   Γ— cxp 5632  dom cdm 5634  ran crn 5635   β€œ cima 5637  Ord word 6317  Oncon0 6318  Lim wlim 6319  suc csuc 6320  Fun wfun 6491   Fn wfn 6492  β€“1-1β†’wf1 6494  β€“ontoβ†’wfo 6495  β€“1-1-ontoβ†’wf1o 6496  β€˜cfv 6497  Ο‰com 7803  reccrdg 8356   β‰Ό cdom 8884  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-rank 9706  df-dju 9842  df-card 9880
This theorem is referenced by:  r1om  10185
  Copyright terms: Public domain W3C validator