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

Theorem ackbij2 9257
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 6352 . . . . . 6 (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏))
2 fvex 6362 . . . . . 6 (rec(𝐺, ∅)‘𝑎) ∈ V
31, 2fun11iun 7291 . . . . 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 9254 . . . . . . . 8 (𝑎 ∈ ω → (rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)))
7 f1of1 6297 . . . . . . . 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 7239 . . . . . . . 8 Ord ω
10 r1fin 8809 . . . . . . . . 9 (𝑎 ∈ ω → (𝑅1𝑎) ∈ Fin)
11 ficardom 8977 . . . . . . . . 9 ((𝑅1𝑎) ∈ Fin → (card‘(𝑅1𝑎)) ∈ ω)
1210, 11syl 17 . . . . . . . 8 (𝑎 ∈ ω → (card‘(𝑅1𝑎)) ∈ ω)
13 ordelss 5900 . . . . . . . 8 ((Ord ω ∧ (card‘(𝑅1𝑎)) ∈ ω) → (card‘(𝑅1𝑎)) ⊆ ω)
149, 12, 13sylancr 698 . . . . . . 7 (𝑎 ∈ ω → (card‘(𝑅1𝑎)) ⊆ ω)
15 f1ss 6267 . . . . . . 7 (((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→(card‘(𝑅1𝑎)) ∧ (card‘(𝑅1𝑎)) ⊆ ω) → (rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→ω)
168, 14, 15syl2anc 696 . . . . . 6 (𝑎 ∈ ω → (rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→ω)
17 nnord 7238 . . . . . . . . 9 (𝑎 ∈ ω → Ord 𝑎)
18 nnord 7238 . . . . . . . . 9 (𝑏 ∈ ω → Ord 𝑏)
19 ordtri2or2 5984 . . . . . . . . 9 ((Ord 𝑎 ∧ Ord 𝑏) → (𝑎𝑏𝑏𝑎))
2017, 18, 19syl2an 495 . . . . . . . 8 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎𝑏𝑏𝑎))
214, 5ackbij2lem4 9256 . . . . . . . . . . 11 (((𝑏 ∈ ω ∧ 𝑎 ∈ ω) ∧ 𝑎𝑏) → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏))
2221ex 449 . . . . . . . . . 10 ((𝑏 ∈ ω ∧ 𝑎 ∈ ω) → (𝑎𝑏 → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏)))
2322ancoms 468 . . . . . . . . 9 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎𝑏 → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏)))
244, 5ackbij2lem4 9256 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑎) → (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎))
2524ex 449 . . . . . . . . 9 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑏𝑎 → (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)))
2623, 25orim12d 919 . . . . . . . 8 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → ((𝑎𝑏𝑏𝑎) → ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎))))
2720, 26mpd 15 . . . . . . 7 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)))
2827ralrimiva 3104 . . . . . 6 (𝑎 ∈ ω → ∀𝑏 ∈ ω ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)))
2916, 28jca 555 . . . . 5 (𝑎 ∈ ω → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→ω ∧ ∀𝑏 ∈ ω ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎))))
303, 29mprg 3064 . . . 4 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎): 𝑎 ∈ ω (𝑅1𝑎)–1-1→ω
31 rdgfun 7681 . . . . . 6 Fun rec(𝐺, ∅)
32 funiunfv 6669 . . . . . . 7 (Fun rec(𝐺, ∅) → 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅) “ ω))
3332eqcomd 2766 . . . . . 6 (Fun rec(𝐺, ∅) → (rec(𝐺, ∅) “ ω) = 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎))
34 f1eq1 6257 . . . . . 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 8802 . . . . . . 7 (Fun 𝑅1 ∧ Lim dom 𝑅1)
3736simpli 476 . . . . . 6 Fun 𝑅1
38 funiunfv 6669 . . . . . 6 (Fun 𝑅1 𝑎 ∈ ω (𝑅1𝑎) = (𝑅1 “ ω))
39 f1eq2 6258 . . . . . 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 5702 . . . 4 ran (rec(𝐺, ∅) “ ω) = 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎
44 eliun 4676 . . . . . 6 (𝑏 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎 ↔ ∃𝑎 ∈ (rec(𝐺, ∅) “ ω)𝑏 ∈ ran 𝑎)
45 df-rex 3056 . . . . . 6 (∃𝑎 ∈ (rec(𝐺, ∅) “ ω)𝑏 ∈ ran 𝑎 ↔ ∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎))
46 funfn 6079 . . . . . . . . . . . 12 (Fun rec(𝐺, ∅) ↔ rec(𝐺, ∅) Fn dom rec(𝐺, ∅))
4731, 46mpbi 220 . . . . . . . . . . 11 rec(𝐺, ∅) Fn dom rec(𝐺, ∅)
48 rdgdmlim 7682 . . . . . . . . . . . 12 Lim dom rec(𝐺, ∅)
49 limomss 7235 . . . . . . . . . . . 12 (Lim dom rec(𝐺, ∅) → ω ⊆ dom rec(𝐺, ∅))
5048, 49ax-mp 5 . . . . . . . . . . 11 ω ⊆ dom rec(𝐺, ∅)
51 fvelimab 6415 . . . . . . . . . . 11 ((rec(𝐺, ∅) Fn dom rec(𝐺, ∅) ∧ ω ⊆ dom rec(𝐺, ∅)) → (𝑎 ∈ (rec(𝐺, ∅) “ ω) ↔ ∃𝑐 ∈ ω (rec(𝐺, ∅)‘𝑐) = 𝑎))
5247, 50, 51mp2an 710 . . . . . . . . . 10 (𝑎 ∈ (rec(𝐺, ∅) “ ω) ↔ ∃𝑐 ∈ ω (rec(𝐺, ∅)‘𝑐) = 𝑎)
534, 5ackbij2lem2 9254 . . . . . . . . . . . . . 14 (𝑐 ∈ ω → (rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–1-1-onto→(card‘(𝑅1𝑐)))
54 f1ofo 6305 . . . . . . . . . . . . . 14 ((rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–1-1-onto→(card‘(𝑅1𝑐)) → (rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–onto→(card‘(𝑅1𝑐)))
55 forn 6279 . . . . . . . . . . . . . 14 ((rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–onto→(card‘(𝑅1𝑐)) → ran (rec(𝐺, ∅)‘𝑐) = (card‘(𝑅1𝑐)))
5653, 54, 553syl 18 . . . . . . . . . . . . 13 (𝑐 ∈ ω → ran (rec(𝐺, ∅)‘𝑐) = (card‘(𝑅1𝑐)))
57 r1fin 8809 . . . . . . . . . . . . . . 15 (𝑐 ∈ ω → (𝑅1𝑐) ∈ Fin)
58 ficardom 8977 . . . . . . . . . . . . . . 15 ((𝑅1𝑐) ∈ Fin → (card‘(𝑅1𝑐)) ∈ ω)
5957, 58syl 17 . . . . . . . . . . . . . 14 (𝑐 ∈ ω → (card‘(𝑅1𝑐)) ∈ ω)
60 ordelss 5900 . . . . . . . . . . . . . 14 ((Ord ω ∧ (card‘(𝑅1𝑐)) ∈ ω) → (card‘(𝑅1𝑐)) ⊆ ω)
619, 59, 60sylancr 698 . . . . . . . . . . . . 13 (𝑐 ∈ ω → (card‘(𝑅1𝑐)) ⊆ ω)
6256, 61eqsstrd 3780 . . . . . . . . . . . 12 (𝑐 ∈ ω → ran (rec(𝐺, ∅)‘𝑐) ⊆ ω)
63 rneq 5506 . . . . . . . . . . . . 13 ((rec(𝐺, ∅)‘𝑐) = 𝑎 → ran (rec(𝐺, ∅)‘𝑐) = ran 𝑎)
6463sseq1d 3773 . . . . . . . . . . . 12 ((rec(𝐺, ∅)‘𝑐) = 𝑎 → (ran (rec(𝐺, ∅)‘𝑐) ⊆ ω ↔ ran 𝑎 ⊆ ω))
6562, 64syl5ibcom 235 . . . . . . . . . . 11 (𝑐 ∈ ω → ((rec(𝐺, ∅)‘𝑐) = 𝑎 → ran 𝑎 ⊆ ω))
6665rexlimiv 3165 . . . . . . . . . 10 (∃𝑐 ∈ ω (rec(𝐺, ∅)‘𝑐) = 𝑎 → ran 𝑎 ⊆ ω)
6752, 66sylbi 207 . . . . . . . . 9 (𝑎 ∈ (rec(𝐺, ∅) “ ω) → ran 𝑎 ⊆ ω)
6867sselda 3744 . . . . . . . 8 ((𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) → 𝑏 ∈ ω)
6968exlimiv 2007 . . . . . . 7 (∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) → 𝑏 ∈ ω)
70 peano2 7251 . . . . . . . . 9 (𝑏 ∈ ω → suc 𝑏 ∈ ω)
71 fnfvima 6659 . . . . . . . . . 10 ((rec(𝐺, ∅) Fn dom rec(𝐺, ∅) ∧ ω ⊆ dom rec(𝐺, ∅) ∧ suc 𝑏 ∈ ω) → (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω))
7247, 50, 71mp3an12 1563 . . . . . . . . 9 (suc 𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω))
7370, 72syl 17 . . . . . . . 8 (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω))
74 vex 3343 . . . . . . . . . 10 𝑏 ∈ V
75 cardnn 8979 . . . . . . . . . . . 12 (suc 𝑏 ∈ ω → (card‘suc 𝑏) = suc 𝑏)
76 fvex 6362 . . . . . . . . . . . . . 14 (𝑅1‘suc 𝑏) ∈ V
7736simpri 481 . . . . . . . . . . . . . . . . 17 Lim dom 𝑅1
78 limomss 7235 . . . . . . . . . . . . . . . . 17 (Lim dom 𝑅1 → ω ⊆ dom 𝑅1)
7977, 78ax-mp 5 . . . . . . . . . . . . . . . 16 ω ⊆ dom 𝑅1
8079sseli 3740 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ ω → suc 𝑏 ∈ dom 𝑅1)
81 onssr1 8867 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ dom 𝑅1 → suc 𝑏 ⊆ (𝑅1‘suc 𝑏))
8280, 81syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ ω → suc 𝑏 ⊆ (𝑅1‘suc 𝑏))
83 ssdomg 8167 . . . . . . . . . . . . . 14 ((𝑅1‘suc 𝑏) ∈ V → (suc 𝑏 ⊆ (𝑅1‘suc 𝑏) → suc 𝑏 ≼ (𝑅1‘suc 𝑏)))
8476, 82, 83mpsyl 68 . . . . . . . . . . . . 13 (suc 𝑏 ∈ ω → suc 𝑏 ≼ (𝑅1‘suc 𝑏))
85 nnon 7236 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ ω → suc 𝑏 ∈ On)
86 onenon 8965 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ On → suc 𝑏 ∈ dom card)
8785, 86syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ ω → suc 𝑏 ∈ dom card)
88 r1fin 8809 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ ω → (𝑅1‘suc 𝑏) ∈ Fin)
89 finnum 8964 . . . . . . . . . . . . . . 15 ((𝑅1‘suc 𝑏) ∈ Fin → (𝑅1‘suc 𝑏) ∈ dom card)
9088, 89syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ ω → (𝑅1‘suc 𝑏) ∈ dom card)
91 carddom2 8993 . . . . . . . . . . . . . 14 ((suc 𝑏 ∈ dom card ∧ (𝑅1‘suc 𝑏) ∈ dom card) → ((card‘suc 𝑏) ⊆ (card‘(𝑅1‘suc 𝑏)) ↔ suc 𝑏 ≼ (𝑅1‘suc 𝑏)))
9287, 90, 91syl2anc 696 . . . . . . . . . . . . 13 (suc 𝑏 ∈ ω → ((card‘suc 𝑏) ⊆ (card‘(𝑅1‘suc 𝑏)) ↔ suc 𝑏 ≼ (𝑅1‘suc 𝑏)))
9384, 92mpbird 247 . . . . . . . . . . . 12 (suc 𝑏 ∈ ω → (card‘suc 𝑏) ⊆ (card‘(𝑅1‘suc 𝑏)))
9475, 93eqsstr3d 3781 . . . . . . . . . . 11 (suc 𝑏 ∈ ω → suc 𝑏 ⊆ (card‘(𝑅1‘suc 𝑏)))
9570, 94syl 17 . . . . . . . . . 10 (𝑏 ∈ ω → suc 𝑏 ⊆ (card‘(𝑅1‘suc 𝑏)))
96 sucssel 5980 . . . . . . . . . 10 (𝑏 ∈ V → (suc 𝑏 ⊆ (card‘(𝑅1‘suc 𝑏)) → 𝑏 ∈ (card‘(𝑅1‘suc 𝑏))))
9774, 95, 96mpsyl 68 . . . . . . . . 9 (𝑏 ∈ ω → 𝑏 ∈ (card‘(𝑅1‘suc 𝑏)))
984, 5ackbij2lem2 9254 . . . . . . . . . 10 (suc 𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)))
99 f1ofo 6305 . . . . . . . . . 10 ((rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)) → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–onto→(card‘(𝑅1‘suc 𝑏)))
100 forn 6279 . . . . . . . . . 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 2842 . . . . . . . 8 (𝑏 ∈ ω → 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏))
103 fvex 6362 . . . . . . . . 9 (rec(𝐺, ∅)‘suc 𝑏) ∈ V
104 eleq1 2827 . . . . . . . . . 10 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑎 ∈ (rec(𝐺, ∅) “ ω) ↔ (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω)))
105 rneq 5506 . . . . . . . . . . 11 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → ran 𝑎 = ran (rec(𝐺, ∅)‘suc 𝑏))
106105eleq2d 2825 . . . . . . . . . 10 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑏 ∈ ran 𝑎𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏)))
107104, 106anbi12d 749 . . . . . . . . 9 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → ((𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) ↔ ((rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏))))
108103, 107spcev 3440 . . . . . . . 8 (((rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏)) → ∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎))
10973, 102, 108syl2anc 696 . . . . . . 7 (𝑏 ∈ ω → ∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎))
11069, 109impbii 199 . . . . . 6 (∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) ↔ 𝑏 ∈ ω)
11144, 45, 1103bitri 286 . . . . 5 (𝑏 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎𝑏 ∈ ω)
112111eqriv 2757 . . . 4 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎 = ω
11343, 112eqtri 2782 . . 3 ran (rec(𝐺, ∅) “ ω) = ω
114 dff1o5 6307 . . 3 ( (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1-onto→ω ↔ ( (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1→ω ∧ ran (rec(𝐺, ∅) “ ω) = ω))
11542, 113, 114mpbir2an 993 . 2 (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1-onto→ω
116 ackbij.h . . 3 𝐻 = (rec(𝐺, ∅) “ ω)
117 f1oeq1 6288 . . 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 382  wa 383   = wceq 1632  wex 1853  wcel 2139  wral 3050  wrex 3051  Vcvv 3340  cin 3714  wss 3715  c0 4058  𝒫 cpw 4302  {csn 4321   cuni 4588   ciun 4672   class class class wbr 4804  cmpt 4881   × cxp 5264  dom cdm 5266  ran crn 5267  cima 5269  Ord word 5883  Oncon0 5884  Lim wlim 5885  suc csuc 5886  Fun wfun 6043   Fn wfn 6044  1-1wf1 6046  ontowfo 6047  1-1-ontowf1o 6048  cfv 6049  ωcom 7230  reccrdg 7674  cdom 8119  Fincfn 8121  𝑅1cr1 8798  cardccrd 8951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-er 7911  df-map 8025  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-r1 8800  df-rank 8801  df-card 8955  df-cda 9182
This theorem is referenced by:  r1om  9258
  Copyright terms: Public domain W3C validator