Step | Hyp | Ref
| Expression |
1 | | brex 4689 |
. . 3
⊢ (A(R ⊗
S)〈B, C〉 →
(A ∈ V
∧ 〈B, C〉 ∈
V)) |
2 | | opexb 4603 |
. . . 4
⊢ (〈B, C〉 ∈ V ↔ (B
∈ V ∧
C ∈
V)) |
3 | 2 | anbi2i 675 |
. . 3
⊢ ((A ∈ V ∧ 〈B, C〉 ∈ V) ↔
(A ∈ V
∧ (B ∈ V ∧ C ∈
V))) |
4 | 1, 3 | sylib 188 |
. 2
⊢ (A(R ⊗
S)〈B, C〉 →
(A ∈ V
∧ (B ∈ V ∧ C ∈
V))) |
5 | | brex 4689 |
. . . 4
⊢ (ARB → (A
∈ V ∧
B ∈
V)) |
6 | | brex 4689 |
. . . 4
⊢ (ASC → (A
∈ V ∧
C ∈
V)) |
7 | 5, 6 | anim12i 549 |
. . 3
⊢ ((ARB ∧ ASC) → ((A
∈ V ∧
B ∈ V)
∧ (A ∈ V ∧ C ∈
V))) |
8 | | anandi 801 |
. . 3
⊢ ((A ∈ V ∧ (B ∈ V ∧ C ∈ V)) ↔
((A ∈ V
∧ B ∈ V) ∧ (A ∈ V ∧ C ∈ V))) |
9 | 7, 8 | sylibr 203 |
. 2
⊢ ((ARB ∧ ASC) → (A
∈ V ∧
(B ∈ V
∧ C ∈ V))) |
10 | | breq1 4642 |
. . . . . 6
⊢ (x = A →
(x(R
⊗ S)〈B, C〉 ↔ A(R ⊗
S)〈B, C〉)) |
11 | | breq1 4642 |
. . . . . . 7
⊢ (x = A →
(xRB ↔
ARB)) |
12 | | breq1 4642 |
. . . . . . 7
⊢ (x = A →
(xSC ↔
ASC)) |
13 | 11, 12 | anbi12d 691 |
. . . . . 6
⊢ (x = A →
((xRB ∧ xSC) ↔
(ARB ∧ ASC))) |
14 | 10, 13 | bibi12d 312 |
. . . . 5
⊢ (x = A →
((x(R
⊗ S)〈B, C〉 ↔
(xRB ∧ xSC)) ↔
(A(R
⊗ S)〈B, C〉 ↔
(ARB ∧ ASC)))) |
15 | 14 | imbi2d 307 |
. . . 4
⊢ (x = A →
(((B ∈ V
∧ C ∈ V) → (x(R ⊗
S)〈B, C〉 ↔
(xRB ∧ xSC))) ↔
((B ∈ V
∧ C ∈ V) → (A(R ⊗
S)〈B, C〉 ↔
(ARB ∧ ASC))))) |
16 | | opeq1 4578 |
. . . . . . 7
⊢ (y = B →
〈y,
z〉 =
〈B,
z〉) |
17 | 16 | breq2d 4651 |
. . . . . 6
⊢ (y = B →
(x(R
⊗ S)〈y, z〉 ↔ x(R ⊗
S)〈B, z〉)) |
18 | | breq2 4643 |
. . . . . . 7
⊢ (y = B →
(xRy ↔
xRB)) |
19 | 18 | anbi1d 685 |
. . . . . 6
⊢ (y = B →
((xRy ∧ xSz) ↔
(xRB ∧ xSz))) |
20 | 17, 19 | bibi12d 312 |
. . . . 5
⊢ (y = B →
((x(R
⊗ S)〈y, z〉 ↔
(xRy ∧ xSz)) ↔
(x(R
⊗ S)〈B, z〉 ↔
(xRB ∧ xSz)))) |
21 | | opeq2 4579 |
. . . . . . 7
⊢ (z = C →
〈B,
z〉 =
〈B,
C〉) |
22 | 21 | breq2d 4651 |
. . . . . 6
⊢ (z = C →
(x(R
⊗ S)〈B, z〉 ↔ x(R ⊗
S)〈B, C〉)) |
23 | | breq2 4643 |
. . . . . . 7
⊢ (z = C →
(xSz ↔
xSC)) |
24 | 23 | anbi2d 684 |
. . . . . 6
⊢ (z = C →
((xRB ∧ xSz) ↔
(xRB ∧ xSC))) |
25 | 22, 24 | bibi12d 312 |
. . . . 5
⊢ (z = C →
((x(R
⊗ S)〈B, z〉 ↔
(xRB ∧ xSz)) ↔
(x(R
⊗ S)〈B, C〉 ↔
(xRB ∧ xSC)))) |
26 | | df-txp 5736 |
. . . . . . 7
⊢ (R ⊗ S) =
((◡1st ∘ R) ∩
(◡2nd ∘ S)) |
27 | 26 | breqi 4645 |
. . . . . 6
⊢ (x(R ⊗
S)〈y, z〉 ↔ x((◡1st ∘ R) ∩
(◡2nd ∘ S))〈y, z〉) |
28 | | brin 4693 |
. . . . . 6
⊢ (x((◡1st ∘ R) ∩
(◡2nd ∘ S))〈y, z〉 ↔
(x(◡1st ∘ R)〈y, z〉 ∧ x(◡2nd ∘ S)〈y, z〉)) |
29 | | brco 4883 |
. . . . . . . 8
⊢ (x(◡1st ∘ R)〈y, z〉 ↔ ∃t(xRt ∧ t◡1st 〈y, z〉)) |
30 | | ancom 437 |
. . . . . . . . . 10
⊢ ((xRt ∧ t◡1st 〈y, z〉) ↔
(t◡1st 〈y, z〉 ∧ xRt)) |
31 | | brcnv 4892 |
. . . . . . . . . . . 12
⊢ (t◡1st 〈y, z〉 ↔ 〈y, z〉1st
t) |
32 | | vex 2862 |
. . . . . . . . . . . . 13
⊢ y ∈
V |
33 | | vex 2862 |
. . . . . . . . . . . . 13
⊢ z ∈
V |
34 | 32, 33 | opbr1st 5501 |
. . . . . . . . . . . 12
⊢ (〈y, z〉1st
t ↔ y = t) |
35 | | equcom 1680 |
. . . . . . . . . . . 12
⊢ (y = t ↔
t = y) |
36 | 31, 34, 35 | 3bitri 262 |
. . . . . . . . . . 11
⊢ (t◡1st 〈y, z〉 ↔ t = y) |
37 | 36 | anbi1i 676 |
. . . . . . . . . 10
⊢ ((t◡1st 〈y, z〉 ∧ xRt) ↔
(t = y
∧ xRt)) |
38 | 30, 37 | bitri 240 |
. . . . . . . . 9
⊢ ((xRt ∧ t◡1st 〈y, z〉) ↔
(t = y
∧ xRt)) |
39 | 38 | exbii 1582 |
. . . . . . . 8
⊢ (∃t(xRt ∧ t◡1st 〈y, z〉) ↔ ∃t(t = y ∧ xRt)) |
40 | | breq2 4643 |
. . . . . . . . 9
⊢ (t = y →
(xRt ↔
xRy)) |
41 | 32, 40 | ceqsexv 2894 |
. . . . . . . 8
⊢ (∃t(t = y ∧ xRt) ↔
xRy) |
42 | 29, 39, 41 | 3bitri 262 |
. . . . . . 7
⊢ (x(◡1st ∘ R)〈y, z〉 ↔ xRy) |
43 | | brco 4883 |
. . . . . . . 8
⊢ (x(◡2nd ∘ S)〈y, z〉 ↔ ∃t(xSt ∧ t◡2nd 〈y, z〉)) |
44 | | ancom 437 |
. . . . . . . . . 10
⊢ ((xSt ∧ t◡2nd 〈y, z〉) ↔
(t◡2nd 〈y, z〉 ∧ xSt)) |
45 | | brcnv 4892 |
. . . . . . . . . . . 12
⊢ (t◡2nd 〈y, z〉 ↔ 〈y, z〉2nd
t) |
46 | 32, 33 | opbr2nd 5502 |
. . . . . . . . . . . 12
⊢ (〈y, z〉2nd
t ↔ z = t) |
47 | | equcom 1680 |
. . . . . . . . . . . 12
⊢ (z = t ↔
t = z) |
48 | 45, 46, 47 | 3bitri 262 |
. . . . . . . . . . 11
⊢ (t◡2nd 〈y, z〉 ↔ t = z) |
49 | 48 | anbi1i 676 |
. . . . . . . . . 10
⊢ ((t◡2nd 〈y, z〉 ∧ xSt) ↔
(t = z
∧ xSt)) |
50 | 44, 49 | bitri 240 |
. . . . . . . . 9
⊢ ((xSt ∧ t◡2nd 〈y, z〉) ↔
(t = z
∧ xSt)) |
51 | 50 | exbii 1582 |
. . . . . . . 8
⊢ (∃t(xSt ∧ t◡2nd 〈y, z〉) ↔ ∃t(t = z ∧ xSt)) |
52 | | breq2 4643 |
. . . . . . . . 9
⊢ (t = z →
(xSt ↔
xSz)) |
53 | 33, 52 | ceqsexv 2894 |
. . . . . . . 8
⊢ (∃t(t = z ∧ xSt) ↔
xSz) |
54 | 43, 51, 53 | 3bitri 262 |
. . . . . . 7
⊢ (x(◡2nd ∘ S)〈y, z〉 ↔ xSz) |
55 | 42, 54 | anbi12i 678 |
. . . . . 6
⊢ ((x(◡1st ∘ R)〈y, z〉 ∧ x(◡2nd ∘ S)〈y, z〉) ↔
(xRy ∧ xSz)) |
56 | 27, 28, 55 | 3bitri 262 |
. . . . 5
⊢ (x(R ⊗
S)〈y, z〉 ↔
(xRy ∧ xSz)) |
57 | 20, 25, 56 | vtocl2g 2918 |
. . . 4
⊢ ((B ∈ V ∧ C ∈ V) → (x(R ⊗
S)〈B, C〉 ↔
(xRB ∧ xSC))) |
58 | 15, 57 | vtoclg 2914 |
. . 3
⊢ (A ∈ V →
((B ∈ V
∧ C ∈ V) → (A(R ⊗
S)〈B, C〉 ↔
(ARB ∧ ASC)))) |
59 | 58 | imp 418 |
. 2
⊢ ((A ∈ V ∧ (B ∈ V ∧ C ∈ V)) →
(A(R
⊗ S)〈B, C〉 ↔
(ARB ∧ ASC))) |
60 | 4, 9, 59 | pm5.21nii 342 |
1
⊢ (A(R ⊗
S)〈B, C〉 ↔
(ARB ∧ ASC)) |