# Metamath Proof Explorer

## Theorem fin23lem25

Description: Lemma for fin23 . In a chain of finite sets, equinumerosity is equivalent to equality. (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Assertion fin23lem25
`|- ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) -> ( A ~~ B <-> A = B ) )`

### Proof

Step Hyp Ref Expression
1 dfpss2
` |-  ( A C. B <-> ( A C_ B /\ -. A = B ) )`
2 php3
` |-  ( ( B e. Fin /\ A C. B ) -> A ~< B )`
3 sdomnen
` |-  ( A ~< B -> -. A ~~ B )`
4 2 3 syl
` |-  ( ( B e. Fin /\ A C. B ) -> -. A ~~ B )`
5 4 ex
` |-  ( B e. Fin -> ( A C. B -> -. A ~~ B ) )`
6 1 5 syl5bir
` |-  ( B e. Fin -> ( ( A C_ B /\ -. A = B ) -> -. A ~~ B ) )`
` |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( A C_ B /\ -. A = B ) -> -. A ~~ B ) )`
8 7 expd
` |-  ( ( A e. Fin /\ B e. Fin ) -> ( A C_ B -> ( -. A = B -> -. A ~~ B ) ) )`
9 dfpss2
` |-  ( B C. A <-> ( B C_ A /\ -. B = A ) )`
10 eqcom
` |-  ( B = A <-> A = B )`
11 10 notbii
` |-  ( -. B = A <-> -. A = B )`
12 11 anbi2i
` |-  ( ( B C_ A /\ -. B = A ) <-> ( B C_ A /\ -. A = B ) )`
13 9 12 bitri
` |-  ( B C. A <-> ( B C_ A /\ -. A = B ) )`
14 php3
` |-  ( ( A e. Fin /\ B C. A ) -> B ~< A )`
15 sdomnen
` |-  ( B ~< A -> -. B ~~ A )`
16 ensym
` |-  ( A ~~ B -> B ~~ A )`
17 15 16 nsyl
` |-  ( B ~< A -> -. A ~~ B )`
18 14 17 syl
` |-  ( ( A e. Fin /\ B C. A ) -> -. A ~~ B )`
19 18 ex
` |-  ( A e. Fin -> ( B C. A -> -. A ~~ B ) )`
20 13 19 syl5bir
` |-  ( A e. Fin -> ( ( B C_ A /\ -. A = B ) -> -. A ~~ B ) )`
` |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( B C_ A /\ -. A = B ) -> -. A ~~ B ) )`
22 21 expd
` |-  ( ( A e. Fin /\ B e. Fin ) -> ( B C_ A -> ( -. A = B -> -. A ~~ B ) ) )`
23 8 22 jaod
` |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( A C_ B \/ B C_ A ) -> ( -. A = B -> -. A ~~ B ) ) )`
24 23 3impia
` |-  ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) -> ( -. A = B -> -. A ~~ B ) )`
25 24 con4d
` |-  ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) -> ( A ~~ B -> A = B ) )`
26 eqeng
` |-  ( A e. Fin -> ( A = B -> A ~~ B ) )`
` |-  ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) -> ( A = B -> A ~~ B ) )`
` |-  ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) -> ( A ~~ B <-> A = B ) )`