Proof of Theorem carden2b
Step | Hyp | Ref
| Expression |
1 | | cardne 9723 |
. . . . 5
⊢
((card‘𝐵)
∈ (card‘𝐴)
→ ¬ (card‘𝐵)
≈ 𝐴) |
2 | | ennum 9705 |
. . . . . . . 8
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ dom card ↔ 𝐵 ∈ dom card)) |
3 | 2 | biimpa 477 |
. . . . . . 7
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → 𝐵 ∈ dom card) |
4 | | cardid2 9711 |
. . . . . . 7
⊢ (𝐵 ∈ dom card →
(card‘𝐵) ≈
𝐵) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐵) ≈ 𝐵) |
6 | | ensym 8789 |
. . . . . . 7
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
7 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → 𝐵 ≈ 𝐴) |
8 | | entr 8792 |
. . . . . 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 9702 |
. . . . 5
⊢
(card‘𝐴)
∈ On |
12 | | cardon 9702 |
. . . . 5
⊢
(card‘𝐵)
∈ On |
13 | | ontri1 6300 |
. . . . 5
⊢
(((card‘𝐴)
∈ On ∧ (card‘𝐵) ∈ On) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ ¬ (card‘𝐵) ∈ (card‘𝐴))) |
14 | 11, 12, 13 | mp2an 689 |
. . . 4
⊢
((card‘𝐴)
⊆ (card‘𝐵)
↔ ¬ (card‘𝐵)
∈ (card‘𝐴)) |
15 | 10, 14 | sylibr 233 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐴) ⊆ (card‘𝐵)) |
16 | | cardne 9723 |
. . . . 5
⊢
((card‘𝐴)
∈ (card‘𝐵)
→ ¬ (card‘𝐴)
≈ 𝐵) |
17 | | cardid2 9711 |
. . . . . 6
⊢ (𝐴 ∈ dom card →
(card‘𝐴) ≈
𝐴) |
18 | | id 22 |
. . . . . 6
⊢ (𝐴 ≈ 𝐵 → 𝐴 ≈ 𝐵) |
19 | | entr 8792 |
. . . . . 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 6300 |
. . . . 5
⊢
(((card‘𝐵)
∈ On ∧ (card‘𝐴) ∈ On) → ((card‘𝐵) ⊆ (card‘𝐴) ↔ ¬ (card‘𝐴) ∈ (card‘𝐵))) |
23 | 12, 11, 22 | mp2an 689 |
. . . 4
⊢
((card‘𝐵)
⊆ (card‘𝐴)
↔ ¬ (card‘𝐴)
∈ (card‘𝐵)) |
24 | 21, 23 | sylibr 233 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐵) ⊆ (card‘𝐴)) |
25 | 15, 24 | eqssd 3938 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card) → (card‘𝐴) = (card‘𝐵)) |
26 | | ndmfv 6804 |
. . . 4
⊢ (¬
𝐴 ∈ dom card →
(card‘𝐴) =
∅) |
27 | 26 | adantl 482 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card) → (card‘𝐴) = ∅) |
28 | 2 | notbid 318 |
. . . . 5
⊢ (𝐴 ≈ 𝐵 → (¬ 𝐴 ∈ dom card ↔ ¬ 𝐵 ∈ dom
card)) |
29 | 28 | biimpa 477 |
. . . 4
⊢ ((𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card) → ¬ 𝐵 ∈ dom
card) |
30 | | ndmfv 6804 |
. . . 4
⊢ (¬
𝐵 ∈ dom card →
(card‘𝐵) =
∅) |
31 | 29, 30 | syl 17 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card) → (card‘𝐵) = ∅) |
32 | 27, 31 | eqtr4d 2781 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card) → (card‘𝐴) = (card‘𝐵)) |
33 | 25, 32 | pm2.61dan 810 |
1
⊢ (𝐴 ≈ 𝐵 → (card‘𝐴) = (card‘𝐵)) |