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