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

Theorem ackbij2 9653
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 6663 . . . . . 6 (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏))
2 fvex 6676 . . . . . 6 (rec(𝐺, ∅)‘𝑎) ∈ V
31, 2f1iun 7634 . . . . 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 9650 . . . . . . . 8 (𝑎 ∈ ω → (rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1-onto→(card‘(𝑅1𝑎)))
7 f1of1 6607 . . . . . . . 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 7578 . . . . . . . 8 Ord ω
10 r1fin 9190 . . . . . . . . 9 (𝑎 ∈ ω → (𝑅1𝑎) ∈ Fin)
11 ficardom 9378 . . . . . . . . 9 ((𝑅1𝑎) ∈ Fin → (card‘(𝑅1𝑎)) ∈ ω)
1210, 11syl 17 . . . . . . . 8 (𝑎 ∈ ω → (card‘(𝑅1𝑎)) ∈ ω)
13 ordelss 6200 . . . . . . . 8 ((Ord ω ∧ (card‘(𝑅1𝑎)) ∈ ω) → (card‘(𝑅1𝑎)) ⊆ ω)
149, 12, 13sylancr 587 . . . . . . 7 (𝑎 ∈ ω → (card‘(𝑅1𝑎)) ⊆ ω)
15 f1ss 6573 . . . . . . 7 (((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→(card‘(𝑅1𝑎)) ∧ (card‘(𝑅1𝑎)) ⊆ ω) → (rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→ω)
168, 14, 15syl2anc 584 . . . . . 6 (𝑎 ∈ ω → (rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→ω)
17 nnord 7577 . . . . . . . . 9 (𝑎 ∈ ω → Ord 𝑎)
18 nnord 7577 . . . . . . . . 9 (𝑏 ∈ ω → Ord 𝑏)
19 ordtri2or2 6280 . . . . . . . . 9 ((Ord 𝑎 ∧ Ord 𝑏) → (𝑎𝑏𝑏𝑎))
2017, 18, 19syl2an 595 . . . . . . . 8 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎𝑏𝑏𝑎))
214, 5ackbij2lem4 9652 . . . . . . . . . . 11 (((𝑏 ∈ ω ∧ 𝑎 ∈ ω) ∧ 𝑎𝑏) → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏))
2221ex 413 . . . . . . . . . 10 ((𝑏 ∈ ω ∧ 𝑎 ∈ ω) → (𝑎𝑏 → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏)))
2322ancoms 459 . . . . . . . . 9 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎𝑏 → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏)))
244, 5ackbij2lem4 9652 . . . . . . . . . 10 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏𝑎) → (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎))
2524ex 413 . . . . . . . . 9 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑏𝑎 → (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)))
2623, 25orim12d 958 . . . . . . . 8 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → ((𝑎𝑏𝑏𝑎) → ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎))))
2720, 26mpd 15 . . . . . . 7 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)))
2827ralrimiva 3179 . . . . . 6 (𝑎 ∈ ω → ∀𝑏 ∈ ω ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)))
2916, 28jca 512 . . . . 5 (𝑎 ∈ ω → ((rec(𝐺, ∅)‘𝑎):(𝑅1𝑎)–1-1→ω ∧ ∀𝑏 ∈ ω ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎))))
303, 29mprg 3149 . . . 4 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎): 𝑎 ∈ ω (𝑅1𝑎)–1-1→ω
31 rdgfun 8041 . . . . . 6 Fun rec(𝐺, ∅)
32 funiunfv 6998 . . . . . . 7 (Fun rec(𝐺, ∅) → 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅) “ ω))
3332eqcomd 2824 . . . . . 6 (Fun rec(𝐺, ∅) → (rec(𝐺, ∅) “ ω) = 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎))
34 f1eq1 6563 . . . . . 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 9183 . . . . . . 7 (Fun 𝑅1 ∧ Lim dom 𝑅1)
3736simpli 484 . . . . . 6 Fun 𝑅1
38 funiunfv 6998 . . . . . 6 (Fun 𝑅1 𝑎 ∈ ω (𝑅1𝑎) = (𝑅1 “ ω))
39 f1eq2 6564 . . . . . 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 279 . . . 4 ( (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1→ω ↔ 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎): 𝑎 ∈ ω (𝑅1𝑎)–1-1→ω)
4230, 41mpbir 232 . . 3 (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1→ω
43 rnuni 6000 . . . 4 ran (rec(𝐺, ∅) “ ω) = 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎
44 eliun 4914 . . . . . 6 (𝑏 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎 ↔ ∃𝑎 ∈ (rec(𝐺, ∅) “ ω)𝑏 ∈ ran 𝑎)
45 df-rex 3141 . . . . . 6 (∃𝑎 ∈ (rec(𝐺, ∅) “ ω)𝑏 ∈ ran 𝑎 ↔ ∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎))
46 funfn 6378 . . . . . . . . . . . 12 (Fun rec(𝐺, ∅) ↔ rec(𝐺, ∅) Fn dom rec(𝐺, ∅))
4731, 46mpbi 231 . . . . . . . . . . 11 rec(𝐺, ∅) Fn dom rec(𝐺, ∅)
48 rdgdmlim 8042 . . . . . . . . . . . 12 Lim dom rec(𝐺, ∅)
49 limomss 7574 . . . . . . . . . . . 12 (Lim dom rec(𝐺, ∅) → ω ⊆ dom rec(𝐺, ∅))
5048, 49ax-mp 5 . . . . . . . . . . 11 ω ⊆ dom rec(𝐺, ∅)
51 fvelimab 6730 . . . . . . . . . . 11 ((rec(𝐺, ∅) Fn dom rec(𝐺, ∅) ∧ ω ⊆ dom rec(𝐺, ∅)) → (𝑎 ∈ (rec(𝐺, ∅) “ ω) ↔ ∃𝑐 ∈ ω (rec(𝐺, ∅)‘𝑐) = 𝑎))
5247, 50, 51mp2an 688 . . . . . . . . . 10 (𝑎 ∈ (rec(𝐺, ∅) “ ω) ↔ ∃𝑐 ∈ ω (rec(𝐺, ∅)‘𝑐) = 𝑎)
534, 5ackbij2lem2 9650 . . . . . . . . . . . . . 14 (𝑐 ∈ ω → (rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–1-1-onto→(card‘(𝑅1𝑐)))
54 f1ofo 6615 . . . . . . . . . . . . . 14 ((rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–1-1-onto→(card‘(𝑅1𝑐)) → (rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–onto→(card‘(𝑅1𝑐)))
55 forn 6586 . . . . . . . . . . . . . 14 ((rec(𝐺, ∅)‘𝑐):(𝑅1𝑐)–onto→(card‘(𝑅1𝑐)) → ran (rec(𝐺, ∅)‘𝑐) = (card‘(𝑅1𝑐)))
5653, 54, 553syl 18 . . . . . . . . . . . . 13 (𝑐 ∈ ω → ran (rec(𝐺, ∅)‘𝑐) = (card‘(𝑅1𝑐)))
57 r1fin 9190 . . . . . . . . . . . . . . 15 (𝑐 ∈ ω → (𝑅1𝑐) ∈ Fin)
58 ficardom 9378 . . . . . . . . . . . . . . 15 ((𝑅1𝑐) ∈ Fin → (card‘(𝑅1𝑐)) ∈ ω)
5957, 58syl 17 . . . . . . . . . . . . . 14 (𝑐 ∈ ω → (card‘(𝑅1𝑐)) ∈ ω)
60 ordelss 6200 . . . . . . . . . . . . . 14 ((Ord ω ∧ (card‘(𝑅1𝑐)) ∈ ω) → (card‘(𝑅1𝑐)) ⊆ ω)
619, 59, 60sylancr 587 . . . . . . . . . . . . 13 (𝑐 ∈ ω → (card‘(𝑅1𝑐)) ⊆ ω)
6256, 61eqsstrd 4002 . . . . . . . . . . . 12 (𝑐 ∈ ω → ran (rec(𝐺, ∅)‘𝑐) ⊆ ω)
63 rneq 5799 . . . . . . . . . . . . 13 ((rec(𝐺, ∅)‘𝑐) = 𝑎 → ran (rec(𝐺, ∅)‘𝑐) = ran 𝑎)
6463sseq1d 3995 . . . . . . . . . . . 12 ((rec(𝐺, ∅)‘𝑐) = 𝑎 → (ran (rec(𝐺, ∅)‘𝑐) ⊆ ω ↔ ran 𝑎 ⊆ ω))
6562, 64syl5ibcom 246 . . . . . . . . . . 11 (𝑐 ∈ ω → ((rec(𝐺, ∅)‘𝑐) = 𝑎 → ran 𝑎 ⊆ ω))
6665rexlimiv 3277 . . . . . . . . . 10 (∃𝑐 ∈ ω (rec(𝐺, ∅)‘𝑐) = 𝑎 → ran 𝑎 ⊆ ω)
6752, 66sylbi 218 . . . . . . . . 9 (𝑎 ∈ (rec(𝐺, ∅) “ ω) → ran 𝑎 ⊆ ω)
6867sselda 3964 . . . . . . . 8 ((𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) → 𝑏 ∈ ω)
6968exlimiv 1922 . . . . . . 7 (∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) → 𝑏 ∈ ω)
70 peano2 7591 . . . . . . . . 9 (𝑏 ∈ ω → suc 𝑏 ∈ ω)
71 fnfvima 6986 . . . . . . . . 9 ((rec(𝐺, ∅) Fn dom rec(𝐺, ∅) ∧ ω ⊆ dom rec(𝐺, ∅) ∧ suc 𝑏 ∈ ω) → (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω))
7247, 50, 70, 71mp3an12i 1456 . . . . . . . 8 (𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω))
73 vex 3495 . . . . . . . . . 10 𝑏 ∈ V
74 cardnn 9380 . . . . . . . . . . . 12 (suc 𝑏 ∈ ω → (card‘suc 𝑏) = suc 𝑏)
75 fvex 6676 . . . . . . . . . . . . . 14 (𝑅1‘suc 𝑏) ∈ V
7636simpri 486 . . . . . . . . . . . . . . . . 17 Lim dom 𝑅1
77 limomss 7574 . . . . . . . . . . . . . . . . 17 (Lim dom 𝑅1 → ω ⊆ dom 𝑅1)
7876, 77ax-mp 5 . . . . . . . . . . . . . . . 16 ω ⊆ dom 𝑅1
7978sseli 3960 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ ω → suc 𝑏 ∈ dom 𝑅1)
80 onssr1 9248 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ dom 𝑅1 → suc 𝑏 ⊆ (𝑅1‘suc 𝑏))
8179, 80syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ ω → suc 𝑏 ⊆ (𝑅1‘suc 𝑏))
82 ssdomg 8543 . . . . . . . . . . . . . 14 ((𝑅1‘suc 𝑏) ∈ V → (suc 𝑏 ⊆ (𝑅1‘suc 𝑏) → suc 𝑏 ≼ (𝑅1‘suc 𝑏)))
8375, 81, 82mpsyl 68 . . . . . . . . . . . . 13 (suc 𝑏 ∈ ω → suc 𝑏 ≼ (𝑅1‘suc 𝑏))
84 nnon 7575 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ ω → suc 𝑏 ∈ On)
85 onenon 9366 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ On → suc 𝑏 ∈ dom card)
8684, 85syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ ω → suc 𝑏 ∈ dom card)
87 r1fin 9190 . . . . . . . . . . . . . . 15 (suc 𝑏 ∈ ω → (𝑅1‘suc 𝑏) ∈ Fin)
88 finnum 9365 . . . . . . . . . . . . . . 15 ((𝑅1‘suc 𝑏) ∈ Fin → (𝑅1‘suc 𝑏) ∈ dom card)
8987, 88syl 17 . . . . . . . . . . . . . 14 (suc 𝑏 ∈ ω → (𝑅1‘suc 𝑏) ∈ dom card)
90 carddom2 9394 . . . . . . . . . . . . . 14 ((suc 𝑏 ∈ dom card ∧ (𝑅1‘suc 𝑏) ∈ dom card) → ((card‘suc 𝑏) ⊆ (card‘(𝑅1‘suc 𝑏)) ↔ suc 𝑏 ≼ (𝑅1‘suc 𝑏)))
9186, 89, 90syl2anc 584 . . . . . . . . . . . . 13 (suc 𝑏 ∈ ω → ((card‘suc 𝑏) ⊆ (card‘(𝑅1‘suc 𝑏)) ↔ suc 𝑏 ≼ (𝑅1‘suc 𝑏)))
9283, 91mpbird 258 . . . . . . . . . . . 12 (suc 𝑏 ∈ ω → (card‘suc 𝑏) ⊆ (card‘(𝑅1‘suc 𝑏)))
9374, 92eqsstrrd 4003 . . . . . . . . . . 11 (suc 𝑏 ∈ ω → suc 𝑏 ⊆ (card‘(𝑅1‘suc 𝑏)))
9470, 93syl 17 . . . . . . . . . 10 (𝑏 ∈ ω → suc 𝑏 ⊆ (card‘(𝑅1‘suc 𝑏)))
95 sucssel 6276 . . . . . . . . . 10 (𝑏 ∈ V → (suc 𝑏 ⊆ (card‘(𝑅1‘suc 𝑏)) → 𝑏 ∈ (card‘(𝑅1‘suc 𝑏))))
9673, 94, 95mpsyl 68 . . . . . . . . 9 (𝑏 ∈ ω → 𝑏 ∈ (card‘(𝑅1‘suc 𝑏)))
974, 5ackbij2lem2 9650 . . . . . . . . . 10 (suc 𝑏 ∈ ω → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)))
98 f1ofo 6615 . . . . . . . . . 10 ((rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc 𝑏)) → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–onto→(card‘(𝑅1‘suc 𝑏)))
99 forn 6586 . . . . . . . . . 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 2913 . . . . . . . 8 (𝑏 ∈ ω → 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏))
102 fvex 6676 . . . . . . . . 9 (rec(𝐺, ∅)‘suc 𝑏) ∈ V
103 eleq1 2897 . . . . . . . . . 10 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑎 ∈ (rec(𝐺, ∅) “ ω) ↔ (rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω)))
104 rneq 5799 . . . . . . . . . . 11 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → ran 𝑎 = ran (rec(𝐺, ∅)‘suc 𝑏))
105104eleq2d 2895 . . . . . . . . . 10 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑏 ∈ ran 𝑎𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏)))
106103, 105anbi12d 630 . . . . . . . . 9 (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → ((𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) ↔ ((rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏))))
107102, 106spcev 3604 . . . . . . . 8 (((rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏)) → ∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎))
10872, 101, 107syl2anc 584 . . . . . . 7 (𝑏 ∈ ω → ∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎))
10969, 108impbii 210 . . . . . 6 (∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) ↔ 𝑏 ∈ ω)
11044, 45, 1093bitri 298 . . . . 5 (𝑏 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎𝑏 ∈ ω)
111110eqriv 2815 . . . 4 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎 = ω
11243, 111eqtri 2841 . . 3 ran (rec(𝐺, ∅) “ ω) = ω
113 dff1o5 6617 . . 3 ( (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1-onto→ω ↔ ( (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1→ω ∧ ran (rec(𝐺, ∅) “ ω) = ω))
11442, 112, 113mpbir2an 707 . 2 (rec(𝐺, ∅) “ ω): (𝑅1 “ ω)–1-1-onto→ω
115 ackbij.h . . 3 𝐻 = (rec(𝐺, ∅) “ ω)
116 f1oeq1 6597 . . 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 232 1 𝐻: (𝑅1 “ ω)–1-1-onto→ω
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 841   = wceq 1528  wex 1771  wcel 2105  wral 3135  wrex 3136  Vcvv 3492  cin 3932  wss 3933  c0 4288  𝒫 cpw 4535  {csn 4557   cuni 4830   ciun 4910   class class class wbr 5057  cmpt 5137   × cxp 5546  dom cdm 5548  ran crn 5549  cima 5551  Ord word 6183  Oncon0 6184  Lim wlim 6185  suc csuc 6186  Fun wfun 6342   Fn wfn 6343  1-1wf1 6345  ontowfo 6346  1-1-ontowf1o 6347  cfv 6348  ωcom 7569  reccrdg 8034  cdom 8495  Fincfn 8497  𝑅1cr1 9179  cardccrd 9352
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-er 8278  df-map 8397  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-r1 9181  df-rank 9182  df-dju 9318  df-card 9356
This theorem is referenced by:  r1om  9654
  Copyright terms: Public domain W3C validator