| Step | Hyp | Ref
| Expression |
| 1 | | df-rank 9805 |
. . . 4
⊢ rank =
(𝑥 ∈ V ↦ ∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)}) |
| 2 | 1 | funmpt2 6605 |
. . 3
⊢ Fun
rank |
| 3 | | mptv 5258 |
. . . . . 6
⊢ (𝑥 ∈ V ↦ ∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)}) = {〈𝑥, 𝑧〉 ∣ 𝑧 = ∩ {𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)}} |
| 4 | 1, 3 | eqtri 2765 |
. . . . 5
⊢ rank =
{〈𝑥, 𝑧〉 ∣ 𝑧 = ∩
{𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)}} |
| 5 | 4 | dmeqi 5915 |
. . . 4
⊢ dom rank
= dom {〈𝑥, 𝑧〉 ∣ 𝑧 = ∩
{𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)}} |
| 6 | | dmopab 5926 |
. . . . 5
⊢ dom
{〈𝑥, 𝑧〉 ∣ 𝑧 = ∩
{𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)}} = {𝑥 ∣ ∃𝑧 𝑧 = ∩ {𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)}} |
| 7 | | eqabcb 2883 |
. . . . . 6
⊢ ({𝑥 ∣ ∃𝑧 𝑧 = ∩ {𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)}} = ∪
(𝑅1 “ On) ↔ ∀𝑥(∃𝑧 𝑧 = ∩ {𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ↔ 𝑥 ∈ ∪
(𝑅1 “ On))) |
| 8 | | rankwflemb 9833 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑦 ∈ On 𝑥 ∈ (𝑅1‘suc
𝑦)) |
| 9 | | intexrab 5347 |
. . . . . . 7
⊢
(∃𝑦 ∈ On
𝑥 ∈
(𝑅1‘suc 𝑦) ↔ ∩ {𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ∈ V) |
| 10 | | isset 3494 |
. . . . . . 7
⊢ (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ∈ V ↔ ∃𝑧 𝑧 = ∩ {𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)}) |
| 11 | 8, 9, 10 | 3bitrri 298 |
. . . . . 6
⊢
(∃𝑧 𝑧 = ∩
{𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ↔ 𝑥 ∈ ∪
(𝑅1 “ On)) |
| 12 | 7, 11 | mpgbir 1799 |
. . . . 5
⊢ {𝑥 ∣ ∃𝑧 𝑧 = ∩ {𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)}} = ∪
(𝑅1 “ On) |
| 13 | 6, 12 | eqtri 2765 |
. . . 4
⊢ dom
{〈𝑥, 𝑧〉 ∣ 𝑧 = ∩
{𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)}} = ∪
(𝑅1 “ On) |
| 14 | 5, 13 | eqtri 2765 |
. . 3
⊢ dom rank
= ∪ (𝑅1 “
On) |
| 15 | | df-fn 6564 |
. . 3
⊢ (rank Fn
∪ (𝑅1 “ On) ↔ (Fun
rank ∧ dom rank = ∪ (𝑅1
“ On))) |
| 16 | 2, 14, 15 | mpbir2an 711 |
. 2
⊢ rank Fn
∪ (𝑅1 “
On) |
| 17 | | rabn0 4389 |
. . . . 5
⊢ ({𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ≠ ∅ ↔ ∃𝑦 ∈ On 𝑥 ∈ (𝑅1‘suc
𝑦)) |
| 18 | 8, 17 | bitr4i 278 |
. . . 4
⊢ (𝑥 ∈ ∪ (𝑅1 “ On) ↔ {𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ≠ ∅) |
| 19 | | intex 5344 |
. . . . . 6
⊢ ({𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ≠ ∅ ↔ ∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ∈ V) |
| 20 | | vex 3484 |
. . . . . . 7
⊢ 𝑥 ∈ V |
| 21 | 1 | fvmpt2 7027 |
. . . . . . 7
⊢ ((𝑥 ∈ V ∧ ∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ∈ V) → (rank‘𝑥) = ∩
{𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)}) |
| 22 | 20, 21 | mpan 690 |
. . . . . 6
⊢ (∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ∈ V → (rank‘𝑥) = ∩
{𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)}) |
| 23 | 19, 22 | sylbi 217 |
. . . . 5
⊢ ({𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ≠ ∅ → (rank‘𝑥) = ∩
{𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)}) |
| 24 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ⊆ On |
| 25 | | oninton 7815 |
. . . . . 6
⊢ (({𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ⊆ On ∧ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)} ≠ ∅) →
∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc
𝑦)} ∈
On) |
| 26 | 24, 25 | mpan 690 |
. . . . 5
⊢ ({𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ≠ ∅ → ∩ {𝑦
∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ∈ On) |
| 27 | 23, 26 | eqeltrd 2841 |
. . . 4
⊢ ({𝑦 ∈ On ∣ 𝑥 ∈
(𝑅1‘suc 𝑦)} ≠ ∅ → (rank‘𝑥) ∈ On) |
| 28 | 18, 27 | sylbi 217 |
. . 3
⊢ (𝑥 ∈ ∪ (𝑅1 “ On) →
(rank‘𝑥) ∈
On) |
| 29 | 28 | rgen 3063 |
. 2
⊢
∀𝑥 ∈
∪ (𝑅1 “
On)(rank‘𝑥) ∈
On |
| 30 | | ffnfv 7139 |
. 2
⊢
(rank:∪ (𝑅1 “
On)⟶On ↔ (rank Fn ∪
(𝑅1 “ On) ∧ ∀𝑥 ∈ ∪
(𝑅1 “ On)(rank‘𝑥) ∈ On)) |
| 31 | 16, 29, 30 | mpbir2an 711 |
1
⊢
rank:∪ (𝑅1 “
On)⟶On |