Proof of Theorem rankr1c
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | id 22 | . . . 4
⊢ (𝐵 = (rank‘𝐴) → 𝐵 = (rank‘𝐴)) | 
| 2 |  | rankdmr1 9842 | . . . 4
⊢
(rank‘𝐴)
∈ dom 𝑅1 | 
| 3 | 1, 2 | eqeltrdi 2848 | . . 3
⊢ (𝐵 = (rank‘𝐴) → 𝐵 ∈ dom
𝑅1) | 
| 4 | 3 | a1i 11 | . 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝐵 = (rank‘𝐴) → 𝐵 ∈ dom
𝑅1)) | 
| 5 |  | elfvdm 6942 | . . . . 5
⊢ (𝐴 ∈
(𝑅1‘suc 𝐵) → suc 𝐵 ∈ dom
𝑅1) | 
| 6 |  | r1funlim 9807 | . . . . . . 7
⊢ (Fun
𝑅1 ∧ Lim dom 𝑅1) | 
| 7 | 6 | simpri 485 | . . . . . 6
⊢ Lim dom
𝑅1 | 
| 8 |  | limsuc 7871 | . . . . . 6
⊢ (Lim dom
𝑅1 → (𝐵 ∈ dom 𝑅1 ↔ suc
𝐵 ∈ dom
𝑅1)) | 
| 9 | 7, 8 | ax-mp 5 | . . . . 5
⊢ (𝐵 ∈ dom
𝑅1 ↔ suc 𝐵 ∈ dom
𝑅1) | 
| 10 | 5, 9 | sylibr 234 | . . . 4
⊢ (𝐴 ∈
(𝑅1‘suc 𝐵) → 𝐵 ∈ dom
𝑅1) | 
| 11 | 10 | adantl 481 | . . 3
⊢ ((¬
𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc
𝐵)) → 𝐵 ∈ dom
𝑅1) | 
| 12 | 11 | a1i 11 | . 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ((¬ 𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc
𝐵)) → 𝐵 ∈ dom
𝑅1)) | 
| 13 |  | eqss 3998 | . . . 4
⊢ (𝐵 = (rank‘𝐴) ↔ (𝐵 ⊆ (rank‘𝐴) ∧ (rank‘𝐴) ⊆ 𝐵)) | 
| 14 |  | rankr1clem 9861 | . . . . 5
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → (¬ 𝐴 ∈ (𝑅1‘𝐵) ↔ 𝐵 ⊆ (rank‘𝐴))) | 
| 15 |  | rankr1ag 9843 | . . . . . . 7
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ suc 𝐵 ∈ dom
𝑅1) → (𝐴 ∈ (𝑅1‘suc
𝐵) ↔ (rank‘𝐴) ∈ suc 𝐵)) | 
| 16 | 9, 15 | sylan2b 594 | . . . . . 6
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → (𝐴 ∈ (𝑅1‘suc
𝐵) ↔ (rank‘𝐴) ∈ suc 𝐵)) | 
| 17 |  | rankon 9836 | . . . . . . 7
⊢
(rank‘𝐴)
∈ On | 
| 18 |  | limord 6443 | . . . . . . . . . 10
⊢ (Lim dom
𝑅1 → Ord dom 𝑅1) | 
| 19 | 7, 18 | ax-mp 5 | . . . . . . . . 9
⊢ Ord dom
𝑅1 | 
| 20 |  | ordelon 6407 | . . . . . . . . 9
⊢ ((Ord dom
𝑅1 ∧ 𝐵 ∈ dom 𝑅1) →
𝐵 ∈
On) | 
| 21 | 19, 20 | mpan 690 | . . . . . . . 8
⊢ (𝐵 ∈ dom
𝑅1 → 𝐵 ∈ On) | 
| 22 | 21 | adantl 481 | . . . . . . 7
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → 𝐵 ∈ On) | 
| 23 |  | onsssuc 6473 | . . . . . . 7
⊢
(((rank‘𝐴)
∈ On ∧ 𝐵 ∈
On) → ((rank‘𝐴)
⊆ 𝐵 ↔
(rank‘𝐴) ∈ suc
𝐵)) | 
| 24 | 17, 22, 23 | sylancr 587 | . . . . . 6
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → ((rank‘𝐴) ⊆ 𝐵 ↔ (rank‘𝐴) ∈ suc 𝐵)) | 
| 25 | 16, 24 | bitr4d 282 | . . . . 5
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → (𝐴 ∈ (𝑅1‘suc
𝐵) ↔ (rank‘𝐴) ⊆ 𝐵)) | 
| 26 | 14, 25 | anbi12d 632 | . . . 4
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → ((¬ 𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc
𝐵)) ↔ (𝐵 ⊆ (rank‘𝐴) ∧ (rank‘𝐴) ⊆ 𝐵))) | 
| 27 | 13, 26 | bitr4id 290 | . . 3
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → (𝐵 = (rank‘𝐴) ↔ (¬ 𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc
𝐵)))) | 
| 28 | 27 | ex 412 | . 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝐵 ∈ dom
𝑅1 → (𝐵 = (rank‘𝐴) ↔ (¬ 𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc
𝐵))))) | 
| 29 | 4, 12, 28 | pm5.21ndd 379 | 1
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝐵 = (rank‘𝐴) ↔ (¬ 𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc
𝐵)))) |