This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrrid 
 |-  ( B e. Fin -> ( ( A C_ B /\ -. A = B ) -> -. A ~~ B ) )
7 6 adantl 
 |-  ( ( 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 biimtrrid 
 |-  ( A e. Fin -> ( ( B C_ A /\ -. A = B ) -> -. A ~~ B ) )
21 20 adantr 
 |-  ( ( 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 ) )
27 26 3ad2ant1 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) -> ( A = B -> A ~~ B ) )
28 25 27 impbid 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) -> ( A ~~ B <-> A = B ) )