Step | Hyp | Ref
| Expression |
1 | | suceq 6247 |
. . 3
⊢ (𝑐 = (rank‘𝑎) → suc 𝑐 = suc (rank‘𝑎)) |
2 | 1 | fveq2d 6690 |
. 2
⊢ (𝑐 = (rank‘𝑎) → (𝑧‘suc 𝑐) = (𝑧‘suc (rank‘𝑎))) |
3 | | aomclem4.f |
. 2
⊢ 𝐹 = {〈𝑎, 𝑏〉 ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))} |
4 | | r1fnon 9281 |
. . . . . . . . . . . . . 14
⊢
𝑅1 Fn On |
5 | | fnfun 6448 |
. . . . . . . . . . . . . 14
⊢
(𝑅1 Fn On → Fun
𝑅1) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ Fun
𝑅1 |
7 | 4 | fndmi 6451 |
. . . . . . . . . . . . . 14
⊢ dom
𝑅1 = On |
8 | 7 | eqimss2i 3946 |
. . . . . . . . . . . . 13
⊢ On
⊆ dom 𝑅1 |
9 | 6, 8 | pm3.2i 474 |
. . . . . . . . . . . 12
⊢ (Fun
𝑅1 ∧ On ⊆ dom
𝑅1) |
10 | | aomclem4.on |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝑧 ∈ On) |
11 | | funfvima2 7016 |
. . . . . . . . . . . 12
⊢ ((Fun
𝑅1 ∧ On ⊆ dom 𝑅1) → (dom
𝑧 ∈ On →
(𝑅1‘dom 𝑧) ∈ (𝑅1 “
On))) |
12 | 9, 10, 11 | mpsyl 68 |
. . . . . . . . . . 11
⊢ (𝜑 →
(𝑅1‘dom 𝑧) ∈ (𝑅1 “
On)) |
13 | | elssuni 4838 |
. . . . . . . . . . 11
⊢
((𝑅1‘dom 𝑧) ∈ (𝑅1 “ On)
→ (𝑅1‘dom 𝑧) ⊆ ∪
(𝑅1 “ On)) |
14 | 12, 13 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(𝑅1‘dom 𝑧) ⊆ ∪
(𝑅1 “ On)) |
15 | 14 | sselda 3887 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ (𝑅1‘dom
𝑧)) → 𝑏 ∈ ∪ (𝑅1 “ On)) |
16 | | rankidb 9314 |
. . . . . . . . 9
⊢ (𝑏 ∈ ∪ (𝑅1 “ On) → 𝑏 ∈
(𝑅1‘suc (rank‘𝑏))) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (𝑅1‘dom
𝑧)) → 𝑏 ∈
(𝑅1‘suc (rank‘𝑏))) |
18 | | suceq 6247 |
. . . . . . . . . 10
⊢
((rank‘𝑏) =
(rank‘𝑎) → suc
(rank‘𝑏) = suc
(rank‘𝑎)) |
19 | 18 | fveq2d 6690 |
. . . . . . . . 9
⊢
((rank‘𝑏) =
(rank‘𝑎) →
(𝑅1‘suc (rank‘𝑏)) = (𝑅1‘suc
(rank‘𝑎))) |
20 | 19 | eleq2d 2819 |
. . . . . . . 8
⊢
((rank‘𝑏) =
(rank‘𝑎) →
(𝑏 ∈
(𝑅1‘suc (rank‘𝑏)) ↔ 𝑏 ∈ (𝑅1‘suc
(rank‘𝑎)))) |
21 | 17, 20 | syl5ibcom 248 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝑅1‘dom
𝑧)) →
((rank‘𝑏) =
(rank‘𝑎) → 𝑏 ∈
(𝑅1‘suc (rank‘𝑎)))) |
22 | 21 | expimpd 457 |
. . . . . 6
⊢ (𝜑 → ((𝑏 ∈ (𝑅1‘dom
𝑧) ∧ (rank‘𝑏) = (rank‘𝑎)) → 𝑏 ∈ (𝑅1‘suc
(rank‘𝑎)))) |
23 | 22 | ss2abdv 3963 |
. . . . 5
⊢ (𝜑 → {𝑏 ∣ (𝑏 ∈ (𝑅1‘dom
𝑧) ∧ (rank‘𝑏) = (rank‘𝑎))} ⊆ {𝑏 ∣ 𝑏 ∈ (𝑅1‘suc
(rank‘𝑎))}) |
24 | | df-rab 3063 |
. . . . 5
⊢ {𝑏 ∈
(𝑅1‘dom 𝑧) ∣ (rank‘𝑏) = (rank‘𝑎)} = {𝑏 ∣ (𝑏 ∈ (𝑅1‘dom
𝑧) ∧ (rank‘𝑏) = (rank‘𝑎))} |
25 | | abid1 2874 |
. . . . 5
⊢
(𝑅1‘suc (rank‘𝑎)) = {𝑏 ∣ 𝑏 ∈ (𝑅1‘suc
(rank‘𝑎))} |
26 | 23, 24, 25 | 3sstr4g 3932 |
. . . 4
⊢ (𝜑 → {𝑏 ∈ (𝑅1‘dom
𝑧) ∣
(rank‘𝑏) =
(rank‘𝑎)} ⊆
(𝑅1‘suc (rank‘𝑎))) |
27 | 26 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑅1‘dom
𝑧)) → {𝑏 ∈
(𝑅1‘dom 𝑧) ∣ (rank‘𝑏) = (rank‘𝑎)} ⊆ (𝑅1‘suc
(rank‘𝑎))) |
28 | | fveq2 6686 |
. . . . 5
⊢ (𝑏 = suc (rank‘𝑎) → (𝑧‘𝑏) = (𝑧‘suc (rank‘𝑎))) |
29 | | fveq2 6686 |
. . . . 5
⊢ (𝑏 = suc (rank‘𝑎) →
(𝑅1‘𝑏) = (𝑅1‘suc
(rank‘𝑎))) |
30 | 28, 29 | weeq12d 40477 |
. . . 4
⊢ (𝑏 = suc (rank‘𝑎) → ((𝑧‘𝑏) We (𝑅1‘𝑏) ↔ (𝑧‘suc (rank‘𝑎)) We (𝑅1‘suc
(rank‘𝑎)))) |
31 | | aomclem4.we |
. . . . . 6
⊢ (𝜑 → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎)) |
32 | | fveq2 6686 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → (𝑧‘𝑎) = (𝑧‘𝑏)) |
33 | | fveq2 6686 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → (𝑅1‘𝑎) =
(𝑅1‘𝑏)) |
34 | 32, 33 | weeq12d 40477 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → ((𝑧‘𝑎) We (𝑅1‘𝑎) ↔ (𝑧‘𝑏) We (𝑅1‘𝑏))) |
35 | 34 | cbvralvw 3350 |
. . . . . 6
⊢
(∀𝑎 ∈
dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎) ↔ ∀𝑏 ∈ dom 𝑧(𝑧‘𝑏) We (𝑅1‘𝑏)) |
36 | 31, 35 | sylib 221 |
. . . . 5
⊢ (𝜑 → ∀𝑏 ∈ dom 𝑧(𝑧‘𝑏) We (𝑅1‘𝑏)) |
37 | 36 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑅1‘dom
𝑧)) → ∀𝑏 ∈ dom 𝑧(𝑧‘𝑏) We (𝑅1‘𝑏)) |
38 | | rankr1ai 9312 |
. . . . . 6
⊢ (𝑎 ∈
(𝑅1‘dom 𝑧) → (rank‘𝑎) ∈ dom 𝑧) |
39 | 38 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑅1‘dom
𝑧)) →
(rank‘𝑎) ∈ dom
𝑧) |
40 | | eloni 6192 |
. . . . . . . 8
⊢ (dom
𝑧 ∈ On → Ord dom
𝑧) |
41 | 10, 40 | syl 17 |
. . . . . . 7
⊢ (𝜑 → Ord dom 𝑧) |
42 | | aomclem4.su |
. . . . . . 7
⊢ (𝜑 → dom 𝑧 = ∪ dom 𝑧) |
43 | | limsuc2 40478 |
. . . . . . 7
⊢ ((Ord dom
𝑧 ∧ dom 𝑧 = ∪
dom 𝑧) →
((rank‘𝑎) ∈ dom
𝑧 ↔ suc
(rank‘𝑎) ∈ dom
𝑧)) |
44 | 41, 42, 43 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ((rank‘𝑎) ∈ dom 𝑧 ↔ suc (rank‘𝑎) ∈ dom 𝑧)) |
45 | 44 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑅1‘dom
𝑧)) →
((rank‘𝑎) ∈ dom
𝑧 ↔ suc
(rank‘𝑎) ∈ dom
𝑧)) |
46 | 39, 45 | mpbid 235 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑅1‘dom
𝑧)) → suc
(rank‘𝑎) ∈ dom
𝑧) |
47 | 30, 37, 46 | rspcdva 3531 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑅1‘dom
𝑧)) → (𝑧‘suc (rank‘𝑎)) We
(𝑅1‘suc (rank‘𝑎))) |
48 | | wess 5522 |
. . 3
⊢ ({𝑏 ∈
(𝑅1‘dom 𝑧) ∣ (rank‘𝑏) = (rank‘𝑎)} ⊆ (𝑅1‘suc
(rank‘𝑎)) →
((𝑧‘suc
(rank‘𝑎)) We
(𝑅1‘suc (rank‘𝑎)) → (𝑧‘suc (rank‘𝑎)) We {𝑏 ∈ (𝑅1‘dom
𝑧) ∣
(rank‘𝑏) =
(rank‘𝑎)})) |
49 | 27, 47, 48 | sylc 65 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑅1‘dom
𝑧)) → (𝑧‘suc (rank‘𝑎)) We {𝑏 ∈ (𝑅1‘dom
𝑧) ∣
(rank‘𝑏) =
(rank‘𝑎)}) |
50 | | rankf 9308 |
. . . 4
⊢
rank:∪ (𝑅1 “
On)⟶On |
51 | 50 | a1i 11 |
. . 3
⊢ (𝜑 → rank:∪ (𝑅1 “
On)⟶On) |
52 | 51, 14 | fssresd 6555 |
. 2
⊢ (𝜑 → (rank ↾
(𝑅1‘dom 𝑧)):(𝑅1‘dom 𝑧)⟶On) |
53 | | epweon 7528 |
. . 3
⊢ E We
On |
54 | 53 | a1i 11 |
. 2
⊢ (𝜑 → E We On) |
55 | 2, 3, 49, 52, 54 | fnwe2 40490 |
1
⊢ (𝜑 → 𝐹 We (𝑅1‘dom 𝑧)) |