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

Metamath Proof Explorer

Theorem phpeqd

Description: Corollary of the Pigeonhole Principle using equality. Strengthening of php expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023) Avoid ax-pow . (Revised by BTernaryTau, 28-Nov-2024)

Ref Expression
Hypotheses phpeqd.1 ⊢ φ → A ∈ Fin
phpeqd.2 ⊢ φ → B ⊆ A
phpeqd.3 ⊢ φ → A ≈ B
Assertion phpeqd ⊢ φ → A = B

Proof

Step Hyp Ref Expression
1 phpeqd.1 ⊢ φ → A ∈ Fin
2 phpeqd.2 ⊢ φ → B ⊆ A
3 phpeqd.3 ⊢ φ → A ≈ B
4 2 adantr ⊢ φ ∧ ¬ A = B → B ⊆ A
5 simpr ⊢ φ ∧ ¬ A = B → ¬ A = B
6 5 neqcomd ⊢ φ ∧ ¬ A = B → ¬ B = A
7 dfpss2 ⊢ B ⊂ A ↔ B ⊆ A ∧ ¬ B = A
8 4 6 7 sylanbrc ⊢ φ ∧ ¬ A = B → B ⊂ A
9 php3 ⊢ A ∈ Fin ∧ B ⊂ A → B ≺ A
10 1 8 9 syl2an2r ⊢ φ ∧ ¬ A = B → B ≺ A
11 sdomnen ⊢ B ≺ A → ¬ B ≈ A
12 ensymfib ⊢ A ∈ Fin → A ≈ B ↔ B ≈ A
13 12 notbid ⊢ A ∈ Fin → ¬ A ≈ B ↔ ¬ B ≈ A
14 13 biimpar ⊢ A ∈ Fin ∧ ¬ B ≈ A → ¬ A ≈ B
15 1 11 14 syl2an ⊢ φ ∧ B ≺ A → ¬ A ≈ B
16 10 15 syldan ⊢ φ ∧ ¬ A = B → ¬ A ≈ B
17 16 ex ⊢ φ → ¬ A = B → ¬ A ≈ B
18 3 17 mt4d ⊢ φ → A = B