| Step | Hyp | Ref
| Expression |
| 1 | | df-pprod 35856 |
. . 3
⊢
pprod(𝐴, 𝐵) = ((𝐴 ∘ (1st ↾ (V ×
V))) ⊗ (𝐵 ∘
(2nd ↾ (V × V)))) |
| 2 | 1 | breqi 5149 |
. 2
⊢
(〈𝑋, 𝑌〉pprod(𝐴, 𝐵)〈𝑍, 𝑊〉 ↔ 〈𝑋, 𝑌〉((𝐴 ∘ (1st ↾ (V ×
V))) ⊗ (𝐵 ∘
(2nd ↾ (V × V))))〈𝑍, 𝑊〉) |
| 3 | | opex 5469 |
. . 3
⊢
〈𝑋, 𝑌〉 ∈ V |
| 4 | | brpprod.3 |
. . 3
⊢ 𝑍 ∈ V |
| 5 | | brpprod.4 |
. . 3
⊢ 𝑊 ∈ V |
| 6 | 3, 4, 5 | brtxp 35881 |
. 2
⊢
(〈𝑋, 𝑌〉((𝐴 ∘ (1st ↾ (V ×
V))) ⊗ (𝐵 ∘
(2nd ↾ (V × V))))〈𝑍, 𝑊〉 ↔ (〈𝑋, 𝑌〉(𝐴 ∘ (1st ↾ (V ×
V)))𝑍 ∧ 〈𝑋, 𝑌〉(𝐵 ∘ (2nd ↾ (V ×
V)))𝑊)) |
| 7 | 3, 4 | brco 5881 |
. . . 4
⊢
(〈𝑋, 𝑌〉(𝐴 ∘ (1st ↾ (V ×
V)))𝑍 ↔ ∃𝑥(〈𝑋, 𝑌〉(1st ↾ (V ×
V))𝑥 ∧ 𝑥𝐴𝑍)) |
| 8 | | brpprod.1 |
. . . . . . . . 9
⊢ 𝑋 ∈ V |
| 9 | | brpprod.2 |
. . . . . . . . 9
⊢ 𝑌 ∈ V |
| 10 | 8, 9 | opelvv 5725 |
. . . . . . . 8
⊢
〈𝑋, 𝑌〉 ∈ (V ×
V) |
| 11 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
| 12 | 11 | brresi 6006 |
. . . . . . . 8
⊢
(〈𝑋, 𝑌〉(1st ↾ (V
× V))𝑥 ↔
(〈𝑋, 𝑌〉 ∈ (V × V) ∧
〈𝑋, 𝑌〉1st 𝑥)) |
| 13 | 10, 12 | mpbiran 709 |
. . . . . . 7
⊢
(〈𝑋, 𝑌〉(1st ↾ (V
× V))𝑥 ↔
〈𝑋, 𝑌〉1st 𝑥) |
| 14 | 8, 9 | br1steq 35771 |
. . . . . . 7
⊢
(〈𝑋, 𝑌〉1st 𝑥 ↔ 𝑥 = 𝑋) |
| 15 | 13, 14 | bitri 275 |
. . . . . 6
⊢
(〈𝑋, 𝑌〉(1st ↾ (V
× V))𝑥 ↔ 𝑥 = 𝑋) |
| 16 | 15 | anbi1i 624 |
. . . . 5
⊢
((〈𝑋, 𝑌〉(1st ↾ (V
× V))𝑥 ∧ 𝑥𝐴𝑍) ↔ (𝑥 = 𝑋 ∧ 𝑥𝐴𝑍)) |
| 17 | 16 | exbii 1848 |
. . . 4
⊢
(∃𝑥(〈𝑋, 𝑌〉(1st ↾ (V ×
V))𝑥 ∧ 𝑥𝐴𝑍) ↔ ∃𝑥(𝑥 = 𝑋 ∧ 𝑥𝐴𝑍)) |
| 18 | | breq1 5146 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥𝐴𝑍 ↔ 𝑋𝐴𝑍)) |
| 19 | 8, 18 | ceqsexv 3532 |
. . . 4
⊢
(∃𝑥(𝑥 = 𝑋 ∧ 𝑥𝐴𝑍) ↔ 𝑋𝐴𝑍) |
| 20 | 7, 17, 19 | 3bitri 297 |
. . 3
⊢
(〈𝑋, 𝑌〉(𝐴 ∘ (1st ↾ (V ×
V)))𝑍 ↔ 𝑋𝐴𝑍) |
| 21 | 3, 5 | brco 5881 |
. . . 4
⊢
(〈𝑋, 𝑌〉(𝐵 ∘ (2nd ↾ (V ×
V)))𝑊 ↔ ∃𝑦(〈𝑋, 𝑌〉(2nd ↾ (V ×
V))𝑦 ∧ 𝑦𝐵𝑊)) |
| 22 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
| 23 | 22 | brresi 6006 |
. . . . . . . 8
⊢
(〈𝑋, 𝑌〉(2nd ↾ (V
× V))𝑦 ↔
(〈𝑋, 𝑌〉 ∈ (V × V) ∧
〈𝑋, 𝑌〉2nd 𝑦)) |
| 24 | 10, 23 | mpbiran 709 |
. . . . . . 7
⊢
(〈𝑋, 𝑌〉(2nd ↾ (V
× V))𝑦 ↔
〈𝑋, 𝑌〉2nd 𝑦) |
| 25 | 8, 9 | br2ndeq 35772 |
. . . . . . 7
⊢
(〈𝑋, 𝑌〉2nd 𝑦 ↔ 𝑦 = 𝑌) |
| 26 | 24, 25 | bitri 275 |
. . . . . 6
⊢
(〈𝑋, 𝑌〉(2nd ↾ (V
× V))𝑦 ↔ 𝑦 = 𝑌) |
| 27 | 26 | anbi1i 624 |
. . . . 5
⊢
((〈𝑋, 𝑌〉(2nd ↾ (V
× V))𝑦 ∧ 𝑦𝐵𝑊) ↔ (𝑦 = 𝑌 ∧ 𝑦𝐵𝑊)) |
| 28 | 27 | exbii 1848 |
. . . 4
⊢
(∃𝑦(〈𝑋, 𝑌〉(2nd ↾ (V ×
V))𝑦 ∧ 𝑦𝐵𝑊) ↔ ∃𝑦(𝑦 = 𝑌 ∧ 𝑦𝐵𝑊)) |
| 29 | | breq1 5146 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝑦𝐵𝑊 ↔ 𝑌𝐵𝑊)) |
| 30 | 9, 29 | ceqsexv 3532 |
. . . 4
⊢
(∃𝑦(𝑦 = 𝑌 ∧ 𝑦𝐵𝑊) ↔ 𝑌𝐵𝑊) |
| 31 | 21, 28, 30 | 3bitri 297 |
. . 3
⊢
(〈𝑋, 𝑌〉(𝐵 ∘ (2nd ↾ (V ×
V)))𝑊 ↔ 𝑌𝐵𝑊) |
| 32 | 20, 31 | anbi12i 628 |
. 2
⊢
((〈𝑋, 𝑌〉(𝐴 ∘ (1st ↾ (V ×
V)))𝑍 ∧ 〈𝑋, 𝑌〉(𝐵 ∘ (2nd ↾ (V ×
V)))𝑊) ↔ (𝑋𝐴𝑍 ∧ 𝑌𝐵𝑊)) |
| 33 | 2, 6, 32 | 3bitri 297 |
1
⊢
(〈𝑋, 𝑌〉pprod(𝐴, 𝐵)〈𝑍, 𝑊〉 ↔ (𝑋𝐴𝑍 ∧ 𝑌𝐵𝑊)) |