Proof of Theorem carden2b
Step | Hyp | Ref
| Expression |
1 | | cardne 8674 |
. . . . 5
⊢
((card‘𝐵)
∈ (card‘𝐴)
→ ¬ (card‘𝐵)
≈ 𝐴) |
2 | | ennum 8656 |
. . . . . . . 8
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ dom card ↔ 𝐵 ∈ dom card)) |
3 | 2 | biimpa 500 |
. . . . . . 7
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → 𝐵 ∈ dom card) |
4 | | cardid2 8662 |
. . . . . . 7
⊢ (𝐵 ∈ dom card →
(card‘𝐵) ≈
𝐵) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐵) ≈ 𝐵) |
6 | | ensym 7891 |
. . . . . . 7
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
7 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → 𝐵 ≈ 𝐴) |
8 | | entr 7894 |
. . . . . 6
⊢
(((card‘𝐵)
≈ 𝐵 ∧ 𝐵 ≈ 𝐴) → (card‘𝐵) ≈ 𝐴) |
9 | 5, 7, 8 | syl2anc 691 |
. . . . 5
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐵) ≈ 𝐴) |
10 | 1, 9 | nsyl3 132 |
. . . 4
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → ¬
(card‘𝐵) ∈
(card‘𝐴)) |
11 | | cardon 8653 |
. . . . 5
⊢
(card‘𝐴)
∈ On |
12 | | cardon 8653 |
. . . . 5
⊢
(card‘𝐵)
∈ On |
13 | | ontri1 5674 |
. . . . 5
⊢
(((card‘𝐴)
∈ On ∧ (card‘𝐵) ∈ On) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ ¬ (card‘𝐵) ∈ (card‘𝐴))) |
14 | 11, 12, 13 | mp2an 704 |
. . . 4
⊢
((card‘𝐴)
⊆ (card‘𝐵)
↔ ¬ (card‘𝐵)
∈ (card‘𝐴)) |
15 | 10, 14 | sylibr 223 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐴) ⊆ (card‘𝐵)) |
16 | | cardne 8674 |
. . . . 5
⊢
((card‘𝐴)
∈ (card‘𝐵)
→ ¬ (card‘𝐴)
≈ 𝐵) |
17 | | cardid2 8662 |
. . . . . 6
⊢ (𝐴 ∈ dom card →
(card‘𝐴) ≈
𝐴) |
18 | | id 22 |
. . . . . 6
⊢ (𝐴 ≈ 𝐵 → 𝐴 ≈ 𝐵) |
19 | | entr 7894 |
. . . . . 6
⊢
(((card‘𝐴)
≈ 𝐴 ∧ 𝐴 ≈ 𝐵) → (card‘𝐴) ≈ 𝐵) |
20 | 17, 18, 19 | syl2anr 494 |
. . . . 5
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐴) ≈ 𝐵) |
21 | 16, 20 | nsyl3 132 |
. . . 4
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → ¬
(card‘𝐴) ∈
(card‘𝐵)) |
22 | | ontri1 5674 |
. . . . 5
⊢
(((card‘𝐵)
∈ On ∧ (card‘𝐴) ∈ On) → ((card‘𝐵) ⊆ (card‘𝐴) ↔ ¬ (card‘𝐴) ∈ (card‘𝐵))) |
23 | 12, 11, 22 | mp2an 704 |
. . . 4
⊢
((card‘𝐵)
⊆ (card‘𝐴)
↔ ¬ (card‘𝐴)
∈ (card‘𝐵)) |
24 | 21, 23 | sylibr 223 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐵) ⊆ (card‘𝐴)) |
25 | 15, 24 | eqssd 3585 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐴) = (card‘𝐵)) |
26 | | ndmfv 6128 |
. . . 4
⊢ (¬
𝐴 ∈ dom card →
(card‘𝐴) =
∅) |
27 | 26 | adantl 481 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card) → (card‘𝐴) = ∅) |
28 | 2 | notbid 307 |
. . . . 5
⊢ (𝐴 ≈ 𝐵 → (¬ 𝐴 ∈ dom card ↔ ¬ 𝐵 ∈ dom
card)) |
29 | 28 | biimpa 500 |
. . . 4
⊢ ((𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card) → ¬ 𝐵 ∈ dom
card) |
30 | | ndmfv 6128 |
. . . 4
⊢ (¬
𝐵 ∈ dom card →
(card‘𝐵) =
∅) |
31 | 29, 30 | syl 17 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card) → (card‘𝐵) = ∅) |
32 | 27, 31 | eqtr4d 2647 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card) → (card‘𝐴) = (card‘𝐵)) |
33 | 25, 32 | pm2.61dan 828 |
1
⊢ (𝐴 ≈ 𝐵 → (card‘𝐴) = (card‘𝐵)) |