# Metamath Proof Explorer

## Theorem fin23lem25

Description: Lemma for fin23 . In a chain of finite sets, equinumerosity is equivalent to equality. (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Assertion fin23lem25 ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\wedge \left({A}\subseteq {B}\vee {B}\subseteq {A}\right)\right)\to \left({A}\approx {B}↔{A}={B}\right)$

### Proof

Step Hyp Ref Expression
1 dfpss2 ${⊢}{A}\subset {B}↔\left({A}\subseteq {B}\wedge ¬{A}={B}\right)$
2 php3 ${⊢}\left({B}\in \mathrm{Fin}\wedge {A}\subset {B}\right)\to {A}\prec {B}$
3 sdomnen ${⊢}{A}\prec {B}\to ¬{A}\approx {B}$
4 2 3 syl ${⊢}\left({B}\in \mathrm{Fin}\wedge {A}\subset {B}\right)\to ¬{A}\approx {B}$
5 4 ex ${⊢}{B}\in \mathrm{Fin}\to \left({A}\subset {B}\to ¬{A}\approx {B}\right)$
6 1 5 syl5bir ${⊢}{B}\in \mathrm{Fin}\to \left(\left({A}\subseteq {B}\wedge ¬{A}={B}\right)\to ¬{A}\approx {B}\right)$
7 6 adantl ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left(\left({A}\subseteq {B}\wedge ¬{A}={B}\right)\to ¬{A}\approx {B}\right)$
8 7 expd ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left({A}\subseteq {B}\to \left(¬{A}={B}\to ¬{A}\approx {B}\right)\right)$
9 dfpss2 ${⊢}{B}\subset {A}↔\left({B}\subseteq {A}\wedge ¬{B}={A}\right)$
10 eqcom ${⊢}{B}={A}↔{A}={B}$
11 10 notbii ${⊢}¬{B}={A}↔¬{A}={B}$
12 11 anbi2i ${⊢}\left({B}\subseteq {A}\wedge ¬{B}={A}\right)↔\left({B}\subseteq {A}\wedge ¬{A}={B}\right)$
13 9 12 bitri ${⊢}{B}\subset {A}↔\left({B}\subseteq {A}\wedge ¬{A}={B}\right)$
14 php3 ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\subset {A}\right)\to {B}\prec {A}$
15 sdomnen ${⊢}{B}\prec {A}\to ¬{B}\approx {A}$
16 ensym ${⊢}{A}\approx {B}\to {B}\approx {A}$
17 15 16 nsyl ${⊢}{B}\prec {A}\to ¬{A}\approx {B}$
18 14 17 syl ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\subset {A}\right)\to ¬{A}\approx {B}$
19 18 ex ${⊢}{A}\in \mathrm{Fin}\to \left({B}\subset {A}\to ¬{A}\approx {B}\right)$
20 13 19 syl5bir ${⊢}{A}\in \mathrm{Fin}\to \left(\left({B}\subseteq {A}\wedge ¬{A}={B}\right)\to ¬{A}\approx {B}\right)$
21 20 adantr ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left(\left({B}\subseteq {A}\wedge ¬{A}={B}\right)\to ¬{A}\approx {B}\right)$
22 21 expd ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left({B}\subseteq {A}\to \left(¬{A}={B}\to ¬{A}\approx {B}\right)\right)$
23 8 22 jaod ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left(\left({A}\subseteq {B}\vee {B}\subseteq {A}\right)\to \left(¬{A}={B}\to ¬{A}\approx {B}\right)\right)$
24 23 3impia ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\wedge \left({A}\subseteq {B}\vee {B}\subseteq {A}\right)\right)\to \left(¬{A}={B}\to ¬{A}\approx {B}\right)$
25 24 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}\approx {B}\to {A}={B}\right)$
26 eqeng ${⊢}{A}\in \mathrm{Fin}\to \left({A}={B}\to {A}\approx {B}\right)$
27 26 3ad2ant1 ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\wedge \left({A}\subseteq {B}\vee {B}\subseteq {A}\right)\right)\to \left({A}={B}\to {A}\approx {B}\right)$
28 25 27 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}\approx {B}↔{A}={B}\right)$