Proof of Theorem r1pwcl
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | r1elwf 9837 | . . . 4
⊢ (𝐴 ∈
(𝑅1‘𝐵) → 𝐴 ∈ ∪
(𝑅1 “ On)) | 
| 2 |  | elfvdm 6942 | . . . 4
⊢ (𝐴 ∈
(𝑅1‘𝐵) → 𝐵 ∈ dom
𝑅1) | 
| 3 | 1, 2 | jca 511 | . . 3
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (𝐴 ∈ ∪
(𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1)) | 
| 4 | 3 | a1i 11 | . 2
⊢ (Lim
𝐵 → (𝐴 ∈ (𝑅1‘𝐵) → (𝐴 ∈ ∪
(𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1))) | 
| 5 |  | r1elwf 9837 | . . . . 5
⊢
(𝒫 𝐴 ∈
(𝑅1‘𝐵) → 𝒫 𝐴 ∈ ∪
(𝑅1 “ On)) | 
| 6 |  | pwwf 9848 | . . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ 𝒫
𝐴 ∈ ∪ (𝑅1 “ On)) | 
| 7 | 5, 6 | sylibr 234 | . . . 4
⊢
(𝒫 𝐴 ∈
(𝑅1‘𝐵) → 𝐴 ∈ ∪
(𝑅1 “ On)) | 
| 8 |  | elfvdm 6942 | . . . 4
⊢
(𝒫 𝐴 ∈
(𝑅1‘𝐵) → 𝐵 ∈ dom
𝑅1) | 
| 9 | 7, 8 | jca 511 | . . 3
⊢
(𝒫 𝐴 ∈
(𝑅1‘𝐵) → (𝐴 ∈ ∪
(𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1)) | 
| 10 | 9 | a1i 11 | . 2
⊢ (Lim
𝐵 → (𝒫 𝐴 ∈
(𝑅1‘𝐵) → (𝐴 ∈ ∪
(𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1))) | 
| 11 |  | limsuc 7871 | . . . . . 6
⊢ (Lim
𝐵 → ((rank‘𝐴) ∈ 𝐵 ↔ suc (rank‘𝐴) ∈ 𝐵)) | 
| 12 | 11 | adantr 480 | . . . . 5
⊢ ((Lim
𝐵 ∧ (𝐴 ∈ ∪
(𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1)) →
((rank‘𝐴) ∈
𝐵 ↔ suc
(rank‘𝐴) ∈ 𝐵)) | 
| 13 |  | rankpwi 9864 | . . . . . . 7
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝒫 𝐴) =
suc (rank‘𝐴)) | 
| 14 | 13 | ad2antrl 728 | . . . . . 6
⊢ ((Lim
𝐵 ∧ (𝐴 ∈ ∪
(𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1)) →
(rank‘𝒫 𝐴) =
suc (rank‘𝐴)) | 
| 15 | 14 | eleq1d 2825 | . . . . 5
⊢ ((Lim
𝐵 ∧ (𝐴 ∈ ∪
(𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1)) →
((rank‘𝒫 𝐴)
∈ 𝐵 ↔ suc
(rank‘𝐴) ∈ 𝐵)) | 
| 16 | 12, 15 | bitr4d 282 | . . . 4
⊢ ((Lim
𝐵 ∧ (𝐴 ∈ ∪
(𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1)) →
((rank‘𝐴) ∈
𝐵 ↔
(rank‘𝒫 𝐴)
∈ 𝐵)) | 
| 17 |  | rankr1ag 9843 | . . . . 5
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → (𝐴 ∈ (𝑅1‘𝐵) ↔ (rank‘𝐴) ∈ 𝐵)) | 
| 18 | 17 | adantl 481 | . . . 4
⊢ ((Lim
𝐵 ∧ (𝐴 ∈ ∪
(𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1)) →
(𝐴 ∈
(𝑅1‘𝐵) ↔ (rank‘𝐴) ∈ 𝐵)) | 
| 19 |  | rankr1ag 9843 | . . . . . 6
⊢
((𝒫 𝐴 ∈
∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → (𝒫 𝐴 ∈ (𝑅1‘𝐵) ↔ (rank‘𝒫
𝐴) ∈ 𝐵)) | 
| 20 | 6, 19 | sylanb 581 | . . . . 5
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → (𝒫 𝐴 ∈ (𝑅1‘𝐵) ↔ (rank‘𝒫
𝐴) ∈ 𝐵)) | 
| 21 | 20 | adantl 481 | . . . 4
⊢ ((Lim
𝐵 ∧ (𝐴 ∈ ∪
(𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1)) →
(𝒫 𝐴 ∈
(𝑅1‘𝐵) ↔ (rank‘𝒫 𝐴) ∈ 𝐵)) | 
| 22 | 16, 18, 21 | 3bitr4d 311 | . . 3
⊢ ((Lim
𝐵 ∧ (𝐴 ∈ ∪
(𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1)) →
(𝐴 ∈
(𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈ (𝑅1‘𝐵))) | 
| 23 | 22 | ex 412 | . 2
⊢ (Lim
𝐵 → ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → (𝐴 ∈ (𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈
(𝑅1‘𝐵)))) | 
| 24 | 4, 10, 23 | pm5.21ndd 379 | 1
⊢ (Lim
𝐵 → (𝐴 ∈ (𝑅1‘𝐵) ↔ 𝒫 𝐴 ∈
(𝑅1‘𝐵))) |