Metamath Proof Explorer


Theorem fphpd

Description: Pigeonhole principle expressed with implicit substitution. If the range is smaller than the domain, two inputs must be mapped to the same output. (Contributed by Stefan O'Rear, 19-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypotheses fphpd.a ( 𝜑𝐵𝐴 )
fphpd.b ( ( 𝜑𝑥𝐴 ) → 𝐶𝐵 )
fphpd.c ( 𝑥 = 𝑦𝐶 = 𝐷 )
Assertion fphpd ( 𝜑 → ∃ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦𝐶 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 fphpd.a ( 𝜑𝐵𝐴 )
2 fphpd.b ( ( 𝜑𝑥𝐴 ) → 𝐶𝐵 )
3 fphpd.c ( 𝑥 = 𝑦𝐶 = 𝐷 )
4 domnsym ( 𝐴𝐵 → ¬ 𝐵𝐴 )
5 4 1 nsyl3 ( 𝜑 → ¬ 𝐴𝐵 )
6 relsdom Rel ≺
7 6 brrelex1i ( 𝐵𝐴𝐵 ∈ V )
8 1 7 syl ( 𝜑𝐵 ∈ V )
9 8 adantr ( ( 𝜑 ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝐶 = 𝐷𝑥 = 𝑦 ) ) → 𝐵 ∈ V )
10 nfv 𝑥 ( 𝜑𝑎𝐴 )
11 nfcsb1v 𝑥 𝑎 / 𝑥 𝐶
12 11 nfel1 𝑥 𝑎 / 𝑥 𝐶𝐵
13 10 12 nfim 𝑥 ( ( 𝜑𝑎𝐴 ) → 𝑎 / 𝑥 𝐶𝐵 )
14 eleq1w ( 𝑥 = 𝑎 → ( 𝑥𝐴𝑎𝐴 ) )
15 14 anbi2d ( 𝑥 = 𝑎 → ( ( 𝜑𝑥𝐴 ) ↔ ( 𝜑𝑎𝐴 ) ) )
16 csbeq1a ( 𝑥 = 𝑎𝐶 = 𝑎 / 𝑥 𝐶 )
17 16 eleq1d ( 𝑥 = 𝑎 → ( 𝐶𝐵 𝑎 / 𝑥 𝐶𝐵 ) )
18 15 17 imbi12d ( 𝑥 = 𝑎 → ( ( ( 𝜑𝑥𝐴 ) → 𝐶𝐵 ) ↔ ( ( 𝜑𝑎𝐴 ) → 𝑎 / 𝑥 𝐶𝐵 ) ) )
19 13 18 2 chvarfv ( ( 𝜑𝑎𝐴 ) → 𝑎 / 𝑥 𝐶𝐵 )
20 19 ex ( 𝜑 → ( 𝑎𝐴 𝑎 / 𝑥 𝐶𝐵 ) )
21 20 adantr ( ( 𝜑 ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝐶 = 𝐷𝑥 = 𝑦 ) ) → ( 𝑎𝐴 𝑎 / 𝑥 𝐶𝐵 ) )
22 csbid 𝑥 / 𝑥 𝐶 = 𝐶
23 vex 𝑦 ∈ V
24 23 3 csbie 𝑦 / 𝑥 𝐶 = 𝐷
25 22 24 eqeq12i ( 𝑥 / 𝑥 𝐶 = 𝑦 / 𝑥 𝐶𝐶 = 𝐷 )
26 25 imbi1i ( ( 𝑥 / 𝑥 𝐶 = 𝑦 / 𝑥 𝐶𝑥 = 𝑦 ) ↔ ( 𝐶 = 𝐷𝑥 = 𝑦 ) )
27 26 2ralbii ( ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 / 𝑥 𝐶 = 𝑦 / 𝑥 𝐶𝑥 = 𝑦 ) ↔ ∀ 𝑥𝐴𝑦𝐴 ( 𝐶 = 𝐷𝑥 = 𝑦 ) )
28 nfcsb1v 𝑥 𝑦 / 𝑥 𝐶
29 11 28 nfeq 𝑥 𝑎 / 𝑥 𝐶 = 𝑦 / 𝑥 𝐶
30 nfv 𝑥 𝑎 = 𝑦
31 29 30 nfim 𝑥 ( 𝑎 / 𝑥 𝐶 = 𝑦 / 𝑥 𝐶𝑎 = 𝑦 )
32 nfv 𝑦 ( 𝑎 / 𝑥 𝐶 = 𝑏 / 𝑥 𝐶𝑎 = 𝑏 )
33 csbeq1 ( 𝑥 = 𝑎 𝑥 / 𝑥 𝐶 = 𝑎 / 𝑥 𝐶 )
34 33 eqeq1d ( 𝑥 = 𝑎 → ( 𝑥 / 𝑥 𝐶 = 𝑦 / 𝑥 𝐶 𝑎 / 𝑥 𝐶 = 𝑦 / 𝑥 𝐶 ) )
35 equequ1 ( 𝑥 = 𝑎 → ( 𝑥 = 𝑦𝑎 = 𝑦 ) )
36 34 35 imbi12d ( 𝑥 = 𝑎 → ( ( 𝑥 / 𝑥 𝐶 = 𝑦 / 𝑥 𝐶𝑥 = 𝑦 ) ↔ ( 𝑎 / 𝑥 𝐶 = 𝑦 / 𝑥 𝐶𝑎 = 𝑦 ) ) )
37 csbeq1 ( 𝑦 = 𝑏 𝑦 / 𝑥 𝐶 = 𝑏 / 𝑥 𝐶 )
38 37 eqeq2d ( 𝑦 = 𝑏 → ( 𝑎 / 𝑥 𝐶 = 𝑦 / 𝑥 𝐶 𝑎 / 𝑥 𝐶 = 𝑏 / 𝑥 𝐶 ) )
39 equequ2 ( 𝑦 = 𝑏 → ( 𝑎 = 𝑦𝑎 = 𝑏 ) )
40 38 39 imbi12d ( 𝑦 = 𝑏 → ( ( 𝑎 / 𝑥 𝐶 = 𝑦 / 𝑥 𝐶𝑎 = 𝑦 ) ↔ ( 𝑎 / 𝑥 𝐶 = 𝑏 / 𝑥 𝐶𝑎 = 𝑏 ) ) )
41 31 32 36 40 rspc2 ( ( 𝑎𝐴𝑏𝐴 ) → ( ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 / 𝑥 𝐶 = 𝑦 / 𝑥 𝐶𝑥 = 𝑦 ) → ( 𝑎 / 𝑥 𝐶 = 𝑏 / 𝑥 𝐶𝑎 = 𝑏 ) ) )
42 41 com12 ( ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 / 𝑥 𝐶 = 𝑦 / 𝑥 𝐶𝑥 = 𝑦 ) → ( ( 𝑎𝐴𝑏𝐴 ) → ( 𝑎 / 𝑥 𝐶 = 𝑏 / 𝑥 𝐶𝑎 = 𝑏 ) ) )
43 27 42 sylbir ( ∀ 𝑥𝐴𝑦𝐴 ( 𝐶 = 𝐷𝑥 = 𝑦 ) → ( ( 𝑎𝐴𝑏𝐴 ) → ( 𝑎 / 𝑥 𝐶 = 𝑏 / 𝑥 𝐶𝑎 = 𝑏 ) ) )
44 id ( ( 𝑎 / 𝑥 𝐶 = 𝑏 / 𝑥 𝐶𝑎 = 𝑏 ) → ( 𝑎 / 𝑥 𝐶 = 𝑏 / 𝑥 𝐶𝑎 = 𝑏 ) )
45 csbeq1 ( 𝑎 = 𝑏 𝑎 / 𝑥 𝐶 = 𝑏 / 𝑥 𝐶 )
46 44 45 impbid1 ( ( 𝑎 / 𝑥 𝐶 = 𝑏 / 𝑥 𝐶𝑎 = 𝑏 ) → ( 𝑎 / 𝑥 𝐶 = 𝑏 / 𝑥 𝐶𝑎 = 𝑏 ) )
47 43 46 syl6 ( ∀ 𝑥𝐴𝑦𝐴 ( 𝐶 = 𝐷𝑥 = 𝑦 ) → ( ( 𝑎𝐴𝑏𝐴 ) → ( 𝑎 / 𝑥 𝐶 = 𝑏 / 𝑥 𝐶𝑎 = 𝑏 ) ) )
48 47 adantl ( ( 𝜑 ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝐶 = 𝐷𝑥 = 𝑦 ) ) → ( ( 𝑎𝐴𝑏𝐴 ) → ( 𝑎 / 𝑥 𝐶 = 𝑏 / 𝑥 𝐶𝑎 = 𝑏 ) ) )
49 21 48 dom2d ( ( 𝜑 ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝐶 = 𝐷𝑥 = 𝑦 ) ) → ( 𝐵 ∈ V → 𝐴𝐵 ) )
50 9 49 mpd ( ( 𝜑 ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝐶 = 𝐷𝑥 = 𝑦 ) ) → 𝐴𝐵 )
51 5 50 mtand ( 𝜑 → ¬ ∀ 𝑥𝐴𝑦𝐴 ( 𝐶 = 𝐷𝑥 = 𝑦 ) )
52 ancom ( ( ¬ 𝑥 = 𝑦𝐶 = 𝐷 ) ↔ ( 𝐶 = 𝐷 ∧ ¬ 𝑥 = 𝑦 ) )
53 df-ne ( 𝑥𝑦 ↔ ¬ 𝑥 = 𝑦 )
54 53 anbi1i ( ( 𝑥𝑦𝐶 = 𝐷 ) ↔ ( ¬ 𝑥 = 𝑦𝐶 = 𝐷 ) )
55 pm4.61 ( ¬ ( 𝐶 = 𝐷𝑥 = 𝑦 ) ↔ ( 𝐶 = 𝐷 ∧ ¬ 𝑥 = 𝑦 ) )
56 52 54 55 3bitr4i ( ( 𝑥𝑦𝐶 = 𝐷 ) ↔ ¬ ( 𝐶 = 𝐷𝑥 = 𝑦 ) )
57 56 rexbii ( ∃ 𝑦𝐴 ( 𝑥𝑦𝐶 = 𝐷 ) ↔ ∃ 𝑦𝐴 ¬ ( 𝐶 = 𝐷𝑥 = 𝑦 ) )
58 rexnal ( ∃ 𝑦𝐴 ¬ ( 𝐶 = 𝐷𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑦𝐴 ( 𝐶 = 𝐷𝑥 = 𝑦 ) )
59 57 58 bitri ( ∃ 𝑦𝐴 ( 𝑥𝑦𝐶 = 𝐷 ) ↔ ¬ ∀ 𝑦𝐴 ( 𝐶 = 𝐷𝑥 = 𝑦 ) )
60 59 rexbii ( ∃ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦𝐶 = 𝐷 ) ↔ ∃ 𝑥𝐴 ¬ ∀ 𝑦𝐴 ( 𝐶 = 𝐷𝑥 = 𝑦 ) )
61 rexnal ( ∃ 𝑥𝐴 ¬ ∀ 𝑦𝐴 ( 𝐶 = 𝐷𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑥𝐴𝑦𝐴 ( 𝐶 = 𝐷𝑥 = 𝑦 ) )
62 60 61 bitri ( ∃ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦𝐶 = 𝐷 ) ↔ ¬ ∀ 𝑥𝐴𝑦𝐴 ( 𝐶 = 𝐷𝑥 = 𝑦 ) )
63 51 62 sylibr ( 𝜑 → ∃ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦𝐶 = 𝐷 ) )