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

Theorem ackbij2 9103
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 6229 . . . . . 6 (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏))
2 fvex 6239 . . . . . 6 (rec(𝐺, ∅)‘𝑎) ∈ V
31, 2fun11iun 7168 . . . . 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 9100 . . . . . . . 8 (𝑎 ∈ ω → (rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)))
7 f1of1 6174 . . . . . . . 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 7116 . . . . . . . 8 Ord ω
10 r1fin 8674 . . . . . . . . 9 (𝑎 ∈ ω → (𝑅1𝑎) ∈ Fin)
11 ficardom 8825 . . . . . . . . 9 ((𝑅1𝑎) ∈ Fin → (card‘(𝑅1𝑎)) ∈ ω)
1210, 11syl 17 . . . . . . . 8 (𝑎 ∈ ω → (card‘(𝑅1𝑎)) ∈ ω)
13 ordelss 5777 . . . . . . . 8 ((Ord ω ∧ (card‘(𝑅1𝑎)) ∈ ω) → (card‘(𝑅1𝑎)) ⊆ ω)
149, 12, 13sylancr 696 . . . . . . 7 (𝑎 ∈ ω → (card‘(𝑅1𝑎)) ⊆ ω)
15 f1ss 6144 . . . . . . 7 (((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→(card‘(𝑅1𝑎)) ∧ (card‘(𝑅1𝑎)) ⊆ ω) → (rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→ω)
168, 14, 15syl2anc 694 . . . . . 6 (𝑎 ∈ ω → (rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→ω)
17 nnord 7115 . . . . . . . . 9 (𝑎 ∈ ω → Ord 𝑎)
18 nnord 7115 . . . . . . . . 9 (𝑏 ∈ ω → Ord 𝑏)
19 ordtri2or2 5861 . . . . . . . . 9 ((Ord 𝑎 ∧ Ord 𝑏) → (𝑎𝑏𝑏𝑎))
2017, 18, 19syl2an 493 . . . . . . . 8 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎𝑏𝑏𝑎))
214, 5ackbij2lem4 9102 . . . . . . . . . . 11 (((𝑏 ∈ ω ∧ 𝑎 ∈ ω) ∧ 𝑎𝑏) → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏))
2221ex 449 . . . . . . . . . 10 ((𝑏 ∈ ω ∧ 𝑎 ∈ ω) → (𝑎𝑏 → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏)))
2322ancoms 468 . . . . . . . . 9 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎𝑏 → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏)))
244, 5ackbij2lem4 9102 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑎) → (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎))
2524ex 449 . . . . . . . . 9 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑏𝑎 → (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)))
2623, 25orim12d 901 . . . . . . . 8 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → ((𝑎𝑏𝑏𝑎) → ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎))))
2720, 26mpd 15 . . . . . . 7 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)))
2827ralrimiva 2995 . . . . . 6 (𝑎 ∈ ω → ∀𝑏 ∈ ω ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)))
2916, 28jca 553 . . . . 5 (𝑎 ∈ ω → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→ω ∧ ∀𝑏 ∈ ω ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎))))
303, 29mprg 2955 . . . 4 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎): 𝑎 ∈ ω (𝑅1𝑎)–1-1→ω
31 rdgfun 7557 . . . . . 6 Fun rec(𝐺, ∅)
32 funiunfv 6546 . . . . . . 7 (Fun rec(𝐺, ∅) → 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅) “ ω))
3332eqcomd 2657 . . . . . 6 (Fun rec(𝐺, ∅) → (rec(𝐺, ∅) “ ω) = 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎))
34 f1eq1 6134 . . . . . 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 8667 . . . . . . 7 (Fun 𝑅1 ∧ Lim dom 𝑅1)
3736simpli 473 . . . . . 6 Fun 𝑅1
38 funiunfv 6546 . . . . . 6 (Fun 𝑅1 𝑎 ∈ ω (𝑅1𝑎) = (𝑅1 “ ω))
39 f1eq2 6135 . . . . . 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 5579 . . . 4 ran (rec(𝐺, ∅) “ ω) = 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎
44 eliun 4556 . . . . . 6 (𝑏 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎 ↔ ∃𝑎 ∈ (rec(𝐺, ∅) “ ω)𝑏 ∈ ran 𝑎)
45 df-rex 2947 . . . . . 6 (∃𝑎 ∈ (rec(𝐺, ∅) “ ω)𝑏 ∈ ran 𝑎 ↔ ∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎))
46 funfn 5956 . . . . . . . . . . . 12 (Fun rec(𝐺, ∅) ↔ rec(𝐺, ∅) Fn dom rec(𝐺, ∅))
4731, 46mpbi 220 . . . . . . . . . . 11 rec(𝐺, ∅) Fn dom rec(𝐺, ∅)
48 rdgdmlim 7558 . . . . . . . . . . . 12 Lim dom rec(𝐺, ∅)
49 limomss 7112 . . . . . . . . . . . 12 (Lim dom rec(𝐺, ∅) → ω ⊆ dom rec(𝐺, ∅))
5048, 49ax-mp 5 . . . . . . . . . . 11 ω ⊆ dom rec(𝐺, ∅)
51 fvelimab 6292 . . . . . . . . . . 11 ((rec(𝐺, ∅) Fn dom rec(𝐺, ∅) ∧ ω ⊆ dom rec(𝐺, ∅)) → (𝑎 ∈ (rec(𝐺, ∅) “ ω) ↔ ∃𝑐 ∈ ω (rec(𝐺, ∅)‘𝑐) = 𝑎))
5247, 50, 51mp2an 708 . . . . . . . . . 10 (𝑎 ∈ (rec(𝐺, ∅) “ ω) ↔ ∃𝑐 ∈ ω (rec(𝐺, ∅)‘𝑐) = 𝑎)
534, 5ackbij2lem2 9100 . . . . . . . . . . . . . 14 (𝑐 ∈ ω → (rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–1-1-onto→(card‘(𝑅1𝑐)))
54 f1ofo 6182 . . . . . . . . . . . . . 14 ((rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–1-1-onto→(card‘(𝑅1𝑐)) → (rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–onto→(card‘(𝑅1𝑐)))
55 forn 6156 . . . . . . . . . . . . . 14 ((rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–onto→(card‘(𝑅1𝑐)) → ran (rec(𝐺, ∅)‘𝑐) = (card‘(𝑅1𝑐)))
5653, 54, 553syl 18 . . . . . . . . . . . . 13 (𝑐 ∈ ω → ran (rec(𝐺, ∅)‘𝑐) = (card‘(𝑅1𝑐)))
57 r1fin 8674 . . . . . . . . . . . . . . 15 (𝑐 ∈ ω → (𝑅1𝑐) ∈ Fin)
58 ficardom 8825 . . . . . . . . . . . . . . 15 ((𝑅1𝑐) ∈ Fin → (card‘(𝑅1𝑐)) ∈ ω)
5957, 58syl 17 . . . . . . . . . . . . . 14 (𝑐 ∈ ω → (card‘(𝑅1𝑐)) ∈ ω)
60 ordelss 5777 . . . . . . . . . . . . . 14 ((Ord ω ∧ (card‘(𝑅1𝑐)) ∈ ω) → (card‘(𝑅1𝑐)) ⊆ ω)
619, 59, 60sylancr 696 . . . . . . . . . . . . 13 (𝑐 ∈ ω → (card‘(𝑅1𝑐)) ⊆ ω)
6256, 61eqsstrd 3672 . . . . . . . . . . . 12 (𝑐 ∈ ω → ran (rec(𝐺, ∅)‘𝑐) ⊆ ω)
63 rneq 5383 . . . . . . . . . . . . 13 ((rec(𝐺, ∅)‘𝑐) = 𝑎 → ran (rec(𝐺, ∅)‘𝑐) = ran 𝑎)
6463sseq1d 3665 . . . . . . . . . . . 12 ((rec(𝐺, ∅)‘𝑐) = 𝑎 → (ran (rec(𝐺, ∅)‘𝑐) ⊆ ω ↔ ran 𝑎 ⊆ ω))
6562, 64syl5ibcom 235 . . . . . . . . . . 11 (𝑐 ∈ ω → ((rec(𝐺, ∅)‘𝑐) = 𝑎 → ran 𝑎 ⊆ ω))
6665rexlimiv 3056 . . . . . . . . . 10 (∃𝑐 ∈ ω (rec(𝐺, ∅)‘𝑐) = 𝑎 → ran 𝑎 ⊆ ω)
6752, 66sylbi 207 . . . . . . . . 9 (𝑎 ∈ (rec(𝐺, ∅) “ ω) → ran 𝑎 ⊆ ω)
6867sselda 3636 . . . . . . . 8 ((𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) → 𝑏 ∈ ω)
6968exlimiv 1898 . . . . . . 7 (∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) → 𝑏 ∈ ω)
70 peano2 7128 . . . . . . . . 9 (𝑏 ∈ ω → suc 𝑏 ∈ ω)
71 fnfvima 6536 . . . . . . . . . 10 ((rec(𝐺, ∅) Fn dom rec(𝐺, ∅) ∧ ω ⊆ dom rec(𝐺, ∅) ∧ suc 𝑏 ∈ ω) → (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω))
7247, 50, 71mp3an12 1454 . . . . . . . . 9 (suc 𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω))
7370, 72syl 17 . . . . . . . 8 (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω))
74 vex 3234 . . . . . . . . . 10 𝑏 ∈ V
75 cardnn 8827 . . . . . . . . . . . 12 (suc 𝑏 ∈ ω → (card‘suc 𝑏) = suc 𝑏)
76 fvex 6239 . . . . . . . . . . . . . 14 (𝑅1‘suc 𝑏) ∈ V
7736simpri 477 . . . . . . . . . . . . . . . . 17 Lim dom 𝑅1
78 limomss 7112 . . . . . . . . . . . . . . . . 17 (Lim dom 𝑅1 → ω ⊆ dom 𝑅1)
7977, 78ax-mp 5 . . . . . . . . . . . . . . . 16 ω ⊆ dom 𝑅1
8079sseli 3632 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ ω → suc 𝑏 ∈ dom 𝑅1)
81 onssr1 8732 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ dom 𝑅1 → suc 𝑏 ⊆ (𝑅1‘suc 𝑏))
8280, 81syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ ω → suc 𝑏 ⊆ (𝑅1‘suc 𝑏))
83 ssdomg 8043 . . . . . . . . . . . . . 14 ((𝑅1‘suc 𝑏) ∈ V → (suc 𝑏 ⊆ (𝑅1‘suc 𝑏) → suc 𝑏 ≼ (𝑅1‘suc 𝑏)))
8476, 82, 83mpsyl 68 . . . . . . . . . . . . 13 (suc 𝑏 ∈ ω → suc 𝑏 ≼ (𝑅1‘suc 𝑏))
85 nnon 7113 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ ω → suc 𝑏 ∈ On)
86 onenon 8813 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ On → suc 𝑏 ∈ dom card)
8785, 86syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ ω → suc 𝑏 ∈ dom card)
88 r1fin 8674 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ ω → (𝑅1‘suc 𝑏) ∈ Fin)
89 finnum 8812 . . . . . . . . . . . . . . 15 ((𝑅1‘suc 𝑏) ∈ Fin → (𝑅1‘suc 𝑏) ∈ dom card)
9088, 89syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ ω → (𝑅1‘suc 𝑏) ∈ dom card)
91 carddom2 8841 . . . . . . . . . . . . . 14 ((suc 𝑏 ∈ dom card ∧ (𝑅1‘suc 𝑏) ∈ dom card) → ((card‘suc 𝑏) ⊆ (card‘(𝑅1‘suc 𝑏)) ↔ suc 𝑏 ≼ (𝑅1‘suc 𝑏)))
9287, 90, 91syl2anc 694 . . . . . . . . . . . . 13 (suc 𝑏 ∈ ω → ((card‘suc 𝑏) ⊆ (card‘(𝑅1‘suc 𝑏)) ↔ suc 𝑏 ≼ (𝑅1‘suc 𝑏)))
9384, 92mpbird 247 . . . . . . . . . . . 12 (suc 𝑏 ∈ ω → (card‘suc 𝑏) ⊆ (card‘(𝑅1‘suc 𝑏)))
9475, 93eqsstr3d 3673 . . . . . . . . . . 11 (suc 𝑏 ∈ ω → suc 𝑏 ⊆ (card‘(𝑅1‘suc 𝑏)))
9570, 94syl 17 . . . . . . . . . 10 (𝑏 ∈ ω → suc 𝑏 ⊆ (card‘(𝑅1‘suc 𝑏)))
96 sucssel 5857 . . . . . . . . . 10 (𝑏 ∈ V → (suc 𝑏 ⊆ (card‘(𝑅1‘suc 𝑏)) → 𝑏 ∈ (card‘(𝑅1‘suc 𝑏))))
9774, 95, 96mpsyl 68 . . . . . . . . 9 (𝑏 ∈ ω → 𝑏 ∈ (card‘(𝑅1‘suc 𝑏)))
984, 5ackbij2lem2 9100 . . . . . . . . . 10 (suc 𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)))
99 f1ofo 6182 . . . . . . . . . 10 ((rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)) → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–onto→(card‘(𝑅1‘suc 𝑏)))
100 forn 6156 . . . . . . . . . 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 2733 . . . . . . . 8 (𝑏 ∈ ω → 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏))
103 fvex 6239 . . . . . . . . 9 (rec(𝐺, ∅)‘suc 𝑏) ∈ V
104 eleq1 2718 . . . . . . . . . 10 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑎 ∈ (rec(𝐺, ∅) “ ω) ↔ (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω)))
105 rneq 5383 . . . . . . . . . . 11 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → ran 𝑎 = ran (rec(𝐺, ∅)‘suc 𝑏))
106105eleq2d 2716 . . . . . . . . . 10 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑏 ∈ ran 𝑎𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏)))
107104, 106anbi12d 747 . . . . . . . . 9 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → ((𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) ↔ ((rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏))))
108103, 107spcev 3331 . . . . . . . 8 (((rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏)) → ∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎))
10973, 102, 108syl2anc 694 . . . . . . 7 (𝑏 ∈ ω → ∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎))
11069, 109impbii 199 . . . . . 6 (∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) ↔ 𝑏 ∈ ω)
11144, 45, 1103bitri 286 . . . . 5 (𝑏 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎𝑏 ∈ ω)
112111eqriv 2648 . . . 4 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎 = ω
11343, 112eqtri 2673 . . 3 ran (rec(𝐺, ∅) “ ω) = ω
114 dff1o5 6184 . . 3 ( (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1-onto→ω ↔ ( (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1→ω ∧ ran (rec(𝐺, ∅) “ ω) = ω))
11542, 113, 114mpbir2an 975 . 2 (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1-onto→ω
116 ackbij.h . . 3 𝐻 = (rec(𝐺, ∅) “ ω)
117 f1oeq1 6165 . . 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 1523  wex 1744  wcel 2030  wral 2941  wrex 2942  Vcvv 3231  cin 3606  wss 3607  c0 3948  𝒫 cpw 4191  {csn 4210   cuni 4468   ciun 4552   class class class wbr 4685  cmpt 4762   × cxp 5141  dom cdm 5143  ran crn 5144  cima 5146  Ord word 5760  Oncon0 5761  Lim wlim 5762  suc csuc 5763  Fun wfun 5920   Fn wfn 5921  1-1wf1 5923  ontowfo 5924  1-1-ontowf1o 5925  cfv 5926  ωcom 7107  reccrdg 7550  cdom 7995  Fincfn 7997  𝑅1cr1 8663  cardccrd 8799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-r1 8665  df-rank 8666  df-card 8803  df-cda 9028
This theorem is referenced by:  r1om  9104
  Copyright terms: Public domain W3C validator