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 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵𝐵𝐴 ) ) → ( 𝐴𝐵𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpl1 ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵𝐵𝐴 ) ) ∧ ¬ 𝐴𝐵 ) → 𝐴 ∈ Fin )
2 simpr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵𝐵𝐴 ) ) ∧ ¬ 𝐴𝐵 ) → ¬ 𝐴𝐵 )
3 simpl3 ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵𝐵𝐴 ) ) ∧ ¬ 𝐴𝐵 ) → ( 𝐴𝐵𝐵𝐴 ) )
4 orel1 ( ¬ 𝐴𝐵 → ( ( 𝐴𝐵𝐵𝐴 ) → 𝐵𝐴 ) )
5 2 3 4 sylc ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵𝐵𝐴 ) ) ∧ ¬ 𝐴𝐵 ) → 𝐵𝐴 )
6 dfpss3 ( 𝐵𝐴 ↔ ( 𝐵𝐴 ∧ ¬ 𝐴𝐵 ) )
7 5 2 6 sylanbrc ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵𝐵𝐴 ) ) ∧ ¬ 𝐴𝐵 ) → 𝐵𝐴 )
8 php3 ( ( 𝐴 ∈ Fin ∧ 𝐵𝐴 ) → 𝐵𝐴 )
9 1 7 8 syl2anc ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵𝐵𝐴 ) ) ∧ ¬ 𝐴𝐵 ) → 𝐵𝐴 )
10 9 ex ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵𝐵𝐴 ) ) → ( ¬ 𝐴𝐵𝐵𝐴 ) )
11 domnsym ( 𝐴𝐵 → ¬ 𝐵𝐴 )
12 11 con2i ( 𝐵𝐴 → ¬ 𝐴𝐵 )
13 10 12 syl6 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵𝐵𝐴 ) ) → ( ¬ 𝐴𝐵 → ¬ 𝐴𝐵 ) )
14 13 con4d ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵𝐵𝐴 ) ) → ( 𝐴𝐵𝐴𝐵 ) )
15 ssdomg ( 𝐵 ∈ Fin → ( 𝐴𝐵𝐴𝐵 ) )
16 15 3ad2ant2 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵𝐵𝐴 ) ) → ( 𝐴𝐵𝐴𝐵 ) )
17 14 16 impbid ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵𝐵𝐴 ) ) → ( 𝐴𝐵𝐴𝐵 ) )