Metamath Proof Explorer

Theorem carden2b

Description: If two sets are equinumerous, then they have equal cardinalities. (This assertion and carden2a are meant to replace carden in ZF without AC.) (Contributed by Mario Carneiro, 9-Jan-2013) (Proof shortened by Mario Carneiro, 27-Apr-2015)

Ref Expression
Assertion carden2b ( 𝐴 ≈ 𝐵 → ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 cardne ⊢ ( ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) → ¬ ( card ‘ 𝐵 ) ≈ 𝐴 )
2 ennum ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ dom card ↔ 𝐵 ∈ dom card ) )
3 2 biimpa ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card ) → 𝐵 ∈ dom card )
4 cardid2 ⊢ ( 𝐵 ∈ dom card → ( card ‘ 𝐵 ) ≈ 𝐵 )
5 3 4 syl ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card ) → ( card ‘ 𝐵 ) ≈ 𝐵 )
6 ensym ⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴 )
7 6 adantr ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card ) → 𝐵 ≈ 𝐴 )
8 entr ⊢ ( ( ( card ‘ 𝐵 ) ≈ 𝐵 ∧ 𝐵 ≈ 𝐴 ) → ( card ‘ 𝐵 ) ≈ 𝐴 )
9 5 7 8 syl2anc ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card ) → ( card ‘ 𝐵 ) ≈ 𝐴 )
10 1 9 nsyl3 ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card ) → ¬ ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) )
11 cardon ⊢ ( card ‘ 𝐴 ) ∈ On
12 cardon ⊢ ( card ‘ 𝐵 ) ∈ On
13 ontri1 ⊢ ( ( ( card ‘ 𝐴 ) ∈ On ∧ ( card ‘ 𝐵 ) ∈ On ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ ¬ ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) ) )
14 11 12 13 mp2an ⊢ ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ ¬ ( card ‘ 𝐵 ) ∈ ( card ‘ 𝐴 ) )
15 10 14 sylibr ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card ) → ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) )
16 cardne ⊢ ( ( card ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) → ¬ ( card ‘ 𝐴 ) ≈ 𝐵 )
17 cardid2 ⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 )
18 id ⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ≈ 𝐵 )
19 entr ⊢ ( ( ( card ‘ 𝐴 ) ≈ 𝐴 ∧ 𝐴 ≈ 𝐵 ) → ( card ‘ 𝐴 ) ≈ 𝐵 )
20 17 18 19 syl2anr ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card ) → ( card ‘ 𝐴 ) ≈ 𝐵 )
21 16 20 nsyl3 ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card ) → ¬ ( card ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) )
22 ontri1 ⊢ ( ( ( card ‘ 𝐵 ) ∈ On ∧ ( card ‘ 𝐴 ) ∈ On ) → ( ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐴 ) ↔ ¬ ( card ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) ) )
23 12 11 22 mp2an ⊢ ( ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐴 ) ↔ ¬ ( card ‘ 𝐴 ) ∈ ( card ‘ 𝐵 ) )
24 21 23 sylibr ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card ) → ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐴 ) )
25 15 24 eqssd ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐴 ∈ dom card ) → ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) )
26 ndmfv ⊢ ( ¬ 𝐴 ∈ dom card → ( card ‘ 𝐴 ) = ∅ )
27 26 adantl ⊢ ( ( 𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card ) → ( card ‘ 𝐴 ) = ∅ )
28 2 notbid ⊢ ( 𝐴 ≈ 𝐵 → ( ¬ 𝐴 ∈ dom card ↔ ¬ 𝐵 ∈ dom card ) )
29 28 biimpa ⊢ ( ( 𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card ) → ¬ 𝐵 ∈ dom card )
30 ndmfv ⊢ ( ¬ 𝐵 ∈ dom card → ( card ‘ 𝐵 ) = ∅ )
31 29 30 syl ⊢ ( ( 𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card ) → ( card ‘ 𝐵 ) = ∅ )
32 27 31 eqtr4d ⊢ ( ( 𝐴 ≈ 𝐵 ∧ ¬ 𝐴 ∈ dom card ) → ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) )
33 25 32 pm2.61dan ⊢ ( 𝐴 ≈ 𝐵 → ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) )