Step | Hyp | Ref
| Expression |
1 | | xrnrel 36270 |
. 2
⊢ Rel
((𝑅 ∩ (𝐴 × 𝐵)) ⋉ (𝑆 ∩ (𝐴 × 𝐶))) |
2 | | relinxp 5699 |
. 2
⊢ Rel
((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) |
3 | | brxrn2 36272 |
. . . . . 6
⊢ (𝑢 ∈ V → (𝑢(𝑅 ⋉ 𝑆)𝑥 ↔ ∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧))) |
4 | 3 | elv 3427 |
. . . . 5
⊢ (𝑢(𝑅 ⋉ 𝑆)𝑥 ↔ ∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)) |
5 | 4 | anbi2i 626 |
. . . 4
⊢ ((𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)𝑥) ↔ (𝑢 ∈ 𝐴 ∧ ∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧))) |
6 | 5 | anbi2i 626 |
. . 3
⊢ ((𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)𝑥)) ↔ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ ∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)))) |
7 | | xrninxp2 36286 |
. . . 4
⊢ ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) = {〈𝑢, 𝑥〉 ∣ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)𝑥))} |
8 | 7 | brabidgaw 36262 |
. . 3
⊢ (𝑢((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶)))𝑥 ↔ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ 𝑢(𝑅 ⋉ 𝑆)𝑥))) |
9 | | brxrn2 36272 |
. . . . 5
⊢ (𝑢 ∈ V → (𝑢((𝑅 ∩ (𝐴 × 𝐵)) ⋉ (𝑆 ∩ (𝐴 × 𝐶)))𝑥 ↔ ∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢(𝑅 ∩ (𝐴 × 𝐵))𝑦 ∧ 𝑢(𝑆 ∩ (𝐴 × 𝐶))𝑧))) |
10 | 9 | elv 3427 |
. . . 4
⊢ (𝑢((𝑅 ∩ (𝐴 × 𝐵)) ⋉ (𝑆 ∩ (𝐴 × 𝐶)))𝑥 ↔ ∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢(𝑅 ∩ (𝐴 × 𝐵))𝑦 ∧ 𝑢(𝑆 ∩ (𝐴 × 𝐶))𝑧)) |
11 | | 3anass 1097 |
. . . . 5
⊢ ((𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢(𝑅 ∩ (𝐴 × 𝐵))𝑦 ∧ 𝑢(𝑆 ∩ (𝐴 × 𝐶))𝑧) ↔ (𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑢(𝑅 ∩ (𝐴 × 𝐵))𝑦 ∧ 𝑢(𝑆 ∩ (𝐴 × 𝐶))𝑧))) |
12 | 11 | 2exbii 1856 |
. . . 4
⊢
(∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢(𝑅 ∩ (𝐴 × 𝐵))𝑦 ∧ 𝑢(𝑆 ∩ (𝐴 × 𝐶))𝑧) ↔ ∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑢(𝑅 ∩ (𝐴 × 𝐵))𝑦 ∧ 𝑢(𝑆 ∩ (𝐴 × 𝐶))𝑧))) |
13 | | brinxp2 5641 |
. . . . . . . . . . . 12
⊢ (𝑢(𝑅 ∩ (𝐴 × 𝐵))𝑦 ↔ ((𝑢 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑢𝑅𝑦)) |
14 | | brinxp2 5641 |
. . . . . . . . . . . 12
⊢ (𝑢(𝑆 ∩ (𝐴 × 𝐶))𝑧 ↔ ((𝑢 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) ∧ 𝑢𝑆𝑧)) |
15 | 13, 14 | anbi12i 630 |
. . . . . . . . . . 11
⊢ ((𝑢(𝑅 ∩ (𝐴 × 𝐵))𝑦 ∧ 𝑢(𝑆 ∩ (𝐴 × 𝐶))𝑧) ↔ (((𝑢 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑢𝑅𝑦) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) ∧ 𝑢𝑆𝑧))) |
16 | | anan 36146 |
. . . . . . . . . . 11
⊢ ((((𝑢 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑢𝑅𝑦) ∧ ((𝑢 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) ∧ 𝑢𝑆𝑧)) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)))) |
17 | 15, 16 | bitri 278 |
. . . . . . . . . 10
⊢ ((𝑢(𝑅 ∩ (𝐴 × 𝐵))𝑦 ∧ 𝑢(𝑆 ∩ (𝐴 × 𝐶))𝑧) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)))) |
18 | 17 | anbi2i 626 |
. . . . . . . . 9
⊢ ((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑢(𝑅 ∩ (𝐴 × 𝐵))𝑦 ∧ 𝑢(𝑆 ∩ (𝐴 × 𝐶))𝑧)) ↔ (𝑥 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧))))) |
19 | | anass 472 |
. . . . . . . . 9
⊢ (((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧))) ↔ (𝑥 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧))))) |
20 | | eqelb 36149 |
. . . . . . . . . . 11
⊢ ((𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑥 ∈ (𝐵 × 𝐶)) ↔ (𝑥 = 〈𝑦, 𝑧〉 ∧ 〈𝑦, 𝑧〉 ∈ (𝐵 × 𝐶))) |
21 | | opelxp 5602 |
. . . . . . . . . . . 12
⊢
(〈𝑦, 𝑧〉 ∈ (𝐵 × 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) |
22 | 21 | anbi2i 626 |
. . . . . . . . . . 11
⊢ ((𝑥 = 〈𝑦, 𝑧〉 ∧ 〈𝑦, 𝑧〉 ∈ (𝐵 × 𝐶)) ↔ (𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶))) |
23 | 20, 22 | bitr2i 279 |
. . . . . . . . . 10
⊢ ((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) ↔ (𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑥 ∈ (𝐵 × 𝐶))) |
24 | 23 | anbi1i 627 |
. . . . . . . . 9
⊢ (((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧))) ↔ ((𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑥 ∈ (𝐵 × 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)))) |
25 | 18, 19, 24 | 3bitr2i 302 |
. . . . . . . 8
⊢ ((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑢(𝑅 ∩ (𝐴 × 𝐵))𝑦 ∧ 𝑢(𝑆 ∩ (𝐴 × 𝐶))𝑧)) ↔ ((𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑥 ∈ (𝐵 × 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)))) |
26 | | ancom 464 |
. . . . . . . . 9
⊢ ((𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑥 ∈ (𝐵 × 𝐶)) ↔ (𝑥 ∈ (𝐵 × 𝐶) ∧ 𝑥 = 〈𝑦, 𝑧〉)) |
27 | 26 | anbi1i 627 |
. . . . . . . 8
⊢ (((𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑥 ∈ (𝐵 × 𝐶)) ∧ (𝑢 ∈ 𝐴 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧))) ↔ ((𝑥 ∈ (𝐵 × 𝐶) ∧ 𝑥 = 〈𝑦, 𝑧〉) ∧ (𝑢 ∈ 𝐴 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)))) |
28 | | anass 472 |
. . . . . . . 8
⊢ (((𝑥 ∈ (𝐵 × 𝐶) ∧ 𝑥 = 〈𝑦, 𝑧〉) ∧ (𝑢 ∈ 𝐴 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧))) ↔ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑢 ∈ 𝐴 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧))))) |
29 | 25, 27, 28 | 3bitri 300 |
. . . . . . 7
⊢ ((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑢(𝑅 ∩ (𝐴 × 𝐵))𝑦 ∧ 𝑢(𝑆 ∩ (𝐴 × 𝐶))𝑧)) ↔ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑢 ∈ 𝐴 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧))))) |
30 | | an12 645 |
. . . . . . . . 9
⊢ ((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑢 ∈ 𝐴 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧))) ↔ (𝑢 ∈ 𝐴 ∧ (𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)))) |
31 | | 3anass 1097 |
. . . . . . . . . 10
⊢ ((𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧) ↔ (𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧))) |
32 | 31 | anbi2i 626 |
. . . . . . . . 9
⊢ ((𝑢 ∈ 𝐴 ∧ (𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)) ↔ (𝑢 ∈ 𝐴 ∧ (𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)))) |
33 | 30, 32 | bitr4i 281 |
. . . . . . . 8
⊢ ((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑢 ∈ 𝐴 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧))) ↔ (𝑢 ∈ 𝐴 ∧ (𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧))) |
34 | 33 | anbi2i 626 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑢 ∈ 𝐴 ∧ (𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)))) ↔ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ (𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)))) |
35 | 29, 34 | bitri 278 |
. . . . . 6
⊢ ((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑢(𝑅 ∩ (𝐴 × 𝐵))𝑦 ∧ 𝑢(𝑆 ∩ (𝐴 × 𝐶))𝑧)) ↔ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ (𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)))) |
36 | 35 | 2exbii 1856 |
. . . . 5
⊢
(∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑢(𝑅 ∩ (𝐴 × 𝐵))𝑦 ∧ 𝑢(𝑆 ∩ (𝐴 × 𝐶))𝑧)) ↔ ∃𝑦∃𝑧(𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ (𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)))) |
37 | | 19.42vv 1966 |
. . . . 5
⊢
(∃𝑦∃𝑧(𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ (𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧))) ↔ (𝑥 ∈ (𝐵 × 𝐶) ∧ ∃𝑦∃𝑧(𝑢 ∈ 𝐴 ∧ (𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)))) |
38 | | 19.42vv 1966 |
. . . . . 6
⊢
(∃𝑦∃𝑧(𝑢 ∈ 𝐴 ∧ (𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)) ↔ (𝑢 ∈ 𝐴 ∧ ∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧))) |
39 | 38 | anbi2i 626 |
. . . . 5
⊢ ((𝑥 ∈ (𝐵 × 𝐶) ∧ ∃𝑦∃𝑧(𝑢 ∈ 𝐴 ∧ (𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧))) ↔ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ ∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)))) |
40 | 36, 37, 39 | 3bitri 300 |
. . . 4
⊢
(∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑢(𝑅 ∩ (𝐴 × 𝐵))𝑦 ∧ 𝑢(𝑆 ∩ (𝐴 × 𝐶))𝑧)) ↔ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ ∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)))) |
41 | 10, 12, 40 | 3bitri 300 |
. . 3
⊢ (𝑢((𝑅 ∩ (𝐴 × 𝐵)) ⋉ (𝑆 ∩ (𝐴 × 𝐶)))𝑥 ↔ (𝑥 ∈ (𝐵 × 𝐶) ∧ (𝑢 ∈ 𝐴 ∧ ∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ 𝑢𝑅𝑦 ∧ 𝑢𝑆𝑧)))) |
42 | 6, 8, 41 | 3bitr4ri 307 |
. 2
⊢ (𝑢((𝑅 ∩ (𝐴 × 𝐵)) ⋉ (𝑆 ∩ (𝐴 × 𝐶)))𝑥 ↔ 𝑢((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶)))𝑥) |
43 | 1, 2, 42 | eqbrriv 5676 |
1
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⋉ (𝑆 ∩ (𝐴 × 𝐶))) = ((𝑅 ⋉ 𝑆) ∩ (𝐴 × (𝐵 × 𝐶))) |