Metamath Proof Explorer

Theorem fphpdo

Description: Pigeonhole principle for sets of real numbers with implicit output reordering. (Contributed by Stefan O'Rear, 12-Sep-2014)

Ref Expression
Hypotheses fphpdo.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
fphpdo.2 ⊢ ( 𝜑 → 𝐵 ∈ V )
fphpdo.3 ⊢ ( 𝜑 → 𝐵 ≺ 𝐴 )
fphpdo.4 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
fphpdo.5 ⊢ ( 𝑧 = 𝑥 → 𝐶 = 𝐷 )
fphpdo.6 ⊢ ( 𝑧 = 𝑦 → 𝐶 = 𝐸 )
Assertion fphpdo ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ 𝐷 = 𝐸 ) )

Proof

Step Hyp Ref Expression
1 fphpdo.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 fphpdo.2 ⊢ ( 𝜑 → 𝐵 ∈ V )
3 fphpdo.3 ⊢ ( 𝜑 → 𝐵 ≺ 𝐴 )
4 fphpdo.4 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
5 fphpdo.5 ⊢ ( 𝑧 = 𝑥 → 𝐶 = 𝐷 )
6 fphpdo.6 ⊢ ( 𝑧 = 𝑦 → 𝐶 = 𝐸 )
7 4 fmpttd ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ 𝐵 )
8 7 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) ∈ 𝐵 )
9 fveq2 ⊢ ( 𝑏 = 𝑐 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) )
10 3 8 9 fphpd ⊢ ( 𝜑 → ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑏 ≠ 𝑐 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) )
11 1 sselda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → 𝑏 ∈ ℝ )
12 11 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) → 𝑏 ∈ ℝ )
13 12 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) → 𝑏 ∈ ℝ )
14 1 sselda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝑐 ∈ ℝ )
15 14 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) → 𝑐 ∈ ℝ )
16 15 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) → 𝑐 ∈ ℝ )
17 13 16 lttri2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) → ( 𝑏 ≠ 𝑐 ↔ ( 𝑏 < 𝑐 ∨ 𝑐 < 𝑏 ) ) )
18 simprl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) → 𝑏 ∈ 𝐴 )
19 18 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) ∧ 𝑏 < 𝑐 ) → 𝑏 ∈ 𝐴 )
20 simprr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) → 𝑐 ∈ 𝐴 )
21 20 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) ∧ 𝑏 < 𝑐 ) → 𝑐 ∈ 𝐴 )
22 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) ∧ 𝑏 < 𝑐 ) → 𝑏 < 𝑐 )
23 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) ∧ 𝑏 < 𝑐 ) → ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) )
24 breq1 ⊢ ( 𝑥 = 𝑏 → ( 𝑥 < 𝑦 ↔ 𝑏 < 𝑦 ) )
25 fveqeq2 ⊢ ( 𝑥 = 𝑏 → ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ↔ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) )
26 24 25 anbi12d ⊢ ( 𝑥 = 𝑏 → ( ( 𝑥 < 𝑦 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ↔ ( 𝑏 < 𝑦 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ) )
27 breq2 ⊢ ( 𝑦 = 𝑐 → ( 𝑏 < 𝑦 ↔ 𝑏 < 𝑐 ) )
28 fveq2 ⊢ ( 𝑦 = 𝑐 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) )
29 28 eqeq2d ⊢ ( 𝑦 = 𝑐 → ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ↔ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) )
30 27 29 anbi12d ⊢ ( 𝑦 = 𝑐 → ( ( 𝑏 < 𝑦 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ↔ ( 𝑏 < 𝑐 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) ) )
31 26 30 rspc2ev ⊢ ( ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ ( 𝑏 < 𝑐 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) )
32 19 21 22 23 31 syl112anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) ∧ 𝑏 < 𝑐 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) )
33 32 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) → ( 𝑏 < 𝑐 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ) )
34 20 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) ∧ 𝑐 < 𝑏 ) → 𝑐 ∈ 𝐴 )
35 18 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) ∧ 𝑐 < 𝑏 ) → 𝑏 ∈ 𝐴 )
36 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) ∧ 𝑐 < 𝑏 ) → 𝑐 < 𝑏 )
37 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) ∧ 𝑐 < 𝑏 ) → ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) )
38 37 eqcomd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) ∧ 𝑐 < 𝑏 ) → ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) )
39 breq1 ⊢ ( 𝑥 = 𝑐 → ( 𝑥 < 𝑦 ↔ 𝑐 < 𝑦 ) )
40 fveqeq2 ⊢ ( 𝑥 = 𝑐 → ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ↔ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) )
41 39 40 anbi12d ⊢ ( 𝑥 = 𝑐 → ( ( 𝑥 < 𝑦 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ↔ ( 𝑐 < 𝑦 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ) )
42 breq2 ⊢ ( 𝑦 = 𝑏 → ( 𝑐 < 𝑦 ↔ 𝑐 < 𝑏 ) )
43 fveq2 ⊢ ( 𝑦 = 𝑏 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) )
44 43 eqeq2d ⊢ ( 𝑦 = 𝑏 → ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ↔ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) ) )
45 42 44 anbi12d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑐 < 𝑦 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ↔ ( 𝑐 < 𝑏 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) ) ) )
46 41 45 rspc2ev ⊢ ( ( 𝑐 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ ( 𝑐 < 𝑏 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) )
47 34 35 36 38 46 syl112anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) ∧ 𝑐 < 𝑏 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) )
48 47 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) → ( 𝑐 < 𝑏 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ) )
49 33 48 jaod ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) → ( ( 𝑏 < 𝑐 ∨ 𝑐 < 𝑏 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ) )
50 eqid ⊢ ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑧 ∈ 𝐴 ↦ 𝐶 )
51 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
52 eleq1w ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
53 52 anbi2d ⊢ ( 𝑧 = 𝑥 → ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ) )
54 5 eleq1d ⊢ ( 𝑧 = 𝑥 → ( 𝐶 ∈ 𝐵 ↔ 𝐷 ∈ 𝐵 ) )
55 53 54 imbi12d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝐵 ) ) )
56 55 4 chvarvv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝐵 )
57 56 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝐷 ∈ 𝐵 )
58 50 5 51 57 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐷 )
59 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
60 eleq1w ⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
61 60 anbi2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ) )
62 6 eleq1d ⊢ ( 𝑧 = 𝑦 → ( 𝐶 ∈ 𝐵 ↔ 𝐸 ∈ 𝐵 ) )
63 61 62 imbi12d ⊢ ( 𝑧 = 𝑦 → ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐸 ∈ 𝐵 ) ) )
64 63 4 chvarvv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐸 ∈ 𝐵 )
65 64 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝐸 ∈ 𝐵 )
66 50 6 59 65 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐸 )
67 58 66 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ↔ 𝐷 = 𝐸 ) )
68 67 biimpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) → 𝐷 = 𝐸 ) )
69 68 anim2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 < 𝑦 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) → ( 𝑥 < 𝑦 ∧ 𝐷 = 𝐸 ) ) )
70 69 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) → ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ 𝐷 = 𝐸 ) ) )
71 70 reximdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ 𝐷 = 𝐸 ) ) )
72 71 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ 𝐷 = 𝐸 ) ) )
73 49 72 syld ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) → ( ( 𝑏 < 𝑐 ∨ 𝑐 < 𝑏 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ 𝐷 = 𝐸 ) ) )
74 17 73 sylbid ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) → ( 𝑏 ≠ 𝑐 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ 𝐷 = 𝐸 ) ) )
75 74 expimpd ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) → ( ( ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ∧ 𝑏 ≠ 𝑐 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ 𝐷 = 𝐸 ) ) )
76 75 ancomsd ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) → ( ( 𝑏 ≠ 𝑐 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ 𝐷 = 𝐸 ) ) )
77 76 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑏 ≠ 𝑐 ∧ ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑏 ) = ( ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑐 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ 𝐷 = 𝐸 ) ) )
78 10 77 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 < 𝑦 ∧ 𝐷 = 𝐸 ) )