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

Metamath Proof Explorer

Theorem fincssdom

Description: In a chain of finite sets, dominance and subset coincide. (Contributed by Stefan O'Rear, 8-Nov-2014)

Ref Expression
Assertion fincssdom 
|- ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) -> ( A ~<_ B <-> A C_ B ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) /\ -. A C_ B ) -> A e. Fin )
2 simpr 
 |-  ( ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) /\ -. A C_ B ) -> -. A C_ B )
3 simpl3 
 |-  ( ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) /\ -. A C_ B ) -> ( A C_ B \/ B C_ A ) )
4 orel1 
 |-  ( -. A C_ B -> ( ( A C_ B \/ B C_ A ) -> B C_ A ) )
5 2 3 4 sylc 
 |-  ( ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) /\ -. A C_ B ) -> B C_ A )
6 dfpss3 
 |-  ( B C. A <-> ( B C_ A /\ -. A C_ B ) )
7 5 2 6 sylanbrc 
 |-  ( ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) /\ -. A C_ B ) -> B C. A )
8 php3 
 |-  ( ( A e. Fin /\ B C. A ) -> B ~< A )
9 1 7 8 syl2anc 
 |-  ( ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) /\ -. A C_ B ) -> B ~< A )
10 9 ex 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) -> ( -. A C_ B -> B ~< A ) )
11 domnsym 
 |-  ( A ~<_ B -> -. B ~< A )
12 11 con2i 
 |-  ( B ~< A -> -. A ~<_ B )
13 10 12 syl6 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) -> ( -. A C_ B -> -. A ~<_ B ) )
14 13 con4d 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) -> ( A ~<_ B -> A C_ B ) )
15 ssdomg 
 |-  ( B e. Fin -> ( A C_ B -> A ~<_ B ) )
16 15 3ad2ant2 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) -> ( A C_ B -> A ~<_ B ) )
17 14 16 impbid 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A C_ B \/ B C_ A ) ) -> ( A ~<_ B <-> A C_ B ) )