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 
|- ( ph -> A e. Fin )
phpeqd.2 
|- ( ph -> B C_ A )
phpeqd.3 
|- ( ph -> A ~~ B )
Assertion phpeqd 
|- ( ph -> A = B )

Proof

Step Hyp Ref Expression
1 phpeqd.1 
 |-  ( ph -> A e. Fin )
2 phpeqd.2 
 |-  ( ph -> B C_ A )
3 phpeqd.3 
 |-  ( ph -> A ~~ B )
4 2 adantr 
 |-  ( ( ph /\ -. A = B ) -> B C_ A )
5 simpr 
 |-  ( ( ph /\ -. A = B ) -> -. A = B )
6 5 neqcomd 
 |-  ( ( ph /\ -. A = B ) -> -. B = A )
7 dfpss2 
 |-  ( B C. A <-> ( B C_ A /\ -. B = A ) )
8 4 6 7 sylanbrc 
 |-  ( ( ph /\ -. A = B ) -> B C. A )
9 php3 
 |-  ( ( A e. Fin /\ B C. A ) -> B ~< A )
10 1 8 9 syl2an2r 
 |-  ( ( ph /\ -. A = B ) -> B ~< A )
11 sdomnen 
 |-  ( B ~< A -> -. B ~~ A )
12 ensymfib 
 |-  ( A e. Fin -> ( A ~~ B <-> B ~~ A ) )
13 12 notbid 
 |-  ( A e. Fin -> ( -. A ~~ B <-> -. B ~~ A ) )
14 13 biimpar 
 |-  ( ( A e. Fin /\ -. B ~~ A ) -> -. A ~~ B )
15 1 11 14 syl2an 
 |-  ( ( ph /\ B ~< A ) -> -. A ~~ B )
16 10 15 syldan 
 |-  ( ( ph /\ -. A = B ) -> -. A ~~ B )
17 16 ex 
 |-  ( ph -> ( -. A = B -> -. A ~~ B ) )
18 3 17 mt4d 
 |-  ( ph -> A = B )