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 syl5bir ⊢ 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 syl5bir ⊢ 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