# Metamath Proof Explorer

## Theorem carden2a

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

Ref Expression
Assertion carden2a
`|- ( ( ( card ` A ) = ( card ` B ) /\ ( card ` A ) =/= (/) ) -> A ~~ B )`

### Proof

Step Hyp Ref Expression
1 df-ne
` |-  ( ( card ` A ) =/= (/) <-> -. ( card ` A ) = (/) )`
2 ndmfv
` |-  ( -. B e. dom card -> ( card ` B ) = (/) )`
3 eqeq1
` |-  ( ( card ` A ) = ( card ` B ) -> ( ( card ` A ) = (/) <-> ( card ` B ) = (/) ) )`
4 2 3 syl5ibr
` |-  ( ( card ` A ) = ( card ` B ) -> ( -. B e. dom card -> ( card ` A ) = (/) ) )`
5 4 con1d
` |-  ( ( card ` A ) = ( card ` B ) -> ( -. ( card ` A ) = (/) -> B e. dom card ) )`
6 5 imp
` |-  ( ( ( card ` A ) = ( card ` B ) /\ -. ( card ` A ) = (/) ) -> B e. dom card )`
7 cardid2
` |-  ( B e. dom card -> ( card ` B ) ~~ B )`
8 6 7 syl
` |-  ( ( ( card ` A ) = ( card ` B ) /\ -. ( card ` A ) = (/) ) -> ( card ` B ) ~~ B )`
9 breq2
` |-  ( ( card ` A ) = ( card ` B ) -> ( A ~~ ( card ` A ) <-> A ~~ ( card ` B ) ) )`
10 entr
` |-  ( ( A ~~ ( card ` B ) /\ ( card ` B ) ~~ B ) -> A ~~ B )`
11 10 ex
` |-  ( A ~~ ( card ` B ) -> ( ( card ` B ) ~~ B -> A ~~ B ) )`
12 9 11 syl6bi
` |-  ( ( card ` A ) = ( card ` B ) -> ( A ~~ ( card ` A ) -> ( ( card ` B ) ~~ B -> A ~~ B ) ) )`
13 cardid2
` |-  ( A e. dom card -> ( card ` A ) ~~ A )`
14 ndmfv
` |-  ( -. A e. dom card -> ( card ` A ) = (/) )`
15 13 14 nsyl4
` |-  ( -. ( card ` A ) = (/) -> ( card ` A ) ~~ A )`
16 15 ensymd
` |-  ( -. ( card ` A ) = (/) -> A ~~ ( card ` A ) )`
17 12 16 impel
` |-  ( ( ( card ` A ) = ( card ` B ) /\ -. ( card ` A ) = (/) ) -> ( ( card ` B ) ~~ B -> A ~~ B ) )`
18 8 17 mpd
` |-  ( ( ( card ` A ) = ( card ` B ) /\ -. ( card ` A ) = (/) ) -> A ~~ B )`
19 1 18 sylan2b
` |-  ( ( ( card ` A ) = ( card ` B ) /\ ( card ` A ) =/= (/) ) -> A ~~ B )`