Step | Hyp | Ref
| Expression |
1 | | fphpdo.3 |
. . 3
⊢ (𝜑 → 𝐵 ≺ 𝐴) |
2 | | fphpdo.4 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐶 ∈ 𝐵) |
3 | 2 | fmpttd 6932 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ 𝐶):𝐴⟶𝐵) |
4 | 3 | ffvelrnda 6904 |
. . 3
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) ∈ 𝐵) |
5 | | fveq2 6717 |
. . 3
⊢ (𝑏 = 𝑐 → ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) |
6 | 1, 4, 5 | fphpd 40341 |
. 2
⊢ (𝜑 → ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ 𝐴 (𝑏 ≠ 𝑐 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐))) |
7 | | fphpdo.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
8 | 7 | sselda 3901 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ ℝ) |
9 | 8 | adantrr 717 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → 𝑏 ∈ ℝ) |
10 | 9 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) → 𝑏 ∈ ℝ) |
11 | 7 | sselda 3901 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ ℝ) |
12 | 11 | adantrl 716 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → 𝑐 ∈ ℝ) |
13 | 12 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) → 𝑐 ∈ ℝ) |
14 | 10, 13 | lttri2d 10971 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) → (𝑏 ≠ 𝑐 ↔ (𝑏 < 𝑐 ∨ 𝑐 < 𝑏))) |
15 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → 𝑏 ∈ 𝐴) |
16 | 15 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) ∧ 𝑏 < 𝑐) → 𝑏 ∈ 𝐴) |
17 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → 𝑐 ∈ 𝐴) |
18 | 17 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) ∧ 𝑏 < 𝑐) → 𝑐 ∈ 𝐴) |
19 | | simpr 488 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) ∧ 𝑏 < 𝑐) → 𝑏 < 𝑐) |
20 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) ∧ 𝑏 < 𝑐) → ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) |
21 | | breq1 5056 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑏 → (𝑥 < 𝑦 ↔ 𝑏 < 𝑦)) |
22 | | fveqeq2 6726 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑏 → (((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦) ↔ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦))) |
23 | 21, 22 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑏 → ((𝑥 < 𝑦 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦)) ↔ (𝑏 < 𝑦 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦)))) |
24 | | breq2 5057 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑐 → (𝑏 < 𝑦 ↔ 𝑏 < 𝑐)) |
25 | | fveq2 6717 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑐 → ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) |
26 | 25 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑐 → (((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦) ↔ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐))) |
27 | 24, 26 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑐 → ((𝑏 < 𝑦 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦)) ↔ (𝑏 < 𝑐 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)))) |
28 | 23, 27 | rspc2ev 3549 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ (𝑏 < 𝑐 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐))) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦))) |
29 | 16, 18, 19, 20, 28 | syl112anc 1376 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) ∧ 𝑏 < 𝑐) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦))) |
30 | 29 | ex 416 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) → (𝑏 < 𝑐 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦)))) |
31 | 17 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) ∧ 𝑐 < 𝑏) → 𝑐 ∈ 𝐴) |
32 | 15 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) ∧ 𝑐 < 𝑏) → 𝑏 ∈ 𝐴) |
33 | | simpr 488 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) ∧ 𝑐 < 𝑏) → 𝑐 < 𝑏) |
34 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) ∧ 𝑐 < 𝑏) → ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) |
35 | 34 | eqcomd 2743 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) ∧ 𝑐 < 𝑏) → ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏)) |
36 | | breq1 5056 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑐 → (𝑥 < 𝑦 ↔ 𝑐 < 𝑦)) |
37 | | fveqeq2 6726 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑐 → (((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦) ↔ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦))) |
38 | 36, 37 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑐 → ((𝑥 < 𝑦 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦)) ↔ (𝑐 < 𝑦 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦)))) |
39 | | breq2 5057 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑏 → (𝑐 < 𝑦 ↔ 𝑐 < 𝑏)) |
40 | | fveq2 6717 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑏 → ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏)) |
41 | 40 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑏 → (((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦) ↔ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏))) |
42 | 39, 41 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑏 → ((𝑐 < 𝑦 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦)) ↔ (𝑐 < 𝑏 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏)))) |
43 | 38, 42 | rspc2ev 3549 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ (𝑐 < 𝑏 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏))) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦))) |
44 | 31, 32, 33, 35, 43 | syl112anc 1376 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) ∧ 𝑐 < 𝑏) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦))) |
45 | 44 | ex 416 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) → (𝑐 < 𝑏 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦)))) |
46 | 30, 45 | jaod 859 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) → ((𝑏 < 𝑐 ∨ 𝑐 < 𝑏) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦)))) |
47 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝐴 ↦ 𝐶) = (𝑧 ∈ 𝐴 ↦ 𝐶) |
48 | | fphpdo.5 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → 𝐶 = 𝐷) |
49 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
50 | | eleq1w 2820 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)) |
51 | 50 | anbi2d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑥 → ((𝜑 ∧ 𝑧 ∈ 𝐴) ↔ (𝜑 ∧ 𝑥 ∈ 𝐴))) |
52 | 48 | eleq1d 2822 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑥 → (𝐶 ∈ 𝐵 ↔ 𝐷 ∈ 𝐵)) |
53 | 51, 52 | imbi12d 348 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑥 → (((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐶 ∈ 𝐵) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐵))) |
54 | 53, 2 | chvarvv 2007 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐵) |
55 | 54 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝐷 ∈ 𝐵) |
56 | 47, 48, 49, 55 | fvmptd3 6841 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = 𝐷) |
57 | | fphpdo.6 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑦 → 𝐶 = 𝐸) |
58 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
59 | | eleq1w 2820 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
60 | 59 | anbi2d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑦 → ((𝜑 ∧ 𝑧 ∈ 𝐴) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴))) |
61 | 57 | eleq1d 2822 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑦 → (𝐶 ∈ 𝐵 ↔ 𝐸 ∈ 𝐵)) |
62 | 60, 61 | imbi12d 348 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑦 → (((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐶 ∈ 𝐵) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐸 ∈ 𝐵))) |
63 | 62, 2 | chvarvv 2007 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐸 ∈ 𝐵) |
64 | 63 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝐸 ∈ 𝐵) |
65 | 47, 57, 58, 64 | fvmptd3 6841 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦) = 𝐸) |
66 | 56, 65 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦) ↔ 𝐷 = 𝐸)) |
67 | 66 | biimpd 232 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦) → 𝐷 = 𝐸)) |
68 | 67 | anim2d 615 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ((𝑥 < 𝑦 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦)) → (𝑥 < 𝑦 ∧ 𝐷 = 𝐸))) |
69 | 68 | reximdva 3193 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦)) → ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ 𝐷 = 𝐸))) |
70 | 69 | reximdva 3193 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ 𝐷 = 𝐸))) |
71 | 70 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑦)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ 𝐷 = 𝐸))) |
72 | 46, 71 | syld 47 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) → ((𝑏 < 𝑐 ∨ 𝑐 < 𝑏) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ 𝐷 = 𝐸))) |
73 | 14, 72 | sylbid 243 |
. . . . 5
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) → (𝑏 ≠ 𝑐 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ 𝐷 = 𝐸))) |
74 | 73 | expimpd 457 |
. . . 4
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → ((((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐) ∧ 𝑏 ≠ 𝑐) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ 𝐷 = 𝐸))) |
75 | 74 | ancomsd 469 |
. . 3
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → ((𝑏 ≠ 𝑐 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ 𝐷 = 𝐸))) |
76 | 75 | rexlimdvva 3213 |
. 2
⊢ (𝜑 → (∃𝑏 ∈ 𝐴 ∃𝑐 ∈ 𝐴 (𝑏 ≠ 𝑐 ∧ ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑏) = ((𝑧 ∈ 𝐴 ↦ 𝐶)‘𝑐)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ 𝐷 = 𝐸))) |
77 | 6, 76 | mpd 15 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ 𝐷 = 𝐸)) |