Step | Hyp | Ref
| Expression |
1 | | suceq 5790 |
. . 3
⊢ (𝑐 = (rank‘𝑎) → suc 𝑐 = suc (rank‘𝑎)) |
2 | 1 | fveq2d 6195 |
. 2
⊢ (𝑐 = (rank‘𝑎) → (𝑧‘suc 𝑐) = (𝑧‘suc (rank‘𝑎))) |
3 | | aomclem4.f |
. 2
⊢ 𝐹 = {〈𝑎, 𝑏〉 ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))} |
4 | | r1fnon 8630 |
. . . . . . . . . . . . . 14
⊢
𝑅1 Fn On |
5 | | fnfun 5988 |
. . . . . . . . . . . . . 14
⊢
(𝑅1 Fn On → Fun
𝑅1) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ Fun
𝑅1 |
7 | | fndm 5990 |
. . . . . . . . . . . . . . 15
⊢
(𝑅1 Fn On → dom 𝑅1 =
On) |
8 | 4, 7 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ dom
𝑅1 = On |
9 | 8 | eqimss2i 3660 |
. . . . . . . . . . . . 13
⊢ On
⊆ dom 𝑅1 |
10 | 6, 9 | pm3.2i 471 |
. . . . . . . . . . . 12
⊢ (Fun
𝑅1 ∧ On ⊆ dom
𝑅1) |
11 | | aomclem4.on |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝑧 ∈ On) |
12 | | funfvima2 6493 |
. . . . . . . . . . . 12
⊢ ((Fun
𝑅1 ∧ On ⊆ dom 𝑅1) → (dom
𝑧 ∈ On →
(𝑅1‘dom 𝑧) ∈ (𝑅1 “
On))) |
13 | 10, 11, 12 | mpsyl 68 |
. . . . . . . . . . 11
⊢ (𝜑 →
(𝑅1‘dom 𝑧) ∈ (𝑅1 “
On)) |
14 | | elssuni 4467 |
. . . . . . . . . . 11
⊢
((𝑅1‘dom 𝑧) ∈ (𝑅1 “ On)
→ (𝑅1‘dom 𝑧) ⊆ ∪
(𝑅1 “ On)) |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(𝑅1‘dom 𝑧) ⊆ ∪
(𝑅1 “ On)) |
16 | 15 | sselda 3603 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ (𝑅1‘dom
𝑧)) → 𝑏 ∈ ∪ (𝑅1 “ On)) |
17 | | rankidb 8663 |
. . . . . . . . 9
⊢ (𝑏 ∈ ∪ (𝑅1 “ On) → 𝑏 ∈
(𝑅1‘suc (rank‘𝑏))) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (𝑅1‘dom
𝑧)) → 𝑏 ∈
(𝑅1‘suc (rank‘𝑏))) |
19 | | suceq 5790 |
. . . . . . . . . 10
⊢
((rank‘𝑏) =
(rank‘𝑎) → suc
(rank‘𝑏) = suc
(rank‘𝑎)) |
20 | 19 | fveq2d 6195 |
. . . . . . . . 9
⊢
((rank‘𝑏) =
(rank‘𝑎) →
(𝑅1‘suc (rank‘𝑏)) = (𝑅1‘suc
(rank‘𝑎))) |
21 | 20 | eleq2d 2687 |
. . . . . . . 8
⊢
((rank‘𝑏) =
(rank‘𝑎) →
(𝑏 ∈
(𝑅1‘suc (rank‘𝑏)) ↔ 𝑏 ∈ (𝑅1‘suc
(rank‘𝑎)))) |
22 | 18, 21 | syl5ibcom 235 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝑅1‘dom
𝑧)) →
((rank‘𝑏) =
(rank‘𝑎) → 𝑏 ∈
(𝑅1‘suc (rank‘𝑎)))) |
23 | 22 | expimpd 629 |
. . . . . 6
⊢ (𝜑 → ((𝑏 ∈ (𝑅1‘dom
𝑧) ∧ (rank‘𝑏) = (rank‘𝑎)) → 𝑏 ∈ (𝑅1‘suc
(rank‘𝑎)))) |
24 | 23 | ss2abdv 3675 |
. . . . 5
⊢ (𝜑 → {𝑏 ∣ (𝑏 ∈ (𝑅1‘dom
𝑧) ∧ (rank‘𝑏) = (rank‘𝑎))} ⊆ {𝑏 ∣ 𝑏 ∈ (𝑅1‘suc
(rank‘𝑎))}) |
25 | | df-rab 2921 |
. . . . 5
⊢ {𝑏 ∈
(𝑅1‘dom 𝑧) ∣ (rank‘𝑏) = (rank‘𝑎)} = {𝑏 ∣ (𝑏 ∈ (𝑅1‘dom
𝑧) ∧ (rank‘𝑏) = (rank‘𝑎))} |
26 | | abid1 2744 |
. . . . 5
⊢
(𝑅1‘suc (rank‘𝑎)) = {𝑏 ∣ 𝑏 ∈ (𝑅1‘suc
(rank‘𝑎))} |
27 | 24, 25, 26 | 3sstr4g 3646 |
. . . 4
⊢ (𝜑 → {𝑏 ∈ (𝑅1‘dom
𝑧) ∣
(rank‘𝑏) =
(rank‘𝑎)} ⊆
(𝑅1‘suc (rank‘𝑎))) |
28 | 27 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑅1‘dom
𝑧)) → {𝑏 ∈
(𝑅1‘dom 𝑧) ∣ (rank‘𝑏) = (rank‘𝑎)} ⊆ (𝑅1‘suc
(rank‘𝑎))) |
29 | | rankr1ai 8661 |
. . . . . 6
⊢ (𝑎 ∈
(𝑅1‘dom 𝑧) → (rank‘𝑎) ∈ dom 𝑧) |
30 | 29 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑅1‘dom
𝑧)) →
(rank‘𝑎) ∈ dom
𝑧) |
31 | | eloni 5733 |
. . . . . . . 8
⊢ (dom
𝑧 ∈ On → Ord dom
𝑧) |
32 | 11, 31 | syl 17 |
. . . . . . 7
⊢ (𝜑 → Ord dom 𝑧) |
33 | | aomclem4.su |
. . . . . . 7
⊢ (𝜑 → dom 𝑧 = ∪ dom 𝑧) |
34 | | limsuc2 37611 |
. . . . . . 7
⊢ ((Ord dom
𝑧 ∧ dom 𝑧 = ∪
dom 𝑧) →
((rank‘𝑎) ∈ dom
𝑧 ↔ suc
(rank‘𝑎) ∈ dom
𝑧)) |
35 | 32, 33, 34 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ((rank‘𝑎) ∈ dom 𝑧 ↔ suc (rank‘𝑎) ∈ dom 𝑧)) |
36 | 35 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑅1‘dom
𝑧)) →
((rank‘𝑎) ∈ dom
𝑧 ↔ suc
(rank‘𝑎) ∈ dom
𝑧)) |
37 | 30, 36 | mpbid 222 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑅1‘dom
𝑧)) → suc
(rank‘𝑎) ∈ dom
𝑧) |
38 | | aomclem4.we |
. . . . . 6
⊢ (𝜑 → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎)) |
39 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → (𝑧‘𝑎) = (𝑧‘𝑏)) |
40 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → (𝑅1‘𝑎) =
(𝑅1‘𝑏)) |
41 | 39, 40 | weeq12d 37610 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → ((𝑧‘𝑎) We (𝑅1‘𝑎) ↔ (𝑧‘𝑏) We (𝑅1‘𝑏))) |
42 | 41 | cbvralv 3171 |
. . . . . 6
⊢
(∀𝑎 ∈
dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎) ↔ ∀𝑏 ∈ dom 𝑧(𝑧‘𝑏) We (𝑅1‘𝑏)) |
43 | 38, 42 | sylib 208 |
. . . . 5
⊢ (𝜑 → ∀𝑏 ∈ dom 𝑧(𝑧‘𝑏) We (𝑅1‘𝑏)) |
44 | 43 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑅1‘dom
𝑧)) → ∀𝑏 ∈ dom 𝑧(𝑧‘𝑏) We (𝑅1‘𝑏)) |
45 | | fveq2 6191 |
. . . . . 6
⊢ (𝑏 = suc (rank‘𝑎) → (𝑧‘𝑏) = (𝑧‘suc (rank‘𝑎))) |
46 | | fveq2 6191 |
. . . . . 6
⊢ (𝑏 = suc (rank‘𝑎) →
(𝑅1‘𝑏) = (𝑅1‘suc
(rank‘𝑎))) |
47 | 45, 46 | weeq12d 37610 |
. . . . 5
⊢ (𝑏 = suc (rank‘𝑎) → ((𝑧‘𝑏) We (𝑅1‘𝑏) ↔ (𝑧‘suc (rank‘𝑎)) We (𝑅1‘suc
(rank‘𝑎)))) |
48 | 47 | rspcva 3307 |
. . . 4
⊢ ((suc
(rank‘𝑎) ∈ dom
𝑧 ∧ ∀𝑏 ∈ dom 𝑧(𝑧‘𝑏) We (𝑅1‘𝑏)) → (𝑧‘suc (rank‘𝑎)) We (𝑅1‘suc
(rank‘𝑎))) |
49 | 37, 44, 48 | syl2anc 693 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑅1‘dom
𝑧)) → (𝑧‘suc (rank‘𝑎)) We
(𝑅1‘suc (rank‘𝑎))) |
50 | | wess 5101 |
. . 3
⊢ ({𝑏 ∈
(𝑅1‘dom 𝑧) ∣ (rank‘𝑏) = (rank‘𝑎)} ⊆ (𝑅1‘suc
(rank‘𝑎)) →
((𝑧‘suc
(rank‘𝑎)) We
(𝑅1‘suc (rank‘𝑎)) → (𝑧‘suc (rank‘𝑎)) We {𝑏 ∈ (𝑅1‘dom
𝑧) ∣
(rank‘𝑏) =
(rank‘𝑎)})) |
51 | 28, 49, 50 | sylc 65 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑅1‘dom
𝑧)) → (𝑧‘suc (rank‘𝑎)) We {𝑏 ∈ (𝑅1‘dom
𝑧) ∣
(rank‘𝑏) =
(rank‘𝑎)}) |
52 | | rankf 8657 |
. . . 4
⊢
rank:∪ (𝑅1 “
On)⟶On |
53 | 52 | a1i 11 |
. . 3
⊢ (𝜑 → rank:∪ (𝑅1 “
On)⟶On) |
54 | 53, 15 | fssresd 6071 |
. 2
⊢ (𝜑 → (rank ↾
(𝑅1‘dom 𝑧)):(𝑅1‘dom 𝑧)⟶On) |
55 | | epweon 6983 |
. . 3
⊢ E We
On |
56 | 55 | a1i 11 |
. 2
⊢ (𝜑 → E We On) |
57 | 2, 3, 51, 54, 56 | fnwe2 37623 |
1
⊢ (𝜑 → 𝐹 We (𝑅1‘dom 𝑧)) |