Proof of Theorem rankaltopb
Step | Hyp | Ref
| Expression |
1 | | snwf 9425 |
. . 3
⊢ (𝐵 ∈ ∪ (𝑅1 “ On) → {𝐵} ∈ ∪ (𝑅1 “ On)) |
2 | | df-altop 33997 |
. . . . . 6
⊢
⟪𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}} |
3 | 2 | fveq2i 6720 |
. . . . 5
⊢
(rank‘⟪𝐴, 𝐵⟫) = (rank‘{{𝐴}, {𝐴, {𝐵}}}) |
4 | | snwf 9425 |
. . . . . . 7
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → {𝐴} ∈ ∪ (𝑅1 “ On)) |
5 | 4 | adantr 484 |
. . . . . 6
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ {𝐵} ∈ ∪ (𝑅1 “ On)) → {𝐴} ∈ ∪ (𝑅1 “ On)) |
6 | | prwf 9427 |
. . . . . 6
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ {𝐵} ∈ ∪ (𝑅1 “ On)) → {𝐴, {𝐵}} ∈ ∪
(𝑅1 “ On)) |
7 | | rankprb 9467 |
. . . . . 6
⊢ (({𝐴} ∈ ∪ (𝑅1 “ On) ∧ {𝐴, {𝐵}} ∈ ∪
(𝑅1 “ On)) → (rank‘{{𝐴}, {𝐴, {𝐵}}}) = suc ((rank‘{𝐴}) ∪ (rank‘{𝐴, {𝐵}}))) |
8 | 5, 6, 7 | syl2anc 587 |
. . . . 5
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ {𝐵} ∈ ∪ (𝑅1 “ On)) →
(rank‘{{𝐴}, {𝐴, {𝐵}}}) = suc ((rank‘{𝐴}) ∪ (rank‘{𝐴, {𝐵}}))) |
9 | 3, 8 | syl5eq 2790 |
. . . 4
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ {𝐵} ∈ ∪ (𝑅1 “ On)) →
(rank‘⟪𝐴,
𝐵⟫) = suc
((rank‘{𝐴}) ∪
(rank‘{𝐴, {𝐵}}))) |
10 | | snsspr1 4727 |
. . . . . . . 8
⊢ {𝐴} ⊆ {𝐴, {𝐵}} |
11 | | ssequn1 4094 |
. . . . . . . 8
⊢ ({𝐴} ⊆ {𝐴, {𝐵}} ↔ ({𝐴} ∪ {𝐴, {𝐵}}) = {𝐴, {𝐵}}) |
12 | 10, 11 | mpbi 233 |
. . . . . . 7
⊢ ({𝐴} ∪ {𝐴, {𝐵}}) = {𝐴, {𝐵}} |
13 | 12 | fveq2i 6720 |
. . . . . 6
⊢
(rank‘({𝐴}
∪ {𝐴, {𝐵}})) = (rank‘{𝐴, {𝐵}}) |
14 | | rankunb 9466 |
. . . . . . 7
⊢ (({𝐴} ∈ ∪ (𝑅1 “ On) ∧ {𝐴, {𝐵}} ∈ ∪
(𝑅1 “ On)) → (rank‘({𝐴} ∪ {𝐴, {𝐵}})) = ((rank‘{𝐴}) ∪ (rank‘{𝐴, {𝐵}}))) |
15 | 5, 6, 14 | syl2anc 587 |
. . . . . 6
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ {𝐵} ∈ ∪ (𝑅1 “ On)) →
(rank‘({𝐴} ∪
{𝐴, {𝐵}})) = ((rank‘{𝐴}) ∪ (rank‘{𝐴, {𝐵}}))) |
16 | | rankprb 9467 |
. . . . . 6
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ {𝐵} ∈ ∪ (𝑅1 “ On)) →
(rank‘{𝐴, {𝐵}}) = suc ((rank‘𝐴) ∪ (rank‘{𝐵}))) |
17 | 13, 15, 16 | 3eqtr3a 2802 |
. . . . 5
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ {𝐵} ∈ ∪ (𝑅1 “ On)) →
((rank‘{𝐴}) ∪
(rank‘{𝐴, {𝐵}})) = suc ((rank‘𝐴) ∪ (rank‘{𝐵}))) |
18 | | suceq 6278 |
. . . . 5
⊢
(((rank‘{𝐴})
∪ (rank‘{𝐴,
{𝐵}})) = suc
((rank‘𝐴) ∪
(rank‘{𝐵})) →
suc ((rank‘{𝐴}) ∪
(rank‘{𝐴, {𝐵}})) = suc suc
((rank‘𝐴) ∪
(rank‘{𝐵}))) |
19 | 17, 18 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ {𝐵} ∈ ∪ (𝑅1 “ On)) → suc
((rank‘{𝐴}) ∪
(rank‘{𝐴, {𝐵}})) = suc suc
((rank‘𝐴) ∪
(rank‘{𝐵}))) |
20 | 9, 19 | eqtrd 2777 |
. . 3
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ {𝐵} ∈ ∪ (𝑅1 “ On)) →
(rank‘⟪𝐴,
𝐵⟫) = suc suc
((rank‘𝐴) ∪
(rank‘{𝐵}))) |
21 | 1, 20 | sylan2 596 |
. 2
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) →
(rank‘⟪𝐴,
𝐵⟫) = suc suc
((rank‘𝐴) ∪
(rank‘{𝐵}))) |
22 | | ranksnb 9443 |
. . . . 5
⊢ (𝐵 ∈ ∪ (𝑅1 “ On) →
(rank‘{𝐵}) = suc
(rank‘𝐵)) |
23 | 22 | uneq2d 4077 |
. . . 4
⊢ (𝐵 ∈ ∪ (𝑅1 “ On) →
((rank‘𝐴) ∪
(rank‘{𝐵})) =
((rank‘𝐴) ∪ suc
(rank‘𝐵))) |
24 | | suceq 6278 |
. . . 4
⊢
(((rank‘𝐴)
∪ (rank‘{𝐵})) =
((rank‘𝐴) ∪ suc
(rank‘𝐵)) → suc
((rank‘𝐴) ∪
(rank‘{𝐵})) = suc
((rank‘𝐴) ∪ suc
(rank‘𝐵))) |
25 | | suceq 6278 |
. . . 4
⊢ (suc
((rank‘𝐴) ∪
(rank‘{𝐵})) = suc
((rank‘𝐴) ∪ suc
(rank‘𝐵)) → suc
suc ((rank‘𝐴) ∪
(rank‘{𝐵})) = suc suc
((rank‘𝐴) ∪ suc
(rank‘𝐵))) |
26 | 23, 24, 25 | 3syl 18 |
. . 3
⊢ (𝐵 ∈ ∪ (𝑅1 “ On) → suc suc
((rank‘𝐴) ∪
(rank‘{𝐵})) = suc suc
((rank‘𝐴) ∪ suc
(rank‘𝐵))) |
27 | 26 | adantl 485 |
. 2
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → suc suc
((rank‘𝐴) ∪
(rank‘{𝐵})) = suc suc
((rank‘𝐴) ∪ suc
(rank‘𝐵))) |
28 | 21, 27 | eqtrd 2777 |
1
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) →
(rank‘⟪𝐴,
𝐵⟫) = suc suc
((rank‘𝐴) ∪ suc
(rank‘𝐵))) |