| Step | Hyp | Ref
| Expression |
| 1 | | unxpwdom3.dv |
. . 3
⊢ (𝜑 → 𝐷 ∈ 𝑋) |
| 2 | | unxpwdom3.bv |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
| 3 | 1, 2 | xpexd 7771 |
. 2
⊢ (𝜑 → (𝐷 × 𝐵) ∈ V) |
| 4 | | simprr 773 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → (𝑎 + 𝑑) ∈ 𝐵) |
| 5 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → 𝑎 ∈ 𝐶) |
| 6 | | unxpwdom3.rc |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ (𝑎 ∈ 𝐶 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎)) |
| 7 | 6 | an4s 660 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎)) |
| 8 | 7 | anassrs 467 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑑 ∈ 𝐷) ∧ 𝑐 ∈ 𝐶) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎)) |
| 9 | 8 | adantlrr 721 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) ∧ 𝑐 ∈ 𝐶) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎)) |
| 10 | 5, 9 | riota5 7417 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑)) = 𝑎) |
| 11 | 10 | eqcomd 2743 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑))) |
| 12 | | eqeq2 2749 |
. . . . . . 7
⊢ (𝑦 = (𝑎 + 𝑑) → ((𝑐 + 𝑑) = 𝑦 ↔ (𝑐 + 𝑑) = (𝑎 + 𝑑))) |
| 13 | 12 | riotabidv 7390 |
. . . . . 6
⊢ (𝑦 = (𝑎 + 𝑑) → (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦) = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑))) |
| 14 | 13 | rspceeqv 3645 |
. . . . 5
⊢ (((𝑎 + 𝑑) ∈ 𝐵 ∧ 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑))) → ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦)) |
| 15 | 4, 11, 14 | syl2anc 584 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦)) |
| 16 | | unxpwdom3.ni |
. . . . . . 7
⊢ (𝜑 → ¬ 𝐷 ≼ 𝐴) |
| 17 | 16 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ¬ 𝐷 ≼ 𝐴) |
| 18 | | unxpwdom3.av |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 19 | 18 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → 𝐴 ∈ 𝑉) |
| 20 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 𝑏 → (𝑎 + 𝑑) = (𝑎 + 𝑏)) |
| 21 | 20 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑏 → ((𝑎 + 𝑑) ∈ 𝐵 ↔ (𝑎 + 𝑏) ∈ 𝐵)) |
| 22 | 21 | notbid 318 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝑏 → (¬ (𝑎 + 𝑑) ∈ 𝐵 ↔ ¬ (𝑎 + 𝑏) ∈ 𝐵)) |
| 23 | 22 | rspcv 3618 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ 𝐷 → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → ¬ (𝑎 + 𝑏) ∈ 𝐵)) |
| 24 | 23 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → ¬ (𝑎 + 𝑏) ∈ 𝐵)) |
| 25 | | unxpwdom3.ov |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵)) |
| 26 | 25 | 3expa 1119 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵)) |
| 27 | | elun 4153 |
. . . . . . . . . . . . 13
⊢ ((𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵) ↔ ((𝑎 + 𝑏) ∈ 𝐴 ∨ (𝑎 + 𝑏) ∈ 𝐵)) |
| 28 | 26, 27 | sylib 218 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → ((𝑎 + 𝑏) ∈ 𝐴 ∨ (𝑎 + 𝑏) ∈ 𝐵)) |
| 29 | 28 | orcomd 872 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → ((𝑎 + 𝑏) ∈ 𝐵 ∨ (𝑎 + 𝑏) ∈ 𝐴)) |
| 30 | 29 | ord 865 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (¬ (𝑎 + 𝑏) ∈ 𝐵 → (𝑎 + 𝑏) ∈ 𝐴)) |
| 31 | 24, 30 | syld 47 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → (𝑎 + 𝑏) ∈ 𝐴)) |
| 32 | 31 | impancom 451 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → (𝑏 ∈ 𝐷 → (𝑎 + 𝑏) ∈ 𝐴)) |
| 33 | | unxpwdom3.lc |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐)) |
| 34 | 33 | ex 412 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ((𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐))) |
| 35 | 34 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → ((𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐))) |
| 36 | 32, 35 | dom2d 9033 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → (𝐴 ∈ 𝑉 → 𝐷 ≼ 𝐴)) |
| 37 | 19, 36 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → 𝐷 ≼ 𝐴) |
| 38 | 17, 37 | mtand 816 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ¬ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) |
| 39 | | dfrex2 3073 |
. . . . 5
⊢
(∃𝑑 ∈
𝐷 (𝑎 + 𝑑) ∈ 𝐵 ↔ ¬ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) |
| 40 | 38, 39 | sylibr 234 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑑 ∈ 𝐷 (𝑎 + 𝑑) ∈ 𝐵) |
| 41 | 15, 40 | reximddv 3171 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑑 ∈ 𝐷 ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦)) |
| 42 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑑 ∈ V |
| 43 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
| 44 | 42, 43 | op1std 8024 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑑, 𝑦〉 → (1st ‘𝑥) = 𝑑) |
| 45 | 44 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑥 = 〈𝑑, 𝑦〉 → (𝑐 + (1st
‘𝑥)) = (𝑐 + 𝑑)) |
| 46 | 42, 43 | op2ndd 8025 |
. . . . . . 7
⊢ (𝑥 = 〈𝑑, 𝑦〉 → (2nd ‘𝑥) = 𝑦) |
| 47 | 45, 46 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑥 = 〈𝑑, 𝑦〉 → ((𝑐 + (1st
‘𝑥)) =
(2nd ‘𝑥)
↔ (𝑐 + 𝑑) = 𝑦)) |
| 48 | 47 | riotabidv 7390 |
. . . . 5
⊢ (𝑥 = 〈𝑑, 𝑦〉 → (℩𝑐 ∈ 𝐶 (𝑐 + (1st
‘𝑥)) =
(2nd ‘𝑥))
= (℩𝑐 ∈
𝐶 (𝑐 + 𝑑) = 𝑦)) |
| 49 | 48 | eqeq2d 2748 |
. . . 4
⊢ (𝑥 = 〈𝑑, 𝑦〉 → (𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st
‘𝑥)) =
(2nd ‘𝑥))
↔ 𝑎 =
(℩𝑐 ∈
𝐶 (𝑐 + 𝑑) = 𝑦))) |
| 50 | 49 | rexxp 5853 |
. . 3
⊢
(∃𝑥 ∈
(𝐷 × 𝐵)𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st
‘𝑥)) =
(2nd ‘𝑥))
↔ ∃𝑑 ∈
𝐷 ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦)) |
| 51 | 41, 50 | sylibr 234 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑥 ∈ (𝐷 × 𝐵)𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st
‘𝑥)) =
(2nd ‘𝑥))) |
| 52 | 3, 51 | wdomd 9621 |
1
⊢ (𝜑 → 𝐶 ≼* (𝐷 × 𝐵)) |