Step | Hyp | Ref
| Expression |
1 | | df-txp 34143 |
. . 3
⊢ (𝐴 ⊗ 𝐵) = ((◡(1st ↾ (V × V))
∘ 𝐴) ∩ (◡(2nd ↾ (V × V))
∘ 𝐵)) |
2 | 1 | breqi 5081 |
. 2
⊢ (𝑋(𝐴 ⊗ 𝐵)〈𝑌, 𝑍〉 ↔ 𝑋((◡(1st ↾ (V × V))
∘ 𝐴) ∩ (◡(2nd ↾ (V × V))
∘ 𝐵))〈𝑌, 𝑍〉) |
3 | | brin 5127 |
. 2
⊢ (𝑋((◡(1st ↾ (V × V))
∘ 𝐴) ∩ (◡(2nd ↾ (V × V))
∘ 𝐵))〈𝑌, 𝑍〉 ↔ (𝑋(◡(1st ↾ (V × V))
∘ 𝐴)〈𝑌, 𝑍〉 ∧ 𝑋(◡(2nd ↾ (V × V))
∘ 𝐵)〈𝑌, 𝑍〉)) |
4 | | brtxp.1 |
. . . . 5
⊢ 𝑋 ∈ V |
5 | | opex 5379 |
. . . . 5
⊢
〈𝑌, 𝑍〉 ∈ V |
6 | 4, 5 | brco 5774 |
. . . 4
⊢ (𝑋(◡(1st ↾ (V × V))
∘ 𝐴)〈𝑌, 𝑍〉 ↔ ∃𝑦(𝑋𝐴𝑦 ∧ 𝑦◡(1st ↾ (V ×
V))〈𝑌, 𝑍〉)) |
7 | | vex 3435 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
8 | 7, 5 | brcnv 5786 |
. . . . . . 7
⊢ (𝑦◡(1st ↾ (V ×
V))〈𝑌, 𝑍〉 ↔ 〈𝑌, 𝑍〉(1st ↾ (V ×
V))𝑦) |
9 | | brtxp.2 |
. . . . . . . . 9
⊢ 𝑌 ∈ V |
10 | | brtxp.3 |
. . . . . . . . 9
⊢ 𝑍 ∈ V |
11 | 9, 10 | opelvv 5625 |
. . . . . . . 8
⊢
〈𝑌, 𝑍〉 ∈ (V ×
V) |
12 | 7 | brresi 5895 |
. . . . . . . 8
⊢
(〈𝑌, 𝑍〉(1st ↾ (V
× V))𝑦 ↔
(〈𝑌, 𝑍〉 ∈ (V × V) ∧
〈𝑌, 𝑍〉1st 𝑦)) |
13 | 11, 12 | mpbiran 706 |
. . . . . . 7
⊢
(〈𝑌, 𝑍〉(1st ↾ (V
× V))𝑦 ↔
〈𝑌, 𝑍〉1st 𝑦) |
14 | 9, 10 | br1steq 33732 |
. . . . . . 7
⊢
(〈𝑌, 𝑍〉1st 𝑦 ↔ 𝑦 = 𝑌) |
15 | 8, 13, 14 | 3bitri 297 |
. . . . . 6
⊢ (𝑦◡(1st ↾ (V ×
V))〈𝑌, 𝑍〉 ↔ 𝑦 = 𝑌) |
16 | 15 | anbi1ci 626 |
. . . . 5
⊢ ((𝑋𝐴𝑦 ∧ 𝑦◡(1st ↾ (V ×
V))〈𝑌, 𝑍〉) ↔ (𝑦 = 𝑌 ∧ 𝑋𝐴𝑦)) |
17 | 16 | exbii 1850 |
. . . 4
⊢
(∃𝑦(𝑋𝐴𝑦 ∧ 𝑦◡(1st ↾ (V ×
V))〈𝑌, 𝑍〉) ↔ ∃𝑦(𝑦 = 𝑌 ∧ 𝑋𝐴𝑦)) |
18 | | breq2 5079 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝑋𝐴𝑦 ↔ 𝑋𝐴𝑌)) |
19 | 9, 18 | ceqsexv 3478 |
. . . 4
⊢
(∃𝑦(𝑦 = 𝑌 ∧ 𝑋𝐴𝑦) ↔ 𝑋𝐴𝑌) |
20 | 6, 17, 19 | 3bitri 297 |
. . 3
⊢ (𝑋(◡(1st ↾ (V × V))
∘ 𝐴)〈𝑌, 𝑍〉 ↔ 𝑋𝐴𝑌) |
21 | 4, 5 | brco 5774 |
. . . 4
⊢ (𝑋(◡(2nd ↾ (V × V))
∘ 𝐵)〈𝑌, 𝑍〉 ↔ ∃𝑧(𝑋𝐵𝑧 ∧ 𝑧◡(2nd ↾ (V ×
V))〈𝑌, 𝑍〉)) |
22 | | vex 3435 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
23 | 22, 5 | brcnv 5786 |
. . . . . . 7
⊢ (𝑧◡(2nd ↾ (V ×
V))〈𝑌, 𝑍〉 ↔ 〈𝑌, 𝑍〉(2nd ↾ (V ×
V))𝑧) |
24 | 22 | brresi 5895 |
. . . . . . . 8
⊢
(〈𝑌, 𝑍〉(2nd ↾ (V
× V))𝑧 ↔
(〈𝑌, 𝑍〉 ∈ (V × V) ∧
〈𝑌, 𝑍〉2nd 𝑧)) |
25 | 11, 24 | mpbiran 706 |
. . . . . . 7
⊢
(〈𝑌, 𝑍〉(2nd ↾ (V
× V))𝑧 ↔
〈𝑌, 𝑍〉2nd 𝑧) |
26 | 9, 10 | br2ndeq 33733 |
. . . . . . 7
⊢
(〈𝑌, 𝑍〉2nd 𝑧 ↔ 𝑧 = 𝑍) |
27 | 23, 25, 26 | 3bitri 297 |
. . . . . 6
⊢ (𝑧◡(2nd ↾ (V ×
V))〈𝑌, 𝑍〉 ↔ 𝑧 = 𝑍) |
28 | 27 | anbi1ci 626 |
. . . . 5
⊢ ((𝑋𝐵𝑧 ∧ 𝑧◡(2nd ↾ (V ×
V))〈𝑌, 𝑍〉) ↔ (𝑧 = 𝑍 ∧ 𝑋𝐵𝑧)) |
29 | 28 | exbii 1850 |
. . . 4
⊢
(∃𝑧(𝑋𝐵𝑧 ∧ 𝑧◡(2nd ↾ (V ×
V))〈𝑌, 𝑍〉) ↔ ∃𝑧(𝑧 = 𝑍 ∧ 𝑋𝐵𝑧)) |
30 | | breq2 5079 |
. . . . 5
⊢ (𝑧 = 𝑍 → (𝑋𝐵𝑧 ↔ 𝑋𝐵𝑍)) |
31 | 10, 30 | ceqsexv 3478 |
. . . 4
⊢
(∃𝑧(𝑧 = 𝑍 ∧ 𝑋𝐵𝑧) ↔ 𝑋𝐵𝑍) |
32 | 21, 29, 31 | 3bitri 297 |
. . 3
⊢ (𝑋(◡(2nd ↾ (V × V))
∘ 𝐵)〈𝑌, 𝑍〉 ↔ 𝑋𝐵𝑍) |
33 | 20, 32 | anbi12i 627 |
. 2
⊢ ((𝑋(◡(1st ↾ (V × V))
∘ 𝐴)〈𝑌, 𝑍〉 ∧ 𝑋(◡(2nd ↾ (V × V))
∘ 𝐵)〈𝑌, 𝑍〉) ↔ (𝑋𝐴𝑌 ∧ 𝑋𝐵𝑍)) |
34 | 2, 3, 33 | 3bitri 297 |
1
⊢ (𝑋(𝐴 ⊗ 𝐵)〈𝑌, 𝑍〉 ↔ (𝑋𝐴𝑌 ∧ 𝑋𝐵𝑍)) |