Proof of Theorem carden2b
| Step | Hyp | Ref
| Expression |
| 1 | | cardne 10005 |
. . . . 5
⊢
((card‘𝐵)
∈ (card‘𝐴)
→ ¬ (card‘𝐵)
≈ 𝐴) |
| 2 | | ennum 9987 |
. . . . . . . 8
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ dom card ↔ 𝐵 ∈ dom card)) |
| 3 | 2 | biimpa 476 |
. . . . . . 7
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → 𝐵 ∈ dom card) |
| 4 | | cardid2 9993 |
. . . . . . 7
⊢ (𝐵 ∈ dom card →
(card‘𝐵) ≈
𝐵) |
| 5 | 3, 4 | syl 17 |
. . . . . 6
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐵) ≈ 𝐵) |
| 6 | | ensym 9043 |
. . . . . . 7
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
| 7 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → 𝐵 ≈ 𝐴) |
| 8 | | entr 9046 |
. . . . . 6
⊢
(((card‘𝐵)
≈ 𝐵 ∧ 𝐵 ≈ 𝐴) → (card‘𝐵) ≈ 𝐴) |
| 9 | 5, 7, 8 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐵) ≈ 𝐴) |
| 10 | 1, 9 | nsyl3 138 |
. . . 4
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → ¬
(card‘𝐵) ∈
(card‘𝐴)) |
| 11 | | cardon 9984 |
. . . . 5
⊢
(card‘𝐴)
∈ On |
| 12 | | cardon 9984 |
. . . . 5
⊢
(card‘𝐵)
∈ On |
| 13 | | ontri1 6418 |
. . . . 5
⊢
(((card‘𝐴)
∈ On ∧ (card‘𝐵) ∈ On) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ ¬ (card‘𝐵) ∈ (card‘𝐴))) |
| 14 | 11, 12, 13 | mp2an 692 |
. . . 4
⊢
((card‘𝐴)
⊆ (card‘𝐵)
↔ ¬ (card‘𝐵)
∈ (card‘𝐴)) |
| 15 | 10, 14 | sylibr 234 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐴) ⊆ (card‘𝐵)) |
| 16 | | cardne 10005 |
. . . . 5
⊢
((card‘𝐴)
∈ (card‘𝐵)
→ ¬ (card‘𝐴)
≈ 𝐵) |
| 17 | | cardid2 9993 |
. . . . . 6
⊢ (𝐴 ∈ dom card →
(card‘𝐴) ≈
𝐴) |
| 18 | | id 22 |
. . . . . 6
⊢ (𝐴 ≈ 𝐵 → 𝐴 ≈ 𝐵) |
| 19 | | entr 9046 |
. . . . . 6
⊢
(((card‘𝐴)
≈ 𝐴 ∧ 𝐴 ≈ 𝐵) → (card‘𝐴) ≈ 𝐵) |
| 20 | 17, 18, 19 | syl2anr 597 |
. . . . 5
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐴) ≈ 𝐵) |
| 21 | 16, 20 | nsyl3 138 |
. . . 4
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → ¬
(card‘𝐴) ∈
(card‘𝐵)) |
| 22 | | ontri1 6418 |
. . . . 5
⊢
(((card‘𝐵)
∈ On ∧ (card‘𝐴) ∈ On) → ((card‘𝐵) ⊆ (card‘𝐴) ↔ ¬ (card‘𝐴) ∈ (card‘𝐵))) |
| 23 | 12, 11, 22 | mp2an 692 |
. . . 4
⊢
((card‘𝐵)
⊆ (card‘𝐴)
↔ ¬ (card‘𝐴)
∈ (card‘𝐵)) |
| 24 | 21, 23 | sylibr 234 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐵) ⊆ (card‘𝐴)) |
| 25 | 15, 24 | eqssd 4001 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐴) = (card‘𝐵)) |
| 26 | | ndmfv 6941 |
. . . 4
⊢ (¬
𝐴 ∈ dom card →
(card‘𝐴) =
∅) |
| 27 | 26 | adantl 481 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card) → (card‘𝐴) = ∅) |
| 28 | 2 | notbid 318 |
. . . . 5
⊢ (𝐴 ≈ 𝐵 → (¬ 𝐴 ∈ dom card ↔ ¬ 𝐵 ∈ dom
card)) |
| 29 | 28 | biimpa 476 |
. . . 4
⊢ ((𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card) → ¬ 𝐵 ∈ dom
card) |
| 30 | | ndmfv 6941 |
. . . 4
⊢ (¬
𝐵 ∈ dom card →
(card‘𝐵) =
∅) |
| 31 | 29, 30 | syl 17 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card) → (card‘𝐵) = ∅) |
| 32 | 27, 31 | eqtr4d 2780 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card) → (card‘𝐴) = (card‘𝐵)) |
| 33 | 25, 32 | pm2.61dan 813 |
1
⊢ (𝐴 ≈ 𝐵 → (card‘𝐴) = (card‘𝐵)) |