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 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 ∧ 𝐶 = 𝐷 ) )