| Step | Hyp | Ref
| Expression |
| 1 | | elfvdm 6943 |
. . 3
⊢ (𝐴 ∈
(𝑅1‘𝐵) → 𝐵 ∈ dom
𝑅1) |
| 2 | | r1val1 9826 |
. . . . . 6
⊢ (𝐵 ∈ dom
𝑅1 → (𝑅1‘𝐵) = ∪
𝑥 ∈ 𝐵 𝒫
(𝑅1‘𝑥)) |
| 3 | 2 | eleq2d 2827 |
. . . . 5
⊢ (𝐵 ∈ dom
𝑅1 → (𝐴 ∈ (𝑅1‘𝐵) ↔ 𝐴 ∈ ∪
𝑥 ∈ 𝐵 𝒫
(𝑅1‘𝑥))) |
| 4 | | eliun 4995 |
. . . . 5
⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝒫
(𝑅1‘𝑥) ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝒫
(𝑅1‘𝑥)) |
| 5 | 3, 4 | bitrdi 287 |
. . . 4
⊢ (𝐵 ∈ dom
𝑅1 → (𝐴 ∈ (𝑅1‘𝐵) ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝒫
(𝑅1‘𝑥))) |
| 6 | | r1funlim 9806 |
. . . . . . . . . . 11
⊢ (Fun
𝑅1 ∧ Lim dom 𝑅1) |
| 7 | 6 | simpri 485 |
. . . . . . . . . 10
⊢ Lim dom
𝑅1 |
| 8 | | limord 6444 |
. . . . . . . . . 10
⊢ (Lim dom
𝑅1 → Ord dom 𝑅1) |
| 9 | 7, 8 | ax-mp 5 |
. . . . . . . . 9
⊢ Ord dom
𝑅1 |
| 10 | | ordtr1 6427 |
. . . . . . . . 9
⊢ (Ord dom
𝑅1 → ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ dom 𝑅1) →
𝑥 ∈ dom
𝑅1)) |
| 11 | 9, 10 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ dom 𝑅1) →
𝑥 ∈ dom
𝑅1) |
| 12 | 11 | ancoms 458 |
. . . . . . 7
⊢ ((𝐵 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ dom
𝑅1) |
| 13 | | r1sucg 9809 |
. . . . . . . 8
⊢ (𝑥 ∈ dom
𝑅1 → (𝑅1‘suc 𝑥) = 𝒫
(𝑅1‘𝑥)) |
| 14 | 13 | eleq2d 2827 |
. . . . . . 7
⊢ (𝑥 ∈ dom
𝑅1 → (𝐴 ∈ (𝑅1‘suc
𝑥) ↔ 𝐴 ∈ 𝒫
(𝑅1‘𝑥))) |
| 15 | 12, 14 | syl 17 |
. . . . . 6
⊢ ((𝐵 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐵) → (𝐴 ∈ (𝑅1‘suc
𝑥) ↔ 𝐴 ∈ 𝒫
(𝑅1‘𝑥))) |
| 16 | | ordsson 7803 |
. . . . . . . . . 10
⊢ (Ord dom
𝑅1 → dom 𝑅1 ⊆
On) |
| 17 | 9, 16 | ax-mp 5 |
. . . . . . . . 9
⊢ dom
𝑅1 ⊆ On |
| 18 | 17, 12 | sselid 3981 |
. . . . . . . 8
⊢ ((𝐵 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
| 19 | | rabid 3458 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc
𝑥)} ↔ (𝑥 ∈ On ∧ 𝐴 ∈
(𝑅1‘suc 𝑥))) |
| 20 | | intss1 4963 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc
𝑥)} → ∩ {𝑥
∈ On ∣ 𝐴 ∈
(𝑅1‘suc 𝑥)} ⊆ 𝑥) |
| 21 | 19, 20 | sylbir 235 |
. . . . . . . 8
⊢ ((𝑥 ∈ On ∧ 𝐴 ∈
(𝑅1‘suc 𝑥)) → ∩ {𝑥 ∈ On ∣ 𝐴 ∈
(𝑅1‘suc 𝑥)} ⊆ 𝑥) |
| 22 | 18, 21 | sylan 580 |
. . . . . . 7
⊢ (((𝐵 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐵) ∧ 𝐴 ∈ (𝑅1‘suc
𝑥)) → ∩ {𝑥
∈ On ∣ 𝐴 ∈
(𝑅1‘suc 𝑥)} ⊆ 𝑥) |
| 23 | 22 | ex 412 |
. . . . . 6
⊢ ((𝐵 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐵) → (𝐴 ∈ (𝑅1‘suc
𝑥) → ∩ {𝑥
∈ On ∣ 𝐴 ∈
(𝑅1‘suc 𝑥)} ⊆ 𝑥)) |
| 24 | 15, 23 | sylbird 260 |
. . . . 5
⊢ ((𝐵 ∈ dom
𝑅1 ∧ 𝑥 ∈ 𝐵) → (𝐴 ∈ 𝒫
(𝑅1‘𝑥) → ∩ {𝑥 ∈ On ∣ 𝐴 ∈
(𝑅1‘suc 𝑥)} ⊆ 𝑥)) |
| 25 | 24 | reximdva 3168 |
. . . 4
⊢ (𝐵 ∈ dom
𝑅1 → (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝒫
(𝑅1‘𝑥) → ∃𝑥 ∈ 𝐵 ∩ {𝑥 ∈ On ∣ 𝐴 ∈
(𝑅1‘suc 𝑥)} ⊆ 𝑥)) |
| 26 | 5, 25 | sylbid 240 |
. . 3
⊢ (𝐵 ∈ dom
𝑅1 → (𝐴 ∈ (𝑅1‘𝐵) → ∃𝑥 ∈ 𝐵 ∩ {𝑥 ∈ On ∣ 𝐴 ∈
(𝑅1‘suc 𝑥)} ⊆ 𝑥)) |
| 27 | 1, 26 | mpcom 38 |
. 2
⊢ (𝐴 ∈
(𝑅1‘𝐵) → ∃𝑥 ∈ 𝐵 ∩ {𝑥 ∈ On ∣ 𝐴 ∈
(𝑅1‘suc 𝑥)} ⊆ 𝑥) |
| 28 | | r1elwf 9836 |
. . . . . . 7
⊢ (𝐴 ∈
(𝑅1‘𝐵) → 𝐴 ∈ ∪
(𝑅1 “ On)) |
| 29 | | rankvalb 9837 |
. . . . . . 7
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝐴) = ∩ {𝑥
∈ On ∣ 𝐴 ∈
(𝑅1‘suc 𝑥)}) |
| 30 | 28, 29 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ∈
(𝑅1‘suc 𝑥)}) |
| 31 | 30 | sseq1d 4015 |
. . . . 5
⊢ (𝐴 ∈
(𝑅1‘𝐵) → ((rank‘𝐴) ⊆ 𝑥 ↔ ∩ {𝑥 ∈ On ∣ 𝐴 ∈
(𝑅1‘suc 𝑥)} ⊆ 𝑥)) |
| 32 | 31 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝑥 ∈ 𝐵) → ((rank‘𝐴) ⊆ 𝑥 ↔ ∩ {𝑥 ∈ On ∣ 𝐴 ∈
(𝑅1‘suc 𝑥)} ⊆ 𝑥)) |
| 33 | | rankon 9835 |
. . . . . . 7
⊢
(rank‘𝐴)
∈ On |
| 34 | 17, 1 | sselid 3981 |
. . . . . . 7
⊢ (𝐴 ∈
(𝑅1‘𝐵) → 𝐵 ∈ On) |
| 35 | | ontr2 6431 |
. . . . . . 7
⊢
(((rank‘𝐴)
∈ On ∧ 𝐵 ∈
On) → (((rank‘𝐴)
⊆ 𝑥 ∧ 𝑥 ∈ 𝐵) → (rank‘𝐴) ∈ 𝐵)) |
| 36 | 33, 34, 35 | sylancr 587 |
. . . . . 6
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (((rank‘𝐴) ⊆ 𝑥 ∧ 𝑥 ∈ 𝐵) → (rank‘𝐴) ∈ 𝐵)) |
| 37 | 36 | expcomd 416 |
. . . . 5
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (𝑥 ∈ 𝐵 → ((rank‘𝐴) ⊆ 𝑥 → (rank‘𝐴) ∈ 𝐵))) |
| 38 | 37 | imp 406 |
. . . 4
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝑥 ∈ 𝐵) → ((rank‘𝐴) ⊆ 𝑥 → (rank‘𝐴) ∈ 𝐵)) |
| 39 | 32, 38 | sylbird 260 |
. . 3
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝑥 ∈ 𝐵) → (∩
{𝑥 ∈ On ∣ 𝐴 ∈
(𝑅1‘suc 𝑥)} ⊆ 𝑥 → (rank‘𝐴) ∈ 𝐵)) |
| 40 | 39 | rexlimdva 3155 |
. 2
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (∃𝑥 ∈ 𝐵 ∩ {𝑥 ∈ On ∣ 𝐴 ∈
(𝑅1‘suc 𝑥)} ⊆ 𝑥 → (rank‘𝐴) ∈ 𝐵)) |
| 41 | 27, 40 | mpd 15 |
1
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (rank‘𝐴) ∈ 𝐵) |