Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (rec(𝐺, ∅)‘𝑎) = (rec(𝐺, ∅)‘𝑏)) |
2 | | fvex 6113 |
. . . . . 6
⊢
(rec(𝐺,
∅)‘𝑎) ∈
V |
3 | 1, 2 | fun11iun 7019 |
. . . . 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 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦)))) |
6 | 4, 5 | ackbij2lem2 8945 |
. . . . . . . 8
⊢ (𝑎 ∈ ω →
(rec(𝐺,
∅)‘𝑎):(𝑅1‘𝑎)–1-1-onto→(card‘(𝑅1‘𝑎))) |
7 | | f1of1 6049 |
. . . . . . . 8
⊢
((rec(𝐺,
∅)‘𝑎):(𝑅1‘𝑎)–1-1-onto→(card‘(𝑅1‘𝑎)) → (rec(𝐺, ∅)‘𝑎):(𝑅1‘𝑎)–1-1→(card‘(𝑅1‘𝑎))) |
8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ (𝑎 ∈ ω →
(rec(𝐺,
∅)‘𝑎):(𝑅1‘𝑎)–1-1→(card‘(𝑅1‘𝑎))) |
9 | | ordom 6966 |
. . . . . . . 8
⊢ Ord
ω |
10 | | r1fin 8519 |
. . . . . . . . 9
⊢ (𝑎 ∈ ω →
(𝑅1‘𝑎) ∈ Fin) |
11 | | ficardom 8670 |
. . . . . . . . 9
⊢
((𝑅1‘𝑎) ∈ Fin →
(card‘(𝑅1‘𝑎)) ∈ ω) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝑎 ∈ ω →
(card‘(𝑅1‘𝑎)) ∈ ω) |
13 | | ordelss 5656 |
. . . . . . . 8
⊢ ((Ord
ω ∧ (card‘(𝑅1‘𝑎)) ∈ ω) →
(card‘(𝑅1‘𝑎)) ⊆ ω) |
14 | 9, 12, 13 | sylancr 694 |
. . . . . . 7
⊢ (𝑎 ∈ ω →
(card‘(𝑅1‘𝑎)) ⊆ ω) |
15 | | f1ss 6019 |
. . . . . . 7
⊢
(((rec(𝐺,
∅)‘𝑎):(𝑅1‘𝑎)–1-1→(card‘(𝑅1‘𝑎)) ∧
(card‘(𝑅1‘𝑎)) ⊆ ω) → (rec(𝐺, ∅)‘𝑎):(𝑅1‘𝑎)–1-1→ω) |
16 | 8, 14, 15 | syl2anc 691 |
. . . . . 6
⊢ (𝑎 ∈ ω →
(rec(𝐺,
∅)‘𝑎):(𝑅1‘𝑎)–1-1→ω) |
17 | | nnord 6965 |
. . . . . . . . 9
⊢ (𝑎 ∈ ω → Ord 𝑎) |
18 | | nnord 6965 |
. . . . . . . . 9
⊢ (𝑏 ∈ ω → Ord 𝑏) |
19 | | ordtri2or2 5740 |
. . . . . . . . 9
⊢ ((Ord
𝑎 ∧ Ord 𝑏) → (𝑎 ⊆ 𝑏 ∨ 𝑏 ⊆ 𝑎)) |
20 | 17, 18, 19 | syl2an 493 |
. . . . . . . 8
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎 ⊆ 𝑏 ∨ 𝑏 ⊆ 𝑎)) |
21 | 4, 5 | ackbij2lem4 8947 |
. . . . . . . . . . 11
⊢ (((𝑏 ∈ ω ∧ 𝑎 ∈ ω) ∧ 𝑎 ⊆ 𝑏) → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏)) |
22 | 21 | ex 449 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ω ∧ 𝑎 ∈ ω) → (𝑎 ⊆ 𝑏 → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏))) |
23 | 22 | ancoms 468 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎 ⊆ 𝑏 → (rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏))) |
24 | 4, 5 | ackbij2lem4 8947 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑏 ⊆ 𝑎) → (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)) |
25 | 24 | ex 449 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑏 ⊆ 𝑎 → (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎))) |
26 | 23, 25 | orim12d 879 |
. . . . . . . 8
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → ((𝑎 ⊆ 𝑏 ∨ 𝑏 ⊆ 𝑎) → ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)))) |
27 | 20, 26 | mpd 15 |
. . . . . . 7
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) →
((rec(𝐺,
∅)‘𝑎) ⊆
(rec(𝐺,
∅)‘𝑏) ∨
(rec(𝐺,
∅)‘𝑏) ⊆
(rec(𝐺,
∅)‘𝑎))) |
28 | 27 | ralrimiva 2949 |
. . . . . 6
⊢ (𝑎 ∈ ω →
∀𝑏 ∈ ω
((rec(𝐺,
∅)‘𝑎) ⊆
(rec(𝐺,
∅)‘𝑏) ∨
(rec(𝐺,
∅)‘𝑏) ⊆
(rec(𝐺,
∅)‘𝑎))) |
29 | 16, 28 | jca 553 |
. . . . 5
⊢ (𝑎 ∈ ω →
((rec(𝐺,
∅)‘𝑎):(𝑅1‘𝑎)–1-1→ω ∧ ∀𝑏 ∈ ω ((rec(𝐺, ∅)‘𝑎) ⊆ (rec(𝐺, ∅)‘𝑏) ∨ (rec(𝐺, ∅)‘𝑏) ⊆ (rec(𝐺, ∅)‘𝑎)))) |
30 | 3, 29 | mprg 2910 |
. . . 4
⊢ ∪ 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎):∪ 𝑎 ∈ ω
(𝑅1‘𝑎)–1-1→ω |
31 | | rdgfun 7399 |
. . . . . 6
⊢ Fun
rec(𝐺,
∅) |
32 | | funiunfv 6410 |
. . . . . . 7
⊢ (Fun
rec(𝐺, ∅) →
∪ 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎) = ∪ (rec(𝐺, ∅) “
ω)) |
33 | 32 | eqcomd 2616 |
. . . . . 6
⊢ (Fun
rec(𝐺, ∅) →
∪ (rec(𝐺, ∅) “ ω) = ∪ 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎)) |
34 | | f1eq1 6009 |
. . . . . 6
⊢ (∪ (rec(𝐺, ∅) “ ω) = ∪ 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎) → (∪
(rec(𝐺, ∅) “
ω):∪ (𝑅1 “
ω)–1-1→ω ↔
∪ 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎):∪
(𝑅1 “ ω)–1-1→ω)) |
35 | 31, 33, 34 | mp2b 10 |
. . . . 5
⊢ (∪ (rec(𝐺, ∅) “ ω):∪ (𝑅1 “ ω)–1-1→ω ↔ ∪ 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎):∪
(𝑅1 “ ω)–1-1→ω) |
36 | | r1funlim 8512 |
. . . . . . 7
⊢ (Fun
𝑅1 ∧ Lim dom 𝑅1) |
37 | 36 | simpli 473 |
. . . . . 6
⊢ Fun
𝑅1 |
38 | | funiunfv 6410 |
. . . . . 6
⊢ (Fun
𝑅1 → ∪ 𝑎 ∈ ω
(𝑅1‘𝑎) = ∪
(𝑅1 “ ω)) |
39 | | f1eq2 6010 |
. . . . . 6
⊢ (∪ 𝑎 ∈ ω
(𝑅1‘𝑎) = ∪
(𝑅1 “ ω) → (∪ 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎):∪ 𝑎 ∈ ω
(𝑅1‘𝑎)–1-1→ω ↔ ∪ 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎):∪
(𝑅1 “ ω)–1-1→ω)) |
40 | 37, 38, 39 | mp2b 10 |
. . . . 5
⊢ (∪ 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎):∪ 𝑎 ∈ ω
(𝑅1‘𝑎)–1-1→ω ↔ ∪ 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎):∪
(𝑅1 “ ω)–1-1→ω) |
41 | 35, 40 | bitr4i 266 |
. . . 4
⊢ (∪ (rec(𝐺, ∅) “ ω):∪ (𝑅1 “ ω)–1-1→ω ↔ ∪ 𝑎 ∈ ω (rec(𝐺, ∅)‘𝑎):∪ 𝑎 ∈ ω
(𝑅1‘𝑎)–1-1→ω) |
42 | 30, 41 | mpbir 220 |
. . 3
⊢ ∪ (rec(𝐺, ∅) “ ω):∪ (𝑅1 “ ω)–1-1→ω |
43 | | rnuni 5463 |
. . . 4
⊢ ran ∪ (rec(𝐺, ∅) “ ω) = ∪ 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎 |
44 | | eliun 4460 |
. . . . . 6
⊢ (𝑏 ∈ ∪ 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎 ↔ ∃𝑎 ∈ (rec(𝐺, ∅) “ ω)𝑏 ∈ ran 𝑎) |
45 | | df-rex 2902 |
. . . . . 6
⊢
(∃𝑎 ∈
(rec(𝐺, ∅) “
ω)𝑏 ∈ ran 𝑎 ↔ ∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎)) |
46 | | funfn 5833 |
. . . . . . . . . . . 12
⊢ (Fun
rec(𝐺, ∅) ↔
rec(𝐺, ∅) Fn dom
rec(𝐺,
∅)) |
47 | 31, 46 | mpbi 219 |
. . . . . . . . . . 11
⊢ rec(𝐺, ∅) Fn dom rec(𝐺, ∅) |
48 | | rdgdmlim 7400 |
. . . . . . . . . . . 12
⊢ Lim dom
rec(𝐺,
∅) |
49 | | limomss 6962 |
. . . . . . . . . . . 12
⊢ (Lim dom
rec(𝐺, ∅) →
ω ⊆ dom rec(𝐺,
∅)) |
50 | 48, 49 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ω
⊆ dom rec(𝐺,
∅) |
51 | | fvelimab 6163 |
. . . . . . . . . . 11
⊢
((rec(𝐺, ∅) Fn
dom rec(𝐺, ∅) ∧
ω ⊆ dom rec(𝐺,
∅)) → (𝑎 ∈
(rec(𝐺, ∅) “
ω) ↔ ∃𝑐
∈ ω (rec(𝐺,
∅)‘𝑐) = 𝑎)) |
52 | 47, 50, 51 | mp2an 704 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (rec(𝐺, ∅) “ ω) ↔
∃𝑐 ∈ ω
(rec(𝐺,
∅)‘𝑐) = 𝑎) |
53 | 4, 5 | ackbij2lem2 8945 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ ω →
(rec(𝐺,
∅)‘𝑐):(𝑅1‘𝑐)–1-1-onto→(card‘(𝑅1‘𝑐))) |
54 | | f1ofo 6057 |
. . . . . . . . . . . . . 14
⊢
((rec(𝐺,
∅)‘𝑐):(𝑅1‘𝑐)–1-1-onto→(card‘(𝑅1‘𝑐)) → (rec(𝐺, ∅)‘𝑐):(𝑅1‘𝑐)–onto→(card‘(𝑅1‘𝑐))) |
55 | | forn 6031 |
. . . . . . . . . . . . . 14
⊢
((rec(𝐺,
∅)‘𝑐):(𝑅1‘𝑐)–onto→(card‘(𝑅1‘𝑐)) → ran (rec(𝐺, ∅)‘𝑐) =
(card‘(𝑅1‘𝑐))) |
56 | 53, 54, 55 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ ω → ran
(rec(𝐺,
∅)‘𝑐) =
(card‘(𝑅1‘𝑐))) |
57 | | r1fin 8519 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ ω →
(𝑅1‘𝑐) ∈ Fin) |
58 | | ficardom 8670 |
. . . . . . . . . . . . . . 15
⊢
((𝑅1‘𝑐) ∈ Fin →
(card‘(𝑅1‘𝑐)) ∈ ω) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ ω →
(card‘(𝑅1‘𝑐)) ∈ ω) |
60 | | ordelss 5656 |
. . . . . . . . . . . . . 14
⊢ ((Ord
ω ∧ (card‘(𝑅1‘𝑐)) ∈ ω) →
(card‘(𝑅1‘𝑐)) ⊆ ω) |
61 | 9, 59, 60 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ ω →
(card‘(𝑅1‘𝑐)) ⊆ ω) |
62 | 56, 61 | eqsstrd 3602 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ ω → ran
(rec(𝐺,
∅)‘𝑐) ⊆
ω) |
63 | | rneq 5272 |
. . . . . . . . . . . . 13
⊢
((rec(𝐺,
∅)‘𝑐) = 𝑎 → ran (rec(𝐺, ∅)‘𝑐) = ran 𝑎) |
64 | 63 | sseq1d 3595 |
. . . . . . . . . . . 12
⊢
((rec(𝐺,
∅)‘𝑐) = 𝑎 → (ran (rec(𝐺, ∅)‘𝑐) ⊆ ω ↔ ran
𝑎 ⊆
ω)) |
65 | 62, 64 | syl5ibcom 234 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ ω →
((rec(𝐺,
∅)‘𝑐) = 𝑎 → ran 𝑎 ⊆ ω)) |
66 | 65 | rexlimiv 3009 |
. . . . . . . . . 10
⊢
(∃𝑐 ∈
ω (rec(𝐺,
∅)‘𝑐) = 𝑎 → ran 𝑎 ⊆ ω) |
67 | 52, 66 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑎 ∈ (rec(𝐺, ∅) “ ω) → ran 𝑎 ⊆
ω) |
68 | 67 | sselda 3568 |
. . . . . . . 8
⊢ ((𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) → 𝑏 ∈ ω) |
69 | 68 | exlimiv 1845 |
. . . . . . 7
⊢
(∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) → 𝑏 ∈ ω) |
70 | | peano2 6978 |
. . . . . . . . 9
⊢ (𝑏 ∈ ω → suc 𝑏 ∈
ω) |
71 | | fnfvima 6400 |
. . . . . . . . . 10
⊢
((rec(𝐺, ∅) Fn
dom rec(𝐺, ∅) ∧
ω ⊆ dom rec(𝐺,
∅) ∧ suc 𝑏 ∈
ω) → (rec(𝐺,
∅)‘suc 𝑏)
∈ (rec(𝐺, ∅)
“ ω)) |
72 | 47, 50, 71 | mp3an12 1406 |
. . . . . . . . 9
⊢ (suc
𝑏 ∈ ω →
(rec(𝐺, ∅)‘suc
𝑏) ∈ (rec(𝐺, ∅) “
ω)) |
73 | 70, 72 | syl 17 |
. . . . . . . 8
⊢ (𝑏 ∈ ω →
(rec(𝐺, ∅)‘suc
𝑏) ∈ (rec(𝐺, ∅) “
ω)) |
74 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
75 | | cardnn 8672 |
. . . . . . . . . . . 12
⊢ (suc
𝑏 ∈ ω →
(card‘suc 𝑏) = suc
𝑏) |
76 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(𝑅1‘suc 𝑏) ∈ V |
77 | 36 | simpri 477 |
. . . . . . . . . . . . . . . . 17
⊢ Lim dom
𝑅1 |
78 | | limomss 6962 |
. . . . . . . . . . . . . . . . 17
⊢ (Lim dom
𝑅1 → ω ⊆ dom
𝑅1) |
79 | 77, 78 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ω
⊆ dom 𝑅1 |
80 | 79 | sseli 3564 |
. . . . . . . . . . . . . . 15
⊢ (suc
𝑏 ∈ ω → suc
𝑏 ∈ dom
𝑅1) |
81 | | onssr1 8577 |
. . . . . . . . . . . . . . 15
⊢ (suc
𝑏 ∈ dom
𝑅1 → suc 𝑏 ⊆ (𝑅1‘suc
𝑏)) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (suc
𝑏 ∈ ω → suc
𝑏 ⊆
(𝑅1‘suc 𝑏)) |
83 | | ssdomg 7887 |
. . . . . . . . . . . . . 14
⊢
((𝑅1‘suc 𝑏) ∈ V → (suc 𝑏 ⊆ (𝑅1‘suc
𝑏) → suc 𝑏 ≼
(𝑅1‘suc 𝑏))) |
84 | 76, 82, 83 | mpsyl 66 |
. . . . . . . . . . . . 13
⊢ (suc
𝑏 ∈ ω → suc
𝑏 ≼
(𝑅1‘suc 𝑏)) |
85 | | nnon 6963 |
. . . . . . . . . . . . . . 15
⊢ (suc
𝑏 ∈ ω → suc
𝑏 ∈
On) |
86 | | onenon 8658 |
. . . . . . . . . . . . . . 15
⊢ (suc
𝑏 ∈ On → suc
𝑏 ∈ dom
card) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (suc
𝑏 ∈ ω → suc
𝑏 ∈ dom
card) |
88 | | r1fin 8519 |
. . . . . . . . . . . . . . 15
⊢ (suc
𝑏 ∈ ω →
(𝑅1‘suc 𝑏) ∈ Fin) |
89 | | finnum 8657 |
. . . . . . . . . . . . . . 15
⊢
((𝑅1‘suc 𝑏) ∈ Fin →
(𝑅1‘suc 𝑏) ∈ dom card) |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (suc
𝑏 ∈ ω →
(𝑅1‘suc 𝑏) ∈ dom card) |
91 | | carddom2 8686 |
. . . . . . . . . . . . . 14
⊢ ((suc
𝑏 ∈ dom card ∧
(𝑅1‘suc 𝑏) ∈ dom card) → ((card‘suc
𝑏) ⊆
(card‘(𝑅1‘suc 𝑏)) ↔ suc 𝑏 ≼ (𝑅1‘suc
𝑏))) |
92 | 87, 90, 91 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (suc
𝑏 ∈ ω →
((card‘suc 𝑏) ⊆
(card‘(𝑅1‘suc 𝑏)) ↔ suc 𝑏 ≼ (𝑅1‘suc
𝑏))) |
93 | 84, 92 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (suc
𝑏 ∈ ω →
(card‘suc 𝑏) ⊆
(card‘(𝑅1‘suc 𝑏))) |
94 | 75, 93 | eqsstr3d 3603 |
. . . . . . . . . . 11
⊢ (suc
𝑏 ∈ ω → suc
𝑏 ⊆
(card‘(𝑅1‘suc 𝑏))) |
95 | 70, 94 | syl 17 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ω → suc 𝑏 ⊆
(card‘(𝑅1‘suc 𝑏))) |
96 | | sucssel 5736 |
. . . . . . . . . 10
⊢ (𝑏 ∈ V → (suc 𝑏 ⊆
(card‘(𝑅1‘suc 𝑏)) → 𝑏 ∈
(card‘(𝑅1‘suc 𝑏)))) |
97 | 74, 95, 96 | mpsyl 66 |
. . . . . . . . 9
⊢ (𝑏 ∈ ω → 𝑏 ∈
(card‘(𝑅1‘suc 𝑏))) |
98 | 4, 5 | ackbij2lem2 8945 |
. . . . . . . . . 10
⊢ (suc
𝑏 ∈ ω →
(rec(𝐺, ∅)‘suc
𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
𝑏))) |
99 | | f1ofo 6057 |
. . . . . . . . . 10
⊢
((rec(𝐺,
∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–1-1-onto→(card‘(𝑅1‘suc
𝑏)) → (rec(𝐺, ∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–onto→(card‘(𝑅1‘suc
𝑏))) |
100 | | forn 6031 |
. . . . . . . . . 10
⊢
((rec(𝐺,
∅)‘suc 𝑏):(𝑅1‘suc 𝑏)–onto→(card‘(𝑅1‘suc
𝑏)) → ran (rec(𝐺, ∅)‘suc 𝑏) =
(card‘(𝑅1‘suc 𝑏))) |
101 | 70, 98, 99, 100 | 4syl 19 |
. . . . . . . . 9
⊢ (𝑏 ∈ ω → ran
(rec(𝐺, ∅)‘suc
𝑏) =
(card‘(𝑅1‘suc 𝑏))) |
102 | 97, 101 | eleqtrrd 2691 |
. . . . . . . 8
⊢ (𝑏 ∈ ω → 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏)) |
103 | | fvex 6113 |
. . . . . . . . 9
⊢
(rec(𝐺,
∅)‘suc 𝑏)
∈ V |
104 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑎 ∈ (rec(𝐺, ∅) “ ω) ↔
(rec(𝐺, ∅)‘suc
𝑏) ∈ (rec(𝐺, ∅) “
ω))) |
105 | | rneq 5272 |
. . . . . . . . . . 11
⊢ (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → ran 𝑎 = ran (rec(𝐺, ∅)‘suc 𝑏)) |
106 | 105 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → (𝑏 ∈ ran 𝑎 ↔ 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏))) |
107 | 104, 106 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑎 = (rec(𝐺, ∅)‘suc 𝑏) → ((𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) ↔ ((rec(𝐺, ∅)‘suc 𝑏) ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran (rec(𝐺, ∅)‘suc 𝑏)))) |
108 | 103, 107 | spcev 3273 |
. . . . . . . 8
⊢
(((rec(𝐺,
∅)‘suc 𝑏)
∈ (rec(𝐺, ∅)
“ ω) ∧ 𝑏
∈ ran (rec(𝐺,
∅)‘suc 𝑏))
→ ∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎)) |
109 | 73, 102, 108 | syl2anc 691 |
. . . . . . 7
⊢ (𝑏 ∈ ω →
∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎)) |
110 | 69, 109 | impbii 198 |
. . . . . 6
⊢
(∃𝑎(𝑎 ∈ (rec(𝐺, ∅) “ ω) ∧ 𝑏 ∈ ran 𝑎) ↔ 𝑏 ∈ ω) |
111 | 44, 45, 110 | 3bitri 285 |
. . . . 5
⊢ (𝑏 ∈ ∪ 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎 ↔ 𝑏 ∈ ω) |
112 | 111 | eqriv 2607 |
. . . 4
⊢ ∪ 𝑎 ∈ (rec(𝐺, ∅) “ ω)ran 𝑎 = ω |
113 | 43, 112 | eqtri 2632 |
. . 3
⊢ ran ∪ (rec(𝐺, ∅) “ ω) =
ω |
114 | | dff1o5 6059 |
. . 3
⊢ (∪ (rec(𝐺, ∅) “ ω):∪ (𝑅1 “ ω)–1-1-onto→ω ↔ (∪
(rec(𝐺, ∅) “
ω):∪ (𝑅1 “
ω)–1-1→ω ∧ ran
∪ (rec(𝐺, ∅) “ ω) =
ω)) |
115 | 42, 113, 114 | mpbir2an 957 |
. 2
⊢ ∪ (rec(𝐺, ∅) “ ω):∪ (𝑅1 “ ω)–1-1-onto→ω |
116 | | ackbij.h |
. . 3
⊢ 𝐻 = ∪
(rec(𝐺, ∅) “
ω) |
117 | | f1oeq1 6040 |
. . 3
⊢ (𝐻 = ∪
(rec(𝐺, ∅) “
ω) → (𝐻:∪ (𝑅1 “ ω)–1-1-onto→ω ↔ ∪
(rec(𝐺, ∅) “
ω):∪ (𝑅1 “
ω)–1-1-onto→ω)) |
118 | 116, 117 | ax-mp 5 |
. 2
⊢ (𝐻:∪
(𝑅1 “ ω)–1-1-onto→ω ↔ ∪
(rec(𝐺, ∅) “
ω):∪ (𝑅1 “
ω)–1-1-onto→ω) |
119 | 115, 118 | mpbir 220 |
1
⊢ 𝐻:∪
(𝑅1 “ ω)–1-1-onto→ω |