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 ⊢A∈Fin∧B∈Fin∧A⊆B∨B⊆A→A≈B↔A=B

Proof

Step Hyp Ref Expression
1 dfpss2 ⊢A⊂B↔A⊆B∧¬A=B
2 php3 ⊢B∈Fin∧A⊂B→A≺B
3 sdomnen ⊢A≺B→¬A≈B
4 2 3 syl ⊢B∈Fin∧A⊂B→¬A≈B
5 4 ex ⊢B∈Fin→A⊂B→¬A≈B
6 1 5 biimtrrid ⊢B∈Fin→A⊆B∧¬A=B→¬A≈B
7 6 adantl ⊢A∈Fin∧B∈Fin→A⊆B∧¬A=B→¬A≈B
8 7 expd ⊢A∈Fin∧B∈Fin→A⊆B→¬A=B→¬A≈B
9 dfpss2 ⊢B⊂A↔B⊆A∧¬B=A
10 eqcom ⊢B=A↔A=B
11 10 notbii ⊢¬B=A↔¬A=B
12 11 anbi2i ⊢B⊆A∧¬B=A↔B⊆A∧¬A=B
13 9 12 bitri ⊢B⊂A↔B⊆A∧¬A=B
14 php3 ⊢A∈Fin∧B⊂A→B≺A
15 sdomnen ⊢B≺A→¬B≈A
16 ensym ⊢A≈B→B≈A
17 15 16 nsyl ⊢B≺A→¬A≈B
18 14 17 syl ⊢A∈Fin∧B⊂A→¬A≈B
19 18 ex ⊢A∈Fin→B⊂A→¬A≈B
20 13 19 biimtrrid ⊢A∈Fin→B⊆A∧¬A=B→¬A≈B
21 20 adantr ⊢A∈Fin∧B∈Fin→B⊆A∧¬A=B→¬A≈B
22 21 expd ⊢A∈Fin∧B∈Fin→B⊆A→¬A=B→¬A≈B
23 8 22 jaod ⊢A∈Fin∧B∈Fin→A⊆B∨B⊆A→¬A=B→¬A≈B
24 23 3impia ⊢A∈Fin∧B∈Fin∧A⊆B∨B⊆A→¬A=B→¬A≈B
25 24 con4d ⊢A∈Fin∧B∈Fin∧A⊆B∨B⊆A→A≈B→A=B
26 eqeng ⊢A∈Fin→A=B→A≈B
27 26 3ad2ant1 ⊢A∈Fin∧B∈Fin∧A⊆B∨B⊆A→A=B→A≈B
28 25 27 impbid ⊢A∈Fin∧B∈Fin∧A⊆B∨B⊆A→A≈B↔A=B