Step | Hyp | Ref
| Expression |
1 | | ovexd 7397 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐶 ↑m (𝐴 ∪ 𝐵)) ∈ V) |
2 | | ovexd 7397 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐶 ↑m 𝐴) ∈ V) |
3 | | ovexd 7397 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐶 ↑m 𝐵) ∈ V) |
4 | 2, 3 | xpexd 7690 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)) ∈ V) |
5 | | elmapi 8794 |
. . . . 5
⊢ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) → 𝑥:(𝐴 ∪ 𝐵)⟶𝐶) |
6 | | ssun1 4137 |
. . . . 5
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
7 | | fssres 6713 |
. . . . 5
⊢ ((𝑥:(𝐴 ∪ 𝐵)⟶𝐶 ∧ 𝐴 ⊆ (𝐴 ∪ 𝐵)) → (𝑥 ↾ 𝐴):𝐴⟶𝐶) |
8 | 5, 6, 7 | sylancl 587 |
. . . 4
⊢ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) → (𝑥 ↾ 𝐴):𝐴⟶𝐶) |
9 | | ssun2 4138 |
. . . . 5
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
10 | | fssres 6713 |
. . . . 5
⊢ ((𝑥:(𝐴 ∪ 𝐵)⟶𝐶 ∧ 𝐵 ⊆ (𝐴 ∪ 𝐵)) → (𝑥 ↾ 𝐵):𝐵⟶𝐶) |
11 | 5, 9, 10 | sylancl 587 |
. . . 4
⊢ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) → (𝑥 ↾ 𝐵):𝐵⟶𝐶) |
12 | 8, 11 | jca 513 |
. . 3
⊢ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) → ((𝑥 ↾ 𝐴):𝐴⟶𝐶 ∧ (𝑥 ↾ 𝐵):𝐵⟶𝐶)) |
13 | | opelxp 5674 |
. . . 4
⊢
(⟨(𝑥 ↾
𝐴), (𝑥 ↾ 𝐵)⟩ ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)) ↔ ((𝑥 ↾ 𝐴) ∈ (𝐶 ↑m 𝐴) ∧ (𝑥 ↾ 𝐵) ∈ (𝐶 ↑m 𝐵))) |
14 | | simpl3 1194 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐶 ∈ 𝑋) |
15 | | simpl1 1192 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐴 ∈ 𝑉) |
16 | 14, 15 | elmapd 8786 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝑥 ↾ 𝐴) ∈ (𝐶 ↑m 𝐴) ↔ (𝑥 ↾ 𝐴):𝐴⟶𝐶)) |
17 | | simpl2 1193 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐵 ∈ 𝑊) |
18 | 14, 17 | elmapd 8786 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝑥 ↾ 𝐵) ∈ (𝐶 ↑m 𝐵) ↔ (𝑥 ↾ 𝐵):𝐵⟶𝐶)) |
19 | 16, 18 | anbi12d 632 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (((𝑥 ↾ 𝐴) ∈ (𝐶 ↑m 𝐴) ∧ (𝑥 ↾ 𝐵) ∈ (𝐶 ↑m 𝐵)) ↔ ((𝑥 ↾ 𝐴):𝐴⟶𝐶 ∧ (𝑥 ↾ 𝐵):𝐵⟶𝐶))) |
20 | 13, 19 | bitrid 283 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)) ↔ ((𝑥 ↾ 𝐴):𝐴⟶𝐶 ∧ (𝑥 ↾ 𝐵):𝐵⟶𝐶))) |
21 | 12, 20 | syl5ibr 246 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) → ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) |
22 | | xp1st 7958 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)) → (1st ‘𝑦) ∈ (𝐶 ↑m 𝐴)) |
23 | 22 | adantl 483 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵))) → (1st ‘𝑦) ∈ (𝐶 ↑m 𝐴)) |
24 | | elmapi 8794 |
. . . . . 6
⊢
((1st ‘𝑦) ∈ (𝐶 ↑m 𝐴) → (1st ‘𝑦):𝐴⟶𝐶) |
25 | 23, 24 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵))) → (1st ‘𝑦):𝐴⟶𝐶) |
26 | | xp2nd 7959 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)) → (2nd ‘𝑦) ∈ (𝐶 ↑m 𝐵)) |
27 | 26 | adantl 483 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵))) → (2nd ‘𝑦) ∈ (𝐶 ↑m 𝐵)) |
28 | | elmapi 8794 |
. . . . . 6
⊢
((2nd ‘𝑦) ∈ (𝐶 ↑m 𝐵) → (2nd ‘𝑦):𝐵⟶𝐶) |
29 | 27, 28 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵))) → (2nd ‘𝑦):𝐵⟶𝐶) |
30 | | simplr 768 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵))) → (𝐴 ∩ 𝐵) = ∅) |
31 | 25, 29, 30 | fun2d 6711 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵))) → ((1st ‘𝑦) ∪ (2nd
‘𝑦)):(𝐴 ∪ 𝐵)⟶𝐶) |
32 | 31 | ex 414 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)) → ((1st ‘𝑦) ∪ (2nd
‘𝑦)):(𝐴 ∪ 𝐵)⟶𝐶)) |
33 | | unexg 7688 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) |
34 | 15, 17, 33 | syl2anc 585 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ∈ V) |
35 | 14, 34 | elmapd 8786 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (((1st
‘𝑦) ∪
(2nd ‘𝑦))
∈ (𝐶
↑m (𝐴 ∪
𝐵)) ↔ ((1st
‘𝑦) ∪
(2nd ‘𝑦)):(𝐴 ∪ 𝐵)⟶𝐶)) |
36 | 32, 35 | sylibrd 259 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)) → ((1st ‘𝑦) ∪ (2nd
‘𝑦)) ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)))) |
37 | | 1st2nd2 7965 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩) |
38 | 37 | ad2antll 728 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩) |
39 | 25 | adantrl 715 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (1st ‘𝑦):𝐴⟶𝐶) |
40 | 29 | adantrl 715 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (2nd ‘𝑦):𝐵⟶𝐶) |
41 | | res0 5946 |
. . . . . . . . . 10
⊢
((1st ‘𝑦) ↾ ∅) = ∅ |
42 | | res0 5946 |
. . . . . . . . . 10
⊢
((2nd ‘𝑦) ↾ ∅) = ∅ |
43 | 41, 42 | eqtr4i 2768 |
. . . . . . . . 9
⊢
((1st ‘𝑦) ↾ ∅) = ((2nd
‘𝑦) ↾
∅) |
44 | | simplr 768 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (𝐴 ∩ 𝐵) = ∅) |
45 | 44 | reseq2d 5942 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → ((1st ‘𝑦) ↾ (𝐴 ∩ 𝐵)) = ((1st ‘𝑦) ↾
∅)) |
46 | 44 | reseq2d 5942 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → ((2nd ‘𝑦) ↾ (𝐴 ∩ 𝐵)) = ((2nd ‘𝑦) ↾
∅)) |
47 | 43, 45, 46 | 3eqtr4a 2803 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → ((1st ‘𝑦) ↾ (𝐴 ∩ 𝐵)) = ((2nd ‘𝑦) ↾ (𝐴 ∩ 𝐵))) |
48 | | fresaunres1 6720 |
. . . . . . . 8
⊢
(((1st ‘𝑦):𝐴⟶𝐶 ∧ (2nd ‘𝑦):𝐵⟶𝐶 ∧ ((1st ‘𝑦) ↾ (𝐴 ∩ 𝐵)) = ((2nd ‘𝑦) ↾ (𝐴 ∩ 𝐵))) → (((1st ‘𝑦) ∪ (2nd
‘𝑦)) ↾ 𝐴) = (1st ‘𝑦)) |
49 | 39, 40, 47, 48 | syl3anc 1372 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (((1st ‘𝑦) ∪ (2nd
‘𝑦)) ↾ 𝐴) = (1st ‘𝑦)) |
50 | | fresaunres2 6719 |
. . . . . . . 8
⊢
(((1st ‘𝑦):𝐴⟶𝐶 ∧ (2nd ‘𝑦):𝐵⟶𝐶 ∧ ((1st ‘𝑦) ↾ (𝐴 ∩ 𝐵)) = ((2nd ‘𝑦) ↾ (𝐴 ∩ 𝐵))) → (((1st ‘𝑦) ∪ (2nd
‘𝑦)) ↾ 𝐵) = (2nd ‘𝑦)) |
51 | 39, 40, 47, 50 | syl3anc 1372 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (((1st ‘𝑦) ∪ (2nd
‘𝑦)) ↾ 𝐵) = (2nd ‘𝑦)) |
52 | 49, 51 | opeq12d 4843 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → ⟨(((1st
‘𝑦) ∪
(2nd ‘𝑦))
↾ 𝐴),
(((1st ‘𝑦)
∪ (2nd ‘𝑦)) ↾ 𝐵)⟩ = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩) |
53 | 38, 52 | eqtr4d 2780 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → 𝑦 = ⟨(((1st ‘𝑦) ∪ (2nd
‘𝑦)) ↾ 𝐴), (((1st
‘𝑦) ∪
(2nd ‘𝑦))
↾ 𝐵)⟩) |
54 | | reseq1 5936 |
. . . . . . 7
⊢ (𝑥 = ((1st ‘𝑦) ∪ (2nd
‘𝑦)) → (𝑥 ↾ 𝐴) = (((1st ‘𝑦) ∪ (2nd
‘𝑦)) ↾ 𝐴)) |
55 | | reseq1 5936 |
. . . . . . 7
⊢ (𝑥 = ((1st ‘𝑦) ∪ (2nd
‘𝑦)) → (𝑥 ↾ 𝐵) = (((1st ‘𝑦) ∪ (2nd
‘𝑦)) ↾ 𝐵)) |
56 | 54, 55 | opeq12d 4843 |
. . . . . 6
⊢ (𝑥 = ((1st ‘𝑦) ∪ (2nd
‘𝑦)) →
⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ = ⟨(((1st
‘𝑦) ∪
(2nd ‘𝑦))
↾ 𝐴),
(((1st ‘𝑦)
∪ (2nd ‘𝑦)) ↾ 𝐵)⟩) |
57 | 56 | eqeq2d 2748 |
. . . . 5
⊢ (𝑥 = ((1st ‘𝑦) ∪ (2nd
‘𝑦)) → (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ ↔ 𝑦 = ⟨(((1st ‘𝑦) ∪ (2nd
‘𝑦)) ↾ 𝐴), (((1st
‘𝑦) ∪
(2nd ‘𝑦))
↾ 𝐵)⟩)) |
58 | 53, 57 | syl5ibrcom 247 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) → 𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩)) |
59 | | ffn 6673 |
. . . . . . . 8
⊢ (𝑥:(𝐴 ∪ 𝐵)⟶𝐶 → 𝑥 Fn (𝐴 ∪ 𝐵)) |
60 | | fnresdm 6625 |
. . . . . . . 8
⊢ (𝑥 Fn (𝐴 ∪ 𝐵) → (𝑥 ↾ (𝐴 ∪ 𝐵)) = 𝑥) |
61 | 5, 59, 60 | 3syl 18 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) → (𝑥 ↾ (𝐴 ∪ 𝐵)) = 𝑥) |
62 | 61 | ad2antrl 727 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (𝑥 ↾ (𝐴 ∪ 𝐵)) = 𝑥) |
63 | 62 | eqcomd 2743 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → 𝑥 = (𝑥 ↾ (𝐴 ∪ 𝐵))) |
64 | | vex 3452 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
65 | 64 | resex 5990 |
. . . . . . . . 9
⊢ (𝑥 ↾ 𝐴) ∈ V |
66 | 64 | resex 5990 |
. . . . . . . . 9
⊢ (𝑥 ↾ 𝐵) ∈ V |
67 | 65, 66 | op1std 7936 |
. . . . . . . 8
⊢ (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → (1st ‘𝑦) = (𝑥 ↾ 𝐴)) |
68 | 65, 66 | op2ndd 7937 |
. . . . . . . 8
⊢ (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → (2nd ‘𝑦) = (𝑥 ↾ 𝐵)) |
69 | 67, 68 | uneq12d 4129 |
. . . . . . 7
⊢ (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → ((1st ‘𝑦) ∪ (2nd
‘𝑦)) = ((𝑥 ↾ 𝐴) ∪ (𝑥 ↾ 𝐵))) |
70 | | resundi 5956 |
. . . . . . 7
⊢ (𝑥 ↾ (𝐴 ∪ 𝐵)) = ((𝑥 ↾ 𝐴) ∪ (𝑥 ↾ 𝐵)) |
71 | 69, 70 | eqtr4di 2795 |
. . . . . 6
⊢ (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → ((1st ‘𝑦) ∪ (2nd
‘𝑦)) = (𝑥 ↾ (𝐴 ∪ 𝐵))) |
72 | 71 | eqeq2d 2748 |
. . . . 5
⊢ (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↔ 𝑥 = (𝑥 ↾ (𝐴 ∪ 𝐵)))) |
73 | 63, 72 | syl5ibrcom 247 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → 𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)))) |
74 | 58, 73 | impbid 211 |
. . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↔ 𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩)) |
75 | 74 | ex 414 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵))) → (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↔ 𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩))) |
76 | 1, 4, 21, 36, 75 | en3d 8936 |
1
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐶 ↑m (𝐴 ∪ 𝐵)) ≈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵))) |