# 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 ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\wedge \left({A}\subseteq {B}\vee {B}\subseteq {A}\right)\right)\to \left({A}\preccurlyeq {B}↔{A}\subseteq {B}\right)$

### Proof

Step Hyp Ref Expression
1 simpl1 ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\wedge \left({A}\subseteq {B}\vee {B}\subseteq {A}\right)\right)\wedge ¬{A}\subseteq {B}\right)\to {A}\in \mathrm{Fin}$
2 simpr ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\wedge \left({A}\subseteq {B}\vee {B}\subseteq {A}\right)\right)\wedge ¬{A}\subseteq {B}\right)\to ¬{A}\subseteq {B}$
3 simpl3 ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\wedge \left({A}\subseteq {B}\vee {B}\subseteq {A}\right)\right)\wedge ¬{A}\subseteq {B}\right)\to \left({A}\subseteq {B}\vee {B}\subseteq {A}\right)$
4 orel1 ${⊢}¬{A}\subseteq {B}\to \left(\left({A}\subseteq {B}\vee {B}\subseteq {A}\right)\to {B}\subseteq {A}\right)$
5 2 3 4 sylc ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\wedge \left({A}\subseteq {B}\vee {B}\subseteq {A}\right)\right)\wedge ¬{A}\subseteq {B}\right)\to {B}\subseteq {A}$
6 dfpss3 ${⊢}{B}\subset {A}↔\left({B}\subseteq {A}\wedge ¬{A}\subseteq {B}\right)$
7 5 2 6 sylanbrc ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\wedge \left({A}\subseteq {B}\vee {B}\subseteq {A}\right)\right)\wedge ¬{A}\subseteq {B}\right)\to {B}\subset {A}$
8 php3 ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\subset {A}\right)\to {B}\prec {A}$
9 1 7 8 syl2anc ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\wedge \left({A}\subseteq {B}\vee {B}\subseteq {A}\right)\right)\wedge ¬{A}\subseteq {B}\right)\to {B}\prec {A}$
10 9 ex ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\wedge \left({A}\subseteq {B}\vee {B}\subseteq {A}\right)\right)\to \left(¬{A}\subseteq {B}\to {B}\prec {A}\right)$
11 domnsym ${⊢}{A}\preccurlyeq {B}\to ¬{B}\prec {A}$
12 11 con2i ${⊢}{B}\prec {A}\to ¬{A}\preccurlyeq {B}$
13 10 12 syl6 ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\wedge \left({A}\subseteq {B}\vee {B}\subseteq {A}\right)\right)\to \left(¬{A}\subseteq {B}\to ¬{A}\preccurlyeq {B}\right)$
14 13 con4d ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\wedge \left({A}\subseteq {B}\vee {B}\subseteq {A}\right)\right)\to \left({A}\preccurlyeq {B}\to {A}\subseteq {B}\right)$
15 ssdomg ${⊢}{B}\in \mathrm{Fin}\to \left({A}\subseteq {B}\to {A}\preccurlyeq {B}\right)$
16 15 3ad2ant2 ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\wedge \left({A}\subseteq {B}\vee {B}\subseteq {A}\right)\right)\to \left({A}\subseteq {B}\to {A}\preccurlyeq {B}\right)$
17 14 16 impbid ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\wedge \left({A}\subseteq {B}\vee {B}\subseteq {A}\right)\right)\to \left({A}\preccurlyeq {B}↔{A}\subseteq {B}\right)$