Step | Hyp | Ref
| Expression |
1 | | unxpwdom3.dv |
. . 3
⊢ (𝜑 → 𝐷 ∈ 𝑋) |
2 | | unxpwdom3.bv |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
3 | 1, 2 | xpexd 7601 |
. 2
⊢ (𝜑 → (𝐷 × 𝐵) ∈ V) |
4 | | simprr 770 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → (𝑎 + 𝑑) ∈ 𝐵) |
5 | | simplr 766 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → 𝑎 ∈ 𝐶) |
6 | | unxpwdom3.rc |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ (𝑎 ∈ 𝐶 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎)) |
7 | 6 | an4s 657 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎)) |
8 | 7 | anassrs 468 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑑 ∈ 𝐷) ∧ 𝑐 ∈ 𝐶) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎)) |
9 | 8 | adantlrr 718 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) ∧ 𝑐 ∈ 𝐶) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎)) |
10 | 5, 9 | riota5 7262 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑)) = 𝑎) |
11 | 10 | eqcomd 2744 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑))) |
12 | | eqeq2 2750 |
. . . . . . 7
⊢ (𝑦 = (𝑎 + 𝑑) → ((𝑐 + 𝑑) = 𝑦 ↔ (𝑐 + 𝑑) = (𝑎 + 𝑑))) |
13 | 12 | riotabidv 7234 |
. . . . . 6
⊢ (𝑦 = (𝑎 + 𝑑) → (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦) = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑))) |
14 | 13 | rspceeqv 3575 |
. . . . 5
⊢ (((𝑎 + 𝑑) ∈ 𝐵 ∧ 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑))) → ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦)) |
15 | 4, 11, 14 | syl2anc 584 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦)) |
16 | | unxpwdom3.ni |
. . . . . . 7
⊢ (𝜑 → ¬ 𝐷 ≼ 𝐴) |
17 | 16 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ¬ 𝐷 ≼ 𝐴) |
18 | | unxpwdom3.av |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
19 | 18 | ad2antrr 723 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → 𝐴 ∈ 𝑉) |
20 | | oveq2 7283 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 𝑏 → (𝑎 + 𝑑) = (𝑎 + 𝑏)) |
21 | 20 | eleq1d 2823 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑏 → ((𝑎 + 𝑑) ∈ 𝐵 ↔ (𝑎 + 𝑏) ∈ 𝐵)) |
22 | 21 | notbid 318 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝑏 → (¬ (𝑎 + 𝑑) ∈ 𝐵 ↔ ¬ (𝑎 + 𝑏) ∈ 𝐵)) |
23 | 22 | rspcv 3557 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ 𝐷 → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → ¬ (𝑎 + 𝑏) ∈ 𝐵)) |
24 | 23 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → ¬ (𝑎 + 𝑏) ∈ 𝐵)) |
25 | | unxpwdom3.ov |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵)) |
26 | 25 | 3expa 1117 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵)) |
27 | | elun 4083 |
. . . . . . . . . . . . 13
⊢ ((𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵) ↔ ((𝑎 + 𝑏) ∈ 𝐴 ∨ (𝑎 + 𝑏) ∈ 𝐵)) |
28 | 26, 27 | sylib 217 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → ((𝑎 + 𝑏) ∈ 𝐴 ∨ (𝑎 + 𝑏) ∈ 𝐵)) |
29 | 28 | orcomd 868 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → ((𝑎 + 𝑏) ∈ 𝐵 ∨ (𝑎 + 𝑏) ∈ 𝐴)) |
30 | 29 | ord 861 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (¬ (𝑎 + 𝑏) ∈ 𝐵 → (𝑎 + 𝑏) ∈ 𝐴)) |
31 | 24, 30 | syld 47 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → (𝑎 + 𝑏) ∈ 𝐴)) |
32 | 31 | impancom 452 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → (𝑏 ∈ 𝐷 → (𝑎 + 𝑏) ∈ 𝐴)) |
33 | | unxpwdom3.lc |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐)) |
34 | 33 | ex 413 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ((𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐))) |
35 | 34 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → ((𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐))) |
36 | 32, 35 | dom2d 8781 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → (𝐴 ∈ 𝑉 → 𝐷 ≼ 𝐴)) |
37 | 19, 36 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → 𝐷 ≼ 𝐴) |
38 | 17, 37 | mtand 813 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ¬ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) |
39 | | dfrex2 3170 |
. . . . 5
⊢
(∃𝑑 ∈
𝐷 (𝑎 + 𝑑) ∈ 𝐵 ↔ ¬ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) |
40 | 38, 39 | sylibr 233 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑑 ∈ 𝐷 (𝑎 + 𝑑) ∈ 𝐵) |
41 | 15, 40 | reximddv 3204 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑑 ∈ 𝐷 ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦)) |
42 | | vex 3436 |
. . . . . . . . 9
⊢ 𝑑 ∈ V |
43 | | vex 3436 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
44 | 42, 43 | op1std 7841 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑑, 𝑦〉 → (1st ‘𝑥) = 𝑑) |
45 | 44 | oveq2d 7291 |
. . . . . . 7
⊢ (𝑥 = 〈𝑑, 𝑦〉 → (𝑐 + (1st
‘𝑥)) = (𝑐 + 𝑑)) |
46 | 42, 43 | op2ndd 7842 |
. . . . . . 7
⊢ (𝑥 = 〈𝑑, 𝑦〉 → (2nd ‘𝑥) = 𝑦) |
47 | 45, 46 | eqeq12d 2754 |
. . . . . 6
⊢ (𝑥 = 〈𝑑, 𝑦〉 → ((𝑐 + (1st
‘𝑥)) =
(2nd ‘𝑥)
↔ (𝑐 + 𝑑) = 𝑦)) |
48 | 47 | riotabidv 7234 |
. . . . 5
⊢ (𝑥 = 〈𝑑, 𝑦〉 → (℩𝑐 ∈ 𝐶 (𝑐 + (1st
‘𝑥)) =
(2nd ‘𝑥))
= (℩𝑐 ∈
𝐶 (𝑐 + 𝑑) = 𝑦)) |
49 | 48 | eqeq2d 2749 |
. . . 4
⊢ (𝑥 = 〈𝑑, 𝑦〉 → (𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st
‘𝑥)) =
(2nd ‘𝑥))
↔ 𝑎 =
(℩𝑐 ∈
𝐶 (𝑐 + 𝑑) = 𝑦))) |
50 | 49 | rexxp 5751 |
. . 3
⊢
(∃𝑥 ∈
(𝐷 × 𝐵)𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st
‘𝑥)) =
(2nd ‘𝑥))
↔ ∃𝑑 ∈
𝐷 ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦)) |
51 | 41, 50 | sylibr 233 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑥 ∈ (𝐷 × 𝐵)𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st
‘𝑥)) =
(2nd ‘𝑥))) |
52 | 3, 51 | wdomd 9340 |
1
⊢ (𝜑 → 𝐶 ≼* (𝐷 × 𝐵)) |