Proof of Theorem carden2b
Step | Hyp | Ref
| Expression |
1 | | cardne 9460 |
. . . . 5
⊢
((card‘𝐵)
∈ (card‘𝐴)
→ ¬ (card‘𝐵)
≈ 𝐴) |
2 | | ennum 9442 |
. . . . . . . 8
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ dom card ↔ 𝐵 ∈ dom card)) |
3 | 2 | biimpa 480 |
. . . . . . 7
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → 𝐵 ∈ dom card) |
4 | | cardid2 9448 |
. . . . . . 7
⊢ (𝐵 ∈ dom card →
(card‘𝐵) ≈
𝐵) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐵) ≈ 𝐵) |
6 | | ensym 8597 |
. . . . . . 7
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
7 | 6 | adantr 484 |
. . . . . 6
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → 𝐵 ≈ 𝐴) |
8 | | entr 8600 |
. . . . . 6
⊢
(((card‘𝐵)
≈ 𝐵 ∧ 𝐵 ≈ 𝐴) → (card‘𝐵) ≈ 𝐴) |
9 | 5, 7, 8 | syl2anc 587 |
. . . . 5
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐵) ≈ 𝐴) |
10 | 1, 9 | nsyl3 140 |
. . . 4
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → ¬
(card‘𝐵) ∈
(card‘𝐴)) |
11 | | cardon 9439 |
. . . . 5
⊢
(card‘𝐴)
∈ On |
12 | | cardon 9439 |
. . . . 5
⊢
(card‘𝐵)
∈ On |
13 | | ontri1 6200 |
. . . . 5
⊢
(((card‘𝐴)
∈ On ∧ (card‘𝐵) ∈ On) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ ¬ (card‘𝐵) ∈ (card‘𝐴))) |
14 | 11, 12, 13 | mp2an 692 |
. . . 4
⊢
((card‘𝐴)
⊆ (card‘𝐵)
↔ ¬ (card‘𝐵)
∈ (card‘𝐴)) |
15 | 10, 14 | sylibr 237 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐴) ⊆ (card‘𝐵)) |
16 | | cardne 9460 |
. . . . 5
⊢
((card‘𝐴)
∈ (card‘𝐵)
→ ¬ (card‘𝐴)
≈ 𝐵) |
17 | | cardid2 9448 |
. . . . . 6
⊢ (𝐴 ∈ dom card →
(card‘𝐴) ≈
𝐴) |
18 | | id 22 |
. . . . . 6
⊢ (𝐴 ≈ 𝐵 → 𝐴 ≈ 𝐵) |
19 | | entr 8600 |
. . . . . 6
⊢
(((card‘𝐴)
≈ 𝐴 ∧ 𝐴 ≈ 𝐵) → (card‘𝐴) ≈ 𝐵) |
20 | 17, 18, 19 | syl2anr 600 |
. . . . 5
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐴) ≈ 𝐵) |
21 | 16, 20 | nsyl3 140 |
. . . 4
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → ¬
(card‘𝐴) ∈
(card‘𝐵)) |
22 | | ontri1 6200 |
. . . . 5
⊢
(((card‘𝐵)
∈ On ∧ (card‘𝐴) ∈ On) → ((card‘𝐵) ⊆ (card‘𝐴) ↔ ¬ (card‘𝐴) ∈ (card‘𝐵))) |
23 | 12, 11, 22 | mp2an 692 |
. . . 4
⊢
((card‘𝐵)
⊆ (card‘𝐴)
↔ ¬ (card‘𝐴)
∈ (card‘𝐵)) |
24 | 21, 23 | sylibr 237 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐵) ⊆ (card‘𝐴)) |
25 | 15, 24 | eqssd 3892 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐴) = (card‘𝐵)) |
26 | | ndmfv 6698 |
. . . 4
⊢ (¬
𝐴 ∈ dom card →
(card‘𝐴) =
∅) |
27 | 26 | adantl 485 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card) → (card‘𝐴) = ∅) |
28 | 2 | notbid 321 |
. . . . 5
⊢ (𝐴 ≈ 𝐵 → (¬ 𝐴 ∈ dom card ↔ ¬ 𝐵 ∈ dom
card)) |
29 | 28 | biimpa 480 |
. . . 4
⊢ ((𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card) → ¬ 𝐵 ∈ dom
card) |
30 | | ndmfv 6698 |
. . . 4
⊢ (¬
𝐵 ∈ dom card →
(card‘𝐵) =
∅) |
31 | 29, 30 | syl 17 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card) → (card‘𝐵) = ∅) |
32 | 27, 31 | eqtr4d 2776 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card) → (card‘𝐴) = (card‘𝐵)) |
33 | 25, 32 | pm2.61dan 813 |
1
⊢ (𝐴 ≈ 𝐵 → (card‘𝐴) = (card‘𝐵)) |