Step | Hyp | Ref
| Expression |
1 | | relco 4762 |
. 2
⊢ Rel
((A ∘ B) ∘ 𝐶) |
2 | | relco 4762 |
. 2
⊢ Rel
(A ∘ (B ∘ 𝐶)) |
3 | | excom 1551 |
. . . 4
⊢ (∃z∃w(x𝐶z ∧ (zBw ∧ wAy)) ↔
∃w∃z(x𝐶z ∧ (zBw ∧ wAy))) |
4 | | anass 381 |
. . . . 5
⊢
(((x𝐶z ∧ zBw) ∧ wAy) ↔
(x𝐶z ∧ (zBw ∧ wAy))) |
5 | 4 | 2exbii 1494 |
. . . 4
⊢ (∃w∃z((x𝐶z ∧ zBw) ∧ wAy) ↔ ∃w∃z(x𝐶z ∧ (zBw ∧ wAy))) |
6 | 3, 5 | bitr4i 176 |
. . 3
⊢ (∃z∃w(x𝐶z ∧ (zBw ∧ wAy)) ↔
∃w∃z((x𝐶z ∧ zBw) ∧ wAy)) |
7 | | vex 2554 |
. . . . . . 7
⊢ z ∈
V |
8 | | vex 2554 |
. . . . . . 7
⊢ y ∈
V |
9 | 7, 8 | brco 4449 |
. . . . . 6
⊢ (z(A ∘
B)y
↔ ∃w(zBw ∧ wAy)) |
10 | 9 | anbi2i 430 |
. . . . 5
⊢
((x𝐶z ∧ z(A ∘ B)y) ↔
(x𝐶z ∧ ∃w(zBw ∧ wAy))) |
11 | 10 | exbii 1493 |
. . . 4
⊢ (∃z(x𝐶z ∧ z(A ∘ B)y) ↔
∃z(x𝐶z ∧ ∃w(zBw ∧ wAy))) |
12 | | vex 2554 |
. . . . 5
⊢ x ∈
V |
13 | 12, 8 | opelco 4450 |
. . . 4
⊢
(〈x, y〉 ∈
((A ∘ B) ∘ 𝐶) ↔ ∃z(x𝐶z ∧ z(A ∘ B)y)) |
14 | | exdistr 1784 |
. . . 4
⊢ (∃z∃w(x𝐶z ∧ (zBw ∧ wAy)) ↔
∃z(x𝐶z ∧ ∃w(zBw ∧ wAy))) |
15 | 11, 13, 14 | 3bitr4i 201 |
. . 3
⊢
(〈x, y〉 ∈
((A ∘ B) ∘ 𝐶) ↔ ∃z∃w(x𝐶z ∧ (zBw ∧ wAy))) |
16 | | vex 2554 |
. . . . . . 7
⊢ w ∈
V |
17 | 12, 16 | brco 4449 |
. . . . . 6
⊢ (x(B ∘
𝐶)w ↔ ∃z(x𝐶z ∧ zBw)) |
18 | 17 | anbi1i 431 |
. . . . 5
⊢
((x(B ∘ 𝐶)w ∧ wAy) ↔
(∃z(x𝐶z ∧ zBw) ∧ wAy)) |
19 | 18 | exbii 1493 |
. . . 4
⊢ (∃w(x(B ∘
𝐶)w ∧ wAy) ↔ ∃w(∃z(x𝐶z ∧ zBw) ∧ wAy)) |
20 | 12, 8 | opelco 4450 |
. . . 4
⊢
(〈x, y〉 ∈
(A ∘ (B ∘ 𝐶)) ↔ ∃w(x(B ∘
𝐶)w ∧ wAy)) |
21 | | 19.41v 1779 |
. . . . 5
⊢ (∃z((x𝐶z ∧ zBw) ∧ wAy) ↔
(∃z(x𝐶z ∧ zBw) ∧ wAy)) |
22 | 21 | exbii 1493 |
. . . 4
⊢ (∃w∃z((x𝐶z ∧ zBw) ∧ wAy) ↔ ∃w(∃z(x𝐶z ∧ zBw) ∧ wAy)) |
23 | 19, 20, 22 | 3bitr4i 201 |
. . 3
⊢
(〈x, y〉 ∈
(A ∘ (B ∘ 𝐶)) ↔ ∃w∃z((x𝐶z ∧ zBw) ∧ wAy)) |
24 | 6, 15, 23 | 3bitr4i 201 |
. 2
⊢
(〈x, y〉 ∈
((A ∘ B) ∘ 𝐶) ↔ 〈x, y〉 ∈ (A ∘
(B ∘ 𝐶))) |
25 | 1, 2, 24 | eqrelriiv 4377 |
1
⊢
((A ∘ B) ∘ 𝐶) = (A
∘ (B ∘ 𝐶)) |