Proof of Theorem rankr1c
Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . 4
⊢ (𝐵 = (rank‘𝐴) → 𝐵 = (rank‘𝐴)) |
2 | | rankdmr1 9417 |
. . . 4
⊢
(rank‘𝐴)
∈ dom 𝑅1 |
3 | 1, 2 | eqeltrdi 2846 |
. . 3
⊢ (𝐵 = (rank‘𝐴) → 𝐵 ∈ dom
𝑅1) |
4 | 3 | a1i 11 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝐵 = (rank‘𝐴) → 𝐵 ∈ dom
𝑅1)) |
5 | | elfvdm 6749 |
. . . . 5
⊢ (𝐴 ∈
(𝑅1‘suc 𝐵) → suc 𝐵 ∈ dom
𝑅1) |
6 | | r1funlim 9382 |
. . . . . . 7
⊢ (Fun
𝑅1 ∧ Lim dom 𝑅1) |
7 | 6 | simpri 489 |
. . . . . 6
⊢ Lim dom
𝑅1 |
8 | | limsuc 7628 |
. . . . . 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 237 |
. . . 4
⊢ (𝐴 ∈
(𝑅1‘suc 𝐵) → 𝐵 ∈ dom
𝑅1) |
11 | 10 | adantl 485 |
. . 3
⊢ ((¬
𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc
𝐵)) → 𝐵 ∈ dom
𝑅1) |
12 | 11 | a1i 11 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ((¬ 𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc
𝐵)) → 𝐵 ∈ dom
𝑅1)) |
13 | | eqss 3916 |
. . . 4
⊢ (𝐵 = (rank‘𝐴) ↔ (𝐵 ⊆ (rank‘𝐴) ∧ (rank‘𝐴) ⊆ 𝐵)) |
14 | | rankr1clem 9436 |
. . . . 5
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → (¬ 𝐴 ∈ (𝑅1‘𝐵) ↔ 𝐵 ⊆ (rank‘𝐴))) |
15 | | rankr1ag 9418 |
. . . . . . 7
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ suc 𝐵 ∈ dom
𝑅1) → (𝐴 ∈ (𝑅1‘suc
𝐵) ↔ (rank‘𝐴) ∈ suc 𝐵)) |
16 | 9, 15 | sylan2b 597 |
. . . . . 6
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → (𝐴 ∈ (𝑅1‘suc
𝐵) ↔ (rank‘𝐴) ∈ suc 𝐵)) |
17 | | rankon 9411 |
. . . . . . 7
⊢
(rank‘𝐴)
∈ On |
18 | | limord 6272 |
. . . . . . . . . 10
⊢ (Lim dom
𝑅1 → Ord dom 𝑅1) |
19 | 7, 18 | ax-mp 5 |
. . . . . . . . 9
⊢ Ord dom
𝑅1 |
20 | | ordelon 6237 |
. . . . . . . . 9
⊢ ((Ord dom
𝑅1 ∧ 𝐵 ∈ dom 𝑅1) →
𝐵 ∈
On) |
21 | 19, 20 | mpan 690 |
. . . . . . . 8
⊢ (𝐵 ∈ dom
𝑅1 → 𝐵 ∈ On) |
22 | 21 | adantl 485 |
. . . . . . 7
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → 𝐵 ∈ On) |
23 | | onsssuc 6300 |
. . . . . . 7
⊢
(((rank‘𝐴)
∈ On ∧ 𝐵 ∈
On) → ((rank‘𝐴)
⊆ 𝐵 ↔
(rank‘𝐴) ∈ suc
𝐵)) |
24 | 17, 22, 23 | sylancr 590 |
. . . . . 6
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → ((rank‘𝐴) ⊆ 𝐵 ↔ (rank‘𝐴) ∈ suc 𝐵)) |
25 | 16, 24 | bitr4d 285 |
. . . . 5
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → (𝐴 ∈ (𝑅1‘suc
𝐵) ↔ (rank‘𝐴) ⊆ 𝐵)) |
26 | 14, 25 | anbi12d 634 |
. . . 4
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → ((¬ 𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc
𝐵)) ↔ (𝐵 ⊆ (rank‘𝐴) ∧ (rank‘𝐴) ⊆ 𝐵))) |
27 | 13, 26 | bitr4id 293 |
. . 3
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom
𝑅1) → (𝐵 = (rank‘𝐴) ↔ (¬ 𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc
𝐵)))) |
28 | 27 | ex 416 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝐵 ∈ dom
𝑅1 → (𝐵 = (rank‘𝐴) ↔ (¬ 𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc
𝐵))))) |
29 | 4, 12, 28 | pm5.21ndd 384 |
1
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝐵 = (rank‘𝐴) ↔ (¬ 𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐴 ∈ (𝑅1‘suc
𝐵)))) |