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

Theorem ackbij2 9009
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 6148 . . . . . 6 (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏))
2 fvex 6158 . . . . . 6 (rec(𝐺, ∅)‘𝑎) ∈ V
31, 2fun11iun 7073 . . . . 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 9006 . . . . . . . 8 (𝑎 ∈ ω → (rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)))
7 f1of1 6093 . . . . . . . 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 7021 . . . . . . . 8 Ord ω
10 r1fin 8580 . . . . . . . . 9 (𝑎 ∈ ω → (𝑅1𝑎) ∈ Fin)
11 ficardom 8731 . . . . . . . . 9 ((𝑅1𝑎) ∈ Fin → (card‘(𝑅1𝑎)) ∈ ω)
1210, 11syl 17 . . . . . . . 8 (𝑎 ∈ ω → (card‘(𝑅1𝑎)) ∈ ω)
13 ordelss 5698 . . . . . . . 8 ((Ord ω ∧ (card‘(𝑅1𝑎)) ∈ ω) → (card‘(𝑅1𝑎)) ⊆ ω)
149, 12, 13sylancr 694 . . . . . . 7 (𝑎 ∈ ω → (card‘(𝑅1𝑎)) ⊆ ω)
15 f1ss 6063 . . . . . . 7 (((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→(card‘(𝑅1𝑎)) ∧ (card‘(𝑅1𝑎)) ⊆ ω) → (rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→ω)
168, 14, 15syl2anc 692 . . . . . 6 (𝑎 ∈ ω → (rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→ω)
17 nnord 7020 . . . . . . . . 9 (𝑎 ∈ ω → Ord 𝑎)
18 nnord 7020 . . . . . . . . 9 (𝑏 ∈ ω → Ord 𝑏)
19 ordtri2or2 5782 . . . . . . . . 9 ((Ord 𝑎 ∧ Ord 𝑏) → (𝑎𝑏𝑏𝑎))
2017, 18, 19syl2an 494 . . . . . . . 8 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎𝑏𝑏𝑎))
214, 5ackbij2lem4 9008 . . . . . . . . . . 11 (((𝑏 ∈ ω ∧ 𝑎 ∈ ω) ∧ 𝑎𝑏) → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏))
2221ex 450 . . . . . . . . . 10 ((𝑏 ∈ ω ∧ 𝑎 ∈ ω) → (𝑎𝑏 → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏)))
2322ancoms 469 . . . . . . . . 9 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎𝑏 → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏)))
244, 5ackbij2lem4 9008 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑎) → (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎))
2524ex 450 . . . . . . . . 9 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑏𝑎 → (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)))
2623, 25orim12d 882 . . . . . . . 8 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → ((𝑎𝑏𝑏𝑎) → ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎))))
2720, 26mpd 15 . . . . . . 7 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)))
2827ralrimiva 2960 . . . . . 6 (𝑎 ∈ ω → ∀𝑏 ∈ ω ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)))
2916, 28jca 554 . . . . 5 (𝑎 ∈ ω → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→ω ∧ ∀𝑏 ∈ ω ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎))))
303, 29mprg 2921 . . . 4 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎): 𝑎 ∈ ω (𝑅1𝑎)–1-1→ω
31 rdgfun 7457 . . . . . 6 Fun rec(𝐺, ∅)
32 funiunfv 6460 . . . . . . 7 (Fun rec(𝐺, ∅) → 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅) “ ω))
3332eqcomd 2627 . . . . . 6 (Fun rec(𝐺, ∅) → (rec(𝐺, ∅) “ ω) = 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎))
34 f1eq1 6053 . . . . . 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 8573 . . . . . . 7 (Fun 𝑅1 ∧ Lim dom 𝑅1)
3736simpli 474 . . . . . 6 Fun 𝑅1
38 funiunfv 6460 . . . . . 6 (Fun 𝑅1 𝑎 ∈ ω (𝑅1𝑎) = (𝑅1 “ ω))
39 f1eq2 6054 . . . . . 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 267 . . . 4 ( (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1→ω ↔ 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎): 𝑎 ∈ ω (𝑅1𝑎)–1-1→ω)
4230, 41mpbir 221 . . 3 (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1→ω
43 rnuni 5503 . . . 4 ran (rec(𝐺, ∅) “ ω) = 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎
44 eliun 4490 . . . . . 6 (𝑏 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎 ↔ ∃𝑎 ∈ (rec(𝐺, ∅) “ ω)𝑏 ∈ ran 𝑎)
45 df-rex 2913 . . . . . 6 (∃𝑎 ∈ (rec(𝐺, ∅) “ ω)𝑏 ∈ ran 𝑎 ↔ ∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎))
46 funfn 5877 . . . . . . . . . . . 12 (Fun rec(𝐺, ∅) ↔ rec(𝐺, ∅) Fn dom rec(𝐺, ∅))
4731, 46mpbi 220 . . . . . . . . . . 11 rec(𝐺, ∅) Fn dom rec(𝐺, ∅)
48 rdgdmlim 7458 . . . . . . . . . . . 12 Lim dom rec(𝐺, ∅)
49 limomss 7017 . . . . . . . . . . . 12 (Lim dom rec(𝐺, ∅) → ω ⊆ dom rec(𝐺, ∅))
5048, 49ax-mp 5 . . . . . . . . . . 11 ω ⊆ dom rec(𝐺, ∅)
51 fvelimab 6210 . . . . . . . . . . 11 ((rec(𝐺, ∅) Fn dom rec(𝐺, ∅) ∧ ω ⊆ dom rec(𝐺, ∅)) → (𝑎 ∈ (rec(𝐺, ∅) “ ω) ↔ ∃𝑐 ∈ ω (rec(𝐺, ∅)‘𝑐) = 𝑎))
5247, 50, 51mp2an 707 . . . . . . . . . 10 (𝑎 ∈ (rec(𝐺, ∅) “ ω) ↔ ∃𝑐 ∈ ω (rec(𝐺, ∅)‘𝑐) = 𝑎)
534, 5ackbij2lem2 9006 . . . . . . . . . . . . . 14 (𝑐 ∈ ω → (rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–1-1-onto→(card‘(𝑅1𝑐)))
54 f1ofo 6101 . . . . . . . . . . . . . 14 ((rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–1-1-onto→(card‘(𝑅1𝑐)) → (rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–onto→(card‘(𝑅1𝑐)))
55 forn 6075 . . . . . . . . . . . . . 14 ((rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–onto→(card‘(𝑅1𝑐)) → ran (rec(𝐺, ∅)‘𝑐) = (card‘(𝑅1𝑐)))
5653, 54, 553syl 18 . . . . . . . . . . . . 13 (𝑐 ∈ ω → ran (rec(𝐺, ∅)‘𝑐) = (card‘(𝑅1𝑐)))
57 r1fin 8580 . . . . . . . . . . . . . . 15 (𝑐 ∈ ω → (𝑅1𝑐) ∈ Fin)
58 ficardom 8731 . . . . . . . . . . . . . . 15 ((𝑅1𝑐) ∈ Fin → (card‘(𝑅1𝑐)) ∈ ω)
5957, 58syl 17 . . . . . . . . . . . . . 14 (𝑐 ∈ ω → (card‘(𝑅1𝑐)) ∈ ω)
60 ordelss 5698 . . . . . . . . . . . . . 14 ((Ord ω ∧ (card‘(𝑅1𝑐)) ∈ ω) → (card‘(𝑅1𝑐)) ⊆ ω)
619, 59, 60sylancr 694 . . . . . . . . . . . . 13 (𝑐 ∈ ω → (card‘(𝑅1𝑐)) ⊆ ω)
6256, 61eqsstrd 3618 . . . . . . . . . . . 12 (𝑐 ∈ ω → ran (rec(𝐺, ∅)‘𝑐) ⊆ ω)
63 rneq 5311 . . . . . . . . . . . . 13 ((rec(𝐺, ∅)‘𝑐) = 𝑎 → ran (rec(𝐺, ∅)‘𝑐) = ran 𝑎)
6463sseq1d 3611 . . . . . . . . . . . 12 ((rec(𝐺, ∅)‘𝑐) = 𝑎 → (ran (rec(𝐺, ∅)‘𝑐) ⊆ ω ↔ ran 𝑎 ⊆ ω))
6562, 64syl5ibcom 235 . . . . . . . . . . 11 (𝑐 ∈ ω → ((rec(𝐺, ∅)‘𝑐) = 𝑎 → ran 𝑎 ⊆ ω))
6665rexlimiv 3020 . . . . . . . . . 10 (∃𝑐 ∈ ω (rec(𝐺, ∅)‘𝑐) = 𝑎 → ran 𝑎 ⊆ ω)
6752, 66sylbi 207 . . . . . . . . 9 (𝑎 ∈ (rec(𝐺, ∅) “ ω) → ran 𝑎 ⊆ ω)
6867sselda 3583 . . . . . . . 8 ((𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) → 𝑏 ∈ ω)
6968exlimiv 1855 . . . . . . 7 (∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) → 𝑏 ∈ ω)
70 peano2 7033 . . . . . . . . 9 (𝑏 ∈ ω → suc 𝑏 ∈ ω)
71 fnfvima 6450 . . . . . . . . . 10 ((rec(𝐺, ∅) Fn dom rec(𝐺, ∅) ∧ ω ⊆ dom rec(𝐺, ∅) ∧ suc 𝑏 ∈ ω) → (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω))
7247, 50, 71mp3an12 1411 . . . . . . . . 9 (suc 𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω))
7370, 72syl 17 . . . . . . . 8 (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω))
74 vex 3189 . . . . . . . . . 10 𝑏 ∈ V
75 cardnn 8733 . . . . . . . . . . . 12 (suc 𝑏 ∈ ω → (card‘suc 𝑏) = suc 𝑏)
76 fvex 6158 . . . . . . . . . . . . . 14 (𝑅1‘suc 𝑏) ∈ V
7736simpri 478 . . . . . . . . . . . . . . . . 17 Lim dom 𝑅1
78 limomss 7017 . . . . . . . . . . . . . . . . 17 (Lim dom 𝑅1 → ω ⊆ dom 𝑅1)
7977, 78ax-mp 5 . . . . . . . . . . . . . . . 16 ω ⊆ dom 𝑅1
8079sseli 3579 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ ω → suc 𝑏 ∈ dom 𝑅1)
81 onssr1 8638 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ dom 𝑅1 → suc 𝑏 ⊆ (𝑅1‘suc 𝑏))
8280, 81syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ ω → suc 𝑏 ⊆ (𝑅1‘suc 𝑏))
83 ssdomg 7945 . . . . . . . . . . . . . 14 ((𝑅1‘suc 𝑏) ∈ V → (suc 𝑏 ⊆ (𝑅1‘suc 𝑏) → suc 𝑏 ≼ (𝑅1‘suc 𝑏)))
8476, 82, 83mpsyl 68 . . . . . . . . . . . . 13 (suc 𝑏 ∈ ω → suc 𝑏 ≼ (𝑅1‘suc 𝑏))
85 nnon 7018 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ ω → suc 𝑏 ∈ On)
86 onenon 8719 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ On → suc 𝑏 ∈ dom card)
8785, 86syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ ω → suc 𝑏 ∈ dom card)
88 r1fin 8580 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ ω → (𝑅1‘suc 𝑏) ∈ Fin)
89 finnum 8718 . . . . . . . . . . . . . . 15 ((𝑅1‘suc 𝑏) ∈ Fin → (𝑅1‘suc 𝑏) ∈ dom card)
9088, 89syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ ω → (𝑅1‘suc 𝑏) ∈ dom card)
91 carddom2 8747 . . . . . . . . . . . . . 14 ((suc 𝑏 ∈ dom card ∧ (𝑅1‘suc 𝑏) ∈ dom card) → ((card‘suc 𝑏) ⊆ (card‘(𝑅1‘suc 𝑏)) ↔ suc 𝑏 ≼ (𝑅1‘suc 𝑏)))
9287, 90, 91syl2anc 692 . . . . . . . . . . . . 13 (suc 𝑏 ∈ ω → ((card‘suc 𝑏) ⊆ (card‘(𝑅1‘suc 𝑏)) ↔ suc 𝑏 ≼ (𝑅1‘suc 𝑏)))
9384, 92mpbird 247 . . . . . . . . . . . 12 (suc 𝑏 ∈ ω → (card‘suc 𝑏) ⊆ (card‘(𝑅1‘suc 𝑏)))
9475, 93eqsstr3d 3619 . . . . . . . . . . 11 (suc 𝑏 ∈ ω → suc 𝑏 ⊆ (card‘(𝑅1‘suc 𝑏)))
9570, 94syl 17 . . . . . . . . . 10 (𝑏 ∈ ω → suc 𝑏 ⊆ (card‘(𝑅1‘suc 𝑏)))
96 sucssel 5778 . . . . . . . . . 10 (𝑏 ∈ V → (suc 𝑏 ⊆ (card‘(𝑅1‘suc 𝑏)) → 𝑏 ∈ (card‘(𝑅1‘suc 𝑏))))
9774, 95, 96mpsyl 68 . . . . . . . . 9 (𝑏 ∈ ω → 𝑏 ∈ (card‘(𝑅1‘suc 𝑏)))
984, 5ackbij2lem2 9006 . . . . . . . . . 10 (suc 𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)))
99 f1ofo 6101 . . . . . . . . . 10 ((rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)) → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–onto→(card‘(𝑅1‘suc 𝑏)))
100 forn 6075 . . . . . . . . . 10 ((rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–onto→(card‘(𝑅1‘suc 𝑏)) → ran (rec(𝐺, ∅)‘suc 𝑏) = (card‘(𝑅1‘suc 𝑏)))
10170, 98, 99, 1004syl 19 . . . . . . . . 9 (𝑏 ∈ ω → ran (rec(𝐺, ∅)‘suc 𝑏) = (card‘(𝑅1‘suc 𝑏)))
10297, 101eleqtrrd 2701 . . . . . . . 8 (𝑏 ∈ ω → 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏))
103 fvex 6158 . . . . . . . . 9 (rec(𝐺, ∅)‘suc 𝑏) ∈ V
104 eleq1 2686 . . . . . . . . . 10 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑎 ∈ (rec(𝐺, ∅) “ ω) ↔ (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω)))
105 rneq 5311 . . . . . . . . . . 11 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → ran 𝑎 = ran (rec(𝐺, ∅)‘suc 𝑏))
106105eleq2d 2684 . . . . . . . . . 10 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑏 ∈ ran 𝑎𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏)))
107104, 106anbi12d 746 . . . . . . . . 9 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → ((𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) ↔ ((rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏))))
108103, 107spcev 3286 . . . . . . . 8 (((rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏)) → ∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎))
10973, 102, 108syl2anc 692 . . . . . . 7 (𝑏 ∈ ω → ∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎))
11069, 109impbii 199 . . . . . 6 (∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) ↔ 𝑏 ∈ ω)
11144, 45, 1103bitri 286 . . . . 5 (𝑏 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎𝑏 ∈ ω)
112111eqriv 2618 . . . 4 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎 = ω
11343, 112eqtri 2643 . . 3 ran (rec(𝐺, ∅) “ ω) = ω
114 dff1o5 6103 . . 3 ( (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1-onto→ω ↔ ( (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1→ω ∧ ran (rec(𝐺, ∅) “ ω) = ω))
11542, 113, 114mpbir2an 954 . 2 (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1-onto→ω
116 ackbij.h . . 3 𝐻 = (rec(𝐺, ∅) “ ω)
117 f1oeq1 6084 . . 3 (𝐻 = (rec(𝐺, ∅) “ ω) → (𝐻: (𝑅1 “ ω)–1-1-onto→ω ↔ (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1-onto→ω))
118116, 117ax-mp 5 . 2 (𝐻: (𝑅1 “ ω)–1-1-onto→ω ↔ (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1-onto→ω)
119115, 118mpbir 221 1 𝐻: (𝑅1 “ ω)–1-1-onto→ω
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wex 1701  wcel 1987  wral 2907  wrex 2908  Vcvv 3186  cin 3554  wss 3555  c0 3891  𝒫 cpw 4130  {csn 4148   cuni 4402   ciun 4485   class class class wbr 4613  cmpt 4673   × cxp 5072  dom cdm 5074  ran crn 5075  cima 5077  Ord word 5681  Oncon0 5682  Lim wlim 5683  suc csuc 5684  Fun wfun 5841   Fn wfn 5842  1-1wf1 5844  ontowfo 5845  1-1-ontowf1o 5846  cfv 5847  ωcom 7012  reccrdg 7450  cdom 7897  Fincfn 7899  𝑅1cr1 8569  cardccrd 8705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-er 7687  df-map 7804  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-r1 8571  df-rank 8572  df-card 8709  df-cda 8934
This theorem is referenced by:  r1om  9010
  Copyright terms: Public domain W3C validator