This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ) → ( 𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵 ) )

Proof

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