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