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 ( ( 𝐴 ∈ 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 ∧ ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ) → ( 𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )