Step | Hyp | Ref
| Expression |
1 | | unxpwdom3.dv |
. . 3
⊢ (𝜑 → 𝐷 ∈ 𝑋) |
2 | | unxpwdom3.bv |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
3 | | xpexg 6960 |
. . 3
⊢ ((𝐷 ∈ 𝑋 ∧ 𝐵 ∈ 𝑊) → (𝐷 × 𝐵) ∈ V) |
4 | 1, 2, 3 | syl2anc 693 |
. 2
⊢ (𝜑 → (𝐷 × 𝐵) ∈ V) |
5 | | simprr 796 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → (𝑎 + 𝑑) ∈ 𝐵) |
6 | | simplr 792 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → 𝑎 ∈ 𝐶) |
7 | | unxpwdom3.rc |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ (𝑎 ∈ 𝐶 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎)) |
8 | 7 | an4s 869 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎)) |
9 | 8 | anassrs 680 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑑 ∈ 𝐷) ∧ 𝑐 ∈ 𝐶) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎)) |
10 | 9 | adantlrr 757 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) ∧ 𝑐 ∈ 𝐶) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎)) |
11 | 6, 10 | riota5 6637 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑)) = 𝑎) |
12 | 11 | eqcomd 2628 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑))) |
13 | | eqeq2 2633 |
. . . . . . . 8
⊢ (𝑦 = (𝑎 + 𝑑) → ((𝑐 + 𝑑) = 𝑦 ↔ (𝑐 + 𝑑) = (𝑎 + 𝑑))) |
14 | 13 | riotabidv 6613 |
. . . . . . 7
⊢ (𝑦 = (𝑎 + 𝑑) → (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦) = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑))) |
15 | 14 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑦 = (𝑎 + 𝑑) → (𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦) ↔ 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑)))) |
16 | 15 | rspcev 3309 |
. . . . 5
⊢ (((𝑎 + 𝑑) ∈ 𝐵 ∧ 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑))) → ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦)) |
17 | 5, 12, 16 | syl2anc 693 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦)) |
18 | | unxpwdom3.ni |
. . . . . . 7
⊢ (𝜑 → ¬ 𝐷 ≼ 𝐴) |
19 | 18 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ¬ 𝐷 ≼ 𝐴) |
20 | | unxpwdom3.av |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
21 | 20 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → 𝐴 ∈ 𝑉) |
22 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 𝑏 → (𝑎 + 𝑑) = (𝑎 + 𝑏)) |
23 | 22 | eleq1d 2686 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑏 → ((𝑎 + 𝑑) ∈ 𝐵 ↔ (𝑎 + 𝑏) ∈ 𝐵)) |
24 | 23 | notbid 308 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝑏 → (¬ (𝑎 + 𝑑) ∈ 𝐵 ↔ ¬ (𝑎 + 𝑏) ∈ 𝐵)) |
25 | 24 | rspcv 3305 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ 𝐷 → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → ¬ (𝑎 + 𝑏) ∈ 𝐵)) |
26 | 25 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → ¬ (𝑎 + 𝑏) ∈ 𝐵)) |
27 | | unxpwdom3.ov |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵)) |
28 | 27 | 3expa 1265 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵)) |
29 | | elun 3753 |
. . . . . . . . . . . . 13
⊢ ((𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵) ↔ ((𝑎 + 𝑏) ∈ 𝐴 ∨ (𝑎 + 𝑏) ∈ 𝐵)) |
30 | 28, 29 | sylib 208 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → ((𝑎 + 𝑏) ∈ 𝐴 ∨ (𝑎 + 𝑏) ∈ 𝐵)) |
31 | 30 | orcomd 403 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → ((𝑎 + 𝑏) ∈ 𝐵 ∨ (𝑎 + 𝑏) ∈ 𝐴)) |
32 | 31 | ord 392 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (¬ (𝑎 + 𝑏) ∈ 𝐵 → (𝑎 + 𝑏) ∈ 𝐴)) |
33 | 26, 32 | syld 47 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → (𝑎 + 𝑏) ∈ 𝐴)) |
34 | 33 | impancom 456 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → (𝑏 ∈ 𝐷 → (𝑎 + 𝑏) ∈ 𝐴)) |
35 | | unxpwdom3.lc |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐)) |
36 | 35 | ex 450 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ((𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐))) |
37 | 36 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → ((𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐))) |
38 | 34, 37 | dom2d 7996 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → (𝐴 ∈ 𝑉 → 𝐷 ≼ 𝐴)) |
39 | 21, 38 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → 𝐷 ≼ 𝐴) |
40 | 19, 39 | mtand 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ¬ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) |
41 | | dfrex2 2996 |
. . . . 5
⊢
(∃𝑑 ∈
𝐷 (𝑎 + 𝑑) ∈ 𝐵 ↔ ¬ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) |
42 | 40, 41 | sylibr 224 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑑 ∈ 𝐷 (𝑎 + 𝑑) ∈ 𝐵) |
43 | 17, 42 | reximddv 3018 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑑 ∈ 𝐷 ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦)) |
44 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑑 ∈ V |
45 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
46 | 44, 45 | op1std 7178 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑑, 𝑦〉 → (1st ‘𝑥) = 𝑑) |
47 | 46 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑥 = 〈𝑑, 𝑦〉 → (𝑐 + (1st
‘𝑥)) = (𝑐 + 𝑑)) |
48 | 44, 45 | op2ndd 7179 |
. . . . . . 7
⊢ (𝑥 = 〈𝑑, 𝑦〉 → (2nd ‘𝑥) = 𝑦) |
49 | 47, 48 | eqeq12d 2637 |
. . . . . 6
⊢ (𝑥 = 〈𝑑, 𝑦〉 → ((𝑐 + (1st
‘𝑥)) =
(2nd ‘𝑥)
↔ (𝑐 + 𝑑) = 𝑦)) |
50 | 49 | riotabidv 6613 |
. . . . 5
⊢ (𝑥 = 〈𝑑, 𝑦〉 → (℩𝑐 ∈ 𝐶 (𝑐 + (1st
‘𝑥)) =
(2nd ‘𝑥))
= (℩𝑐 ∈
𝐶 (𝑐 + 𝑑) = 𝑦)) |
51 | 50 | eqeq2d 2632 |
. . . 4
⊢ (𝑥 = 〈𝑑, 𝑦〉 → (𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st
‘𝑥)) =
(2nd ‘𝑥))
↔ 𝑎 =
(℩𝑐 ∈
𝐶 (𝑐 + 𝑑) = 𝑦))) |
52 | 51 | rexxp 5264 |
. . 3
⊢
(∃𝑥 ∈
(𝐷 × 𝐵)𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st
‘𝑥)) =
(2nd ‘𝑥))
↔ ∃𝑑 ∈
𝐷 ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦)) |
53 | 43, 52 | sylibr 224 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑥 ∈ (𝐷 × 𝐵)𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st
‘𝑥)) =
(2nd ‘𝑥))) |
54 | 4, 53 | wdomd 8486 |
1
⊢ (𝜑 → 𝐶 ≼* (𝐷 × 𝐵)) |