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∈Fin∧B∈Fin∧A⊆B∨B⊆A→A≼B↔A⊆B

Proof

Step Hyp Ref Expression
1 simpl1 ⊢A∈Fin∧B∈Fin∧A⊆B∨B⊆A∧¬A⊆B→A∈Fin
2 simpr ⊢A∈Fin∧B∈Fin∧A⊆B∨B⊆A∧¬A⊆B→¬A⊆B
3 simpl3 ⊢A∈Fin∧B∈Fin∧A⊆B∨B⊆A∧¬A⊆B→A⊆B∨B⊆A
4 orel1 ⊢¬A⊆B→A⊆B∨B⊆A→B⊆A
5 2 3 4 sylc ⊢A∈Fin∧B∈Fin∧A⊆B∨B⊆A∧¬A⊆B→B⊆A
6 dfpss3 ⊢B⊂A↔B⊆A∧¬A⊆B
7 5 2 6 sylanbrc ⊢A∈Fin∧B∈Fin∧A⊆B∨B⊆A∧¬A⊆B→B⊂A
8 php3 ⊢A∈Fin∧B⊂A→B≺A
9 1 7 8 syl2anc ⊢A∈Fin∧B∈Fin∧A⊆B∨B⊆A∧¬A⊆B→B≺A
10 9 ex ⊢A∈Fin∧B∈Fin∧A⊆B∨B⊆A→¬A⊆B→B≺A
11 domnsym ⊢A≼B→¬B≺A
12 11 con2i ⊢B≺A→¬A≼B
13 10 12 syl6 ⊢A∈Fin∧B∈Fin∧A⊆B∨B⊆A→¬A⊆B→¬A≼B
14 13 con4d ⊢A∈Fin∧B∈Fin∧A⊆B∨B⊆A→A≼B→A⊆B
15 ssdomg ⊢B∈Fin→A⊆B→A≼B
16 15 3ad2ant2 ⊢A∈Fin∧B∈Fin∧A⊆B∨B⊆A→A⊆B→A≼B
17 14 16 impbid ⊢A∈Fin∧B∈Fin∧A⊆B∨B⊆A→A≼B↔A⊆B