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

Theorem ackbij2 9320
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 6377 . . . . . 6 (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏))
2 fvex 6390 . . . . . 6 (rec(𝐺, ∅)‘𝑎) ∈ V
31, 2fun11iun 7326 . . . . 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 9317 . . . . . . . 8 (𝑎 ∈ ω → (rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)))
7 f1of1 6321 . . . . . . . 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 7274 . . . . . . . 8 Ord ω
10 r1fin 8853 . . . . . . . . 9 (𝑎 ∈ ω → (𝑅1𝑎) ∈ Fin)
11 ficardom 9040 . . . . . . . . 9 ((𝑅1𝑎) ∈ Fin → (card‘(𝑅1𝑎)) ∈ ω)
1210, 11syl 17 . . . . . . . 8 (𝑎 ∈ ω → (card‘(𝑅1𝑎)) ∈ ω)
13 ordelss 5926 . . . . . . . 8 ((Ord ω ∧ (card‘(𝑅1𝑎)) ∈ ω) → (card‘(𝑅1𝑎)) ⊆ ω)
149, 12, 13sylancr 581 . . . . . . 7 (𝑎 ∈ ω → (card‘(𝑅1𝑎)) ⊆ ω)
15 f1ss 6290 . . . . . . 7 (((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→(card‘(𝑅1𝑎)) ∧ (card‘(𝑅1𝑎)) ⊆ ω) → (rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→ω)
168, 14, 15syl2anc 579 . . . . . 6 (𝑎 ∈ ω → (rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→ω)
17 nnord 7273 . . . . . . . . 9 (𝑎 ∈ ω → Ord 𝑎)
18 nnord 7273 . . . . . . . . 9 (𝑏 ∈ ω → Ord 𝑏)
19 ordtri2or2 6006 . . . . . . . . 9 ((Ord 𝑎 ∧ Ord 𝑏) → (𝑎𝑏𝑏𝑎))
2017, 18, 19syl2an 589 . . . . . . . 8 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎𝑏𝑏𝑎))
214, 5ackbij2lem4 9319 . . . . . . . . . . 11 (((𝑏 ∈ ω ∧ 𝑎 ∈ ω) ∧ 𝑎𝑏) → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏))
2221ex 401 . . . . . . . . . 10 ((𝑏 ∈ ω ∧ 𝑎 ∈ ω) → (𝑎𝑏 → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏)))
2322ancoms 450 . . . . . . . . 9 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎𝑏 → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏)))
244, 5ackbij2lem4 9319 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑎) → (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎))
2524ex 401 . . . . . . . . 9 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑏𝑎 → (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)))
2623, 25orim12d 987 . . . . . . . 8 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → ((𝑎𝑏𝑏𝑎) → ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎))))
2720, 26mpd 15 . . . . . . 7 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)))
2827ralrimiva 3113 . . . . . 6 (𝑎 ∈ ω → ∀𝑏 ∈ ω ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)))
2916, 28jca 507 . . . . 5 (𝑎 ∈ ω → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→ω ∧ ∀𝑏 ∈ ω ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎))))
303, 29mprg 3073 . . . 4 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎): 𝑎 ∈ ω (𝑅1𝑎)–1-1→ω
31 rdgfun 7718 . . . . . 6 Fun rec(𝐺, ∅)
32 funiunfv 6700 . . . . . . 7 (Fun rec(𝐺, ∅) → 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅) “ ω))
3332eqcomd 2771 . . . . . 6 (Fun rec(𝐺, ∅) → (rec(𝐺, ∅) “ ω) = 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎))
34 f1eq1 6280 . . . . . 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 8846 . . . . . . 7 (Fun 𝑅1 ∧ Lim dom 𝑅1)
3736simpli 476 . . . . . 6 Fun 𝑅1
38 funiunfv 6700 . . . . . 6 (Fun 𝑅1 𝑎 ∈ ω (𝑅1𝑎) = (𝑅1 “ ω))
39 f1eq2 6281 . . . . . 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 269 . . . 4 ( (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1→ω ↔ 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎): 𝑎 ∈ ω (𝑅1𝑎)–1-1→ω)
4230, 41mpbir 222 . . 3 (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1→ω
43 rnuni 5729 . . . 4 ran (rec(𝐺, ∅) “ ω) = 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎
44 eliun 4682 . . . . . 6 (𝑏 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎 ↔ ∃𝑎 ∈ (rec(𝐺, ∅) “ ω)𝑏 ∈ ran 𝑎)
45 df-rex 3061 . . . . . 6 (∃𝑎 ∈ (rec(𝐺, ∅) “ ω)𝑏 ∈ ran 𝑎 ↔ ∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎))
46 funfn 6100 . . . . . . . . . . . 12 (Fun rec(𝐺, ∅) ↔ rec(𝐺, ∅) Fn dom rec(𝐺, ∅))
4731, 46mpbi 221 . . . . . . . . . . 11 rec(𝐺, ∅) Fn dom rec(𝐺, ∅)
48 rdgdmlim 7719 . . . . . . . . . . . 12 Lim dom rec(𝐺, ∅)
49 limomss 7270 . . . . . . . . . . . 12 (Lim dom rec(𝐺, ∅) → ω ⊆ dom rec(𝐺, ∅))
5048, 49ax-mp 5 . . . . . . . . . . 11 ω ⊆ dom rec(𝐺, ∅)
51 fvelimab 6444 . . . . . . . . . . 11 ((rec(𝐺, ∅) Fn dom rec(𝐺, ∅) ∧ ω ⊆ dom rec(𝐺, ∅)) → (𝑎 ∈ (rec(𝐺, ∅) “ ω) ↔ ∃𝑐 ∈ ω (rec(𝐺, ∅)‘𝑐) = 𝑎))
5247, 50, 51mp2an 683 . . . . . . . . . 10 (𝑎 ∈ (rec(𝐺, ∅) “ ω) ↔ ∃𝑐 ∈ ω (rec(𝐺, ∅)‘𝑐) = 𝑎)
534, 5ackbij2lem2 9317 . . . . . . . . . . . . . 14 (𝑐 ∈ ω → (rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–1-1-onto→(card‘(𝑅1𝑐)))
54 f1ofo 6329 . . . . . . . . . . . . . 14 ((rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–1-1-onto→(card‘(𝑅1𝑐)) → (rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–onto→(card‘(𝑅1𝑐)))
55 forn 6303 . . . . . . . . . . . . . 14 ((rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–onto→(card‘(𝑅1𝑐)) → ran (rec(𝐺, ∅)‘𝑐) = (card‘(𝑅1𝑐)))
5653, 54, 553syl 18 . . . . . . . . . . . . 13 (𝑐 ∈ ω → ran (rec(𝐺, ∅)‘𝑐) = (card‘(𝑅1𝑐)))
57 r1fin 8853 . . . . . . . . . . . . . . 15 (𝑐 ∈ ω → (𝑅1𝑐) ∈ Fin)
58 ficardom 9040 . . . . . . . . . . . . . . 15 ((𝑅1𝑐) ∈ Fin → (card‘(𝑅1𝑐)) ∈ ω)
5957, 58syl 17 . . . . . . . . . . . . . 14 (𝑐 ∈ ω → (card‘(𝑅1𝑐)) ∈ ω)
60 ordelss 5926 . . . . . . . . . . . . . 14 ((Ord ω ∧ (card‘(𝑅1𝑐)) ∈ ω) → (card‘(𝑅1𝑐)) ⊆ ω)
619, 59, 60sylancr 581 . . . . . . . . . . . . 13 (𝑐 ∈ ω → (card‘(𝑅1𝑐)) ⊆ ω)
6256, 61eqsstrd 3801 . . . . . . . . . . . 12 (𝑐 ∈ ω → ran (rec(𝐺, ∅)‘𝑐) ⊆ ω)
63 rneq 5521 . . . . . . . . . . . . 13 ((rec(𝐺, ∅)‘𝑐) = 𝑎 → ran (rec(𝐺, ∅)‘𝑐) = ran 𝑎)
6463sseq1d 3794 . . . . . . . . . . . 12 ((rec(𝐺, ∅)‘𝑐) = 𝑎 → (ran (rec(𝐺, ∅)‘𝑐) ⊆ ω ↔ ran 𝑎 ⊆ ω))
6562, 64syl5ibcom 236 . . . . . . . . . . 11 (𝑐 ∈ ω → ((rec(𝐺, ∅)‘𝑐) = 𝑎 → ran 𝑎 ⊆ ω))
6665rexlimiv 3174 . . . . . . . . . 10 (∃𝑐 ∈ ω (rec(𝐺, ∅)‘𝑐) = 𝑎 → ran 𝑎 ⊆ ω)
6752, 66sylbi 208 . . . . . . . . 9 (𝑎 ∈ (rec(𝐺, ∅) “ ω) → ran 𝑎 ⊆ ω)
6867sselda 3763 . . . . . . . 8 ((𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) → 𝑏 ∈ ω)
6968exlimiv 2025 . . . . . . 7 (∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) → 𝑏 ∈ ω)
70 peano2 7286 . . . . . . . . 9 (𝑏 ∈ ω → suc 𝑏 ∈ ω)
71 fnfvima 6691 . . . . . . . . . 10 ((rec(𝐺, ∅) Fn dom rec(𝐺, ∅) ∧ ω ⊆ dom rec(𝐺, ∅) ∧ suc 𝑏 ∈ ω) → (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω))
7247, 50, 71mp3an12 1575 . . . . . . . . 9 (suc 𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω))
7370, 72syl 17 . . . . . . . 8 (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω))
74 vex 3353 . . . . . . . . . 10 𝑏 ∈ V
75 cardnn 9042 . . . . . . . . . . . 12 (suc 𝑏 ∈ ω → (card‘suc 𝑏) = suc 𝑏)
76 fvex 6390 . . . . . . . . . . . . . 14 (𝑅1‘suc 𝑏) ∈ V
7736simpri 479 . . . . . . . . . . . . . . . . 17 Lim dom 𝑅1
78 limomss 7270 . . . . . . . . . . . . . . . . 17 (Lim dom 𝑅1 → ω ⊆ dom 𝑅1)
7977, 78ax-mp 5 . . . . . . . . . . . . . . . 16 ω ⊆ dom 𝑅1
8079sseli 3759 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ ω → suc 𝑏 ∈ dom 𝑅1)
81 onssr1 8911 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ dom 𝑅1 → suc 𝑏 ⊆ (𝑅1‘suc 𝑏))
8280, 81syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ ω → suc 𝑏 ⊆ (𝑅1‘suc 𝑏))
83 ssdomg 8208 . . . . . . . . . . . . . 14 ((𝑅1‘suc 𝑏) ∈ V → (suc 𝑏 ⊆ (𝑅1‘suc 𝑏) → suc 𝑏 ≼ (𝑅1‘suc 𝑏)))
8476, 82, 83mpsyl 68 . . . . . . . . . . . . 13 (suc 𝑏 ∈ ω → suc 𝑏 ≼ (𝑅1‘suc 𝑏))
85 nnon 7271 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ ω → suc 𝑏 ∈ On)
86 onenon 9028 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ On → suc 𝑏 ∈ dom card)
8785, 86syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ ω → suc 𝑏 ∈ dom card)
88 r1fin 8853 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ ω → (𝑅1‘suc 𝑏) ∈ Fin)
89 finnum 9027 . . . . . . . . . . . . . . 15 ((𝑅1‘suc 𝑏) ∈ Fin → (𝑅1‘suc 𝑏) ∈ dom card)
9088, 89syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ ω → (𝑅1‘suc 𝑏) ∈ dom card)
91 carddom2 9056 . . . . . . . . . . . . . 14 ((suc 𝑏 ∈ dom card ∧ (𝑅1‘suc 𝑏) ∈ dom card) → ((card‘suc 𝑏) ⊆ (card‘(𝑅1‘suc 𝑏)) ↔ suc 𝑏 ≼ (𝑅1‘suc 𝑏)))
9287, 90, 91syl2anc 579 . . . . . . . . . . . . 13 (suc 𝑏 ∈ ω → ((card‘suc 𝑏) ⊆ (card‘(𝑅1‘suc 𝑏)) ↔ suc 𝑏 ≼ (𝑅1‘suc 𝑏)))
9384, 92mpbird 248 . . . . . . . . . . . 12 (suc 𝑏 ∈ ω → (card‘suc 𝑏) ⊆ (card‘(𝑅1‘suc 𝑏)))
9475, 93eqsstr3d 3802 . . . . . . . . . . 11 (suc 𝑏 ∈ ω → suc 𝑏 ⊆ (card‘(𝑅1‘suc 𝑏)))
9570, 94syl 17 . . . . . . . . . 10 (𝑏 ∈ ω → suc 𝑏 ⊆ (card‘(𝑅1‘suc 𝑏)))
96 sucssel 6002 . . . . . . . . . 10 (𝑏 ∈ V → (suc 𝑏 ⊆ (card‘(𝑅1‘suc 𝑏)) → 𝑏 ∈ (card‘(𝑅1‘suc 𝑏))))
9774, 95, 96mpsyl 68 . . . . . . . . 9 (𝑏 ∈ ω → 𝑏 ∈ (card‘(𝑅1‘suc 𝑏)))
984, 5ackbij2lem2 9317 . . . . . . . . . 10 (suc 𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)))
99 f1ofo 6329 . . . . . . . . . 10 ((rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)) → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–onto→(card‘(𝑅1‘suc 𝑏)))
100 forn 6303 . . . . . . . . . 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 2847 . . . . . . . 8 (𝑏 ∈ ω → 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏))
103 fvex 6390 . . . . . . . . 9 (rec(𝐺, ∅)‘suc 𝑏) ∈ V
104 eleq1 2832 . . . . . . . . . 10 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑎 ∈ (rec(𝐺, ∅) “ ω) ↔ (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω)))
105 rneq 5521 . . . . . . . . . . 11 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → ran 𝑎 = ran (rec(𝐺, ∅)‘suc 𝑏))
106105eleq2d 2830 . . . . . . . . . 10 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑏 ∈ ran 𝑎𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏)))
107104, 106anbi12d 624 . . . . . . . . 9 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → ((𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) ↔ ((rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏))))
108103, 107spcev 3453 . . . . . . . 8 (((rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏)) → ∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎))
10973, 102, 108syl2anc 579 . . . . . . 7 (𝑏 ∈ ω → ∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎))
11069, 109impbii 200 . . . . . 6 (∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) ↔ 𝑏 ∈ ω)
11144, 45, 1103bitri 288 . . . . 5 (𝑏 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎𝑏 ∈ ω)
112111eqriv 2762 . . . 4 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎 = ω
11343, 112eqtri 2787 . . 3 ran (rec(𝐺, ∅) “ ω) = ω
114 dff1o5 6331 . . 3 ( (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1-onto→ω ↔ ( (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1→ω ∧ ran (rec(𝐺, ∅) “ ω) = ω))
11542, 113, 114mpbir2an 702 . 2 (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1-onto→ω
116 ackbij.h . . 3 𝐻 = (rec(𝐺, ∅) “ ω)
117 f1oeq1 6312 . . 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 222 1 𝐻: (𝑅1 “ ω)–1-1-onto→ω
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wo 873   = wceq 1652  wex 1874  wcel 2155  wral 3055  wrex 3056  Vcvv 3350  cin 3733  wss 3734  c0 4081  𝒫 cpw 4317  {csn 4336   cuni 4596   ciun 4678   class class class wbr 4811  cmpt 4890   × cxp 5277  dom cdm 5279  ran crn 5280  cima 5282  Ord word 5909  Oncon0 5910  Lim wlim 5911  suc csuc 5912  Fun wfun 6064   Fn wfn 6065  1-1wf1 6067  ontowfo 6068  1-1-ontowf1o 6069  cfv 6070  ωcom 7265  reccrdg 7711  cdom 8160  Fincfn 8162  𝑅1cr1 8842  cardccrd 9014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-om 7266  df-1st 7368  df-2nd 7369  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-1o 7766  df-2o 7767  df-oadd 7770  df-er 7949  df-map 8064  df-en 8163  df-dom 8164  df-sdom 8165  df-fin 8166  df-r1 8844  df-rank 8845  df-card 9018  df-cda 9245
This theorem is referenced by:  r1om  9321
  Copyright terms: Public domain W3C validator