Step | Hyp | Ref
| Expression |
1 | | df-pprod 34896 |
. 2
⊢
pprod(𝐴, 𝐵) = ((𝐴 ∘ (1st ↾ (V ×
V))) ⊗ (𝐵 ∘
(2nd ↾ (V × V)))) |
2 | | txprel 34920 |
. . 3
⊢ Rel
((𝐴 ∘ (1st
↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V ×
V)))) |
3 | | txpss3v 34919 |
. . . . . . 7
⊢ ((𝐴 ∘ (1st ↾
(V × V))) ⊗ (𝐵
∘ (2nd ↾ (V × V)))) ⊆ (V × (V ×
V)) |
4 | 3 | sseli 3978 |
. . . . . 6
⊢
(⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∘ (1st ↾
(V × V))) ⊗ (𝐵
∘ (2nd ↾ (V × V)))) → ⟨𝑥, 𝑦⟩ ∈ (V × (V ×
V))) |
5 | | opelxp2 5719 |
. . . . . 6
⊢
(⟨𝑥, 𝑦⟩ ∈ (V × (V
× V)) → 𝑦 ∈
(V × V)) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢
(⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∘ (1st ↾
(V × V))) ⊗ (𝐵
∘ (2nd ↾ (V × V)))) → 𝑦 ∈ (V × V)) |
7 | | elvv 5750 |
. . . . . 6
⊢ (𝑦 ∈ (V × V) ↔
∃𝑧∃𝑤 𝑦 = ⟨𝑧, 𝑤⟩) |
8 | | opeq2 4874 |
. . . . . . . . 9
⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ⟨𝑧, 𝑤⟩⟩) |
9 | 8 | eleq1d 2818 |
. . . . . . . 8
⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∘ (1st ↾ (V ×
V))) ⊗ (𝐵 ∘
(2nd ↾ (V × V)))) ↔ ⟨𝑥, ⟨𝑧, 𝑤⟩⟩ ∈ ((𝐴 ∘ (1st ↾ (V ×
V))) ⊗ (𝐵 ∘
(2nd ↾ (V × V)))))) |
10 | | df-br 5149 |
. . . . . . . . 9
⊢ (𝑥((𝐴 ∘ (1st ↾ (V ×
V))) ⊗ (𝐵 ∘
(2nd ↾ (V × V))))⟨𝑧, 𝑤⟩ ↔ ⟨𝑥, ⟨𝑧, 𝑤⟩⟩ ∈ ((𝐴 ∘ (1st ↾ (V ×
V))) ⊗ (𝐵 ∘
(2nd ↾ (V × V))))) |
11 | | vex 3478 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
12 | | vex 3478 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
13 | | vex 3478 |
. . . . . . . . . . 11
⊢ 𝑤 ∈ V |
14 | 11, 12, 13 | brtxp 34921 |
. . . . . . . . . 10
⊢ (𝑥((𝐴 ∘ (1st ↾ (V ×
V))) ⊗ (𝐵 ∘
(2nd ↾ (V × V))))⟨𝑧, 𝑤⟩ ↔ (𝑥(𝐴 ∘ (1st ↾ (V ×
V)))𝑧 ∧ 𝑥(𝐵 ∘ (2nd ↾ (V ×
V)))𝑤)) |
15 | 11, 12 | brco 5870 |
. . . . . . . . . . . 12
⊢ (𝑥(𝐴 ∘ (1st ↾ (V ×
V)))𝑧 ↔ ∃𝑦(𝑥(1st ↾ (V × V))𝑦 ∧ 𝑦𝐴𝑧)) |
16 | | vex 3478 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
17 | 16 | brresi 5990 |
. . . . . . . . . . . . . . 15
⊢ (𝑥(1st ↾ (V
× V))𝑦 ↔ (𝑥 ∈ (V × V) ∧
𝑥1st 𝑦)) |
18 | 17 | simplbi 498 |
. . . . . . . . . . . . . 14
⊢ (𝑥(1st ↾ (V
× V))𝑦 → 𝑥 ∈ (V ×
V)) |
19 | 18 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑥(1st ↾ (V
× V))𝑦 ∧ 𝑦𝐴𝑧) → 𝑥 ∈ (V × V)) |
20 | 19 | exlimiv 1933 |
. . . . . . . . . . . 12
⊢
(∃𝑦(𝑥(1st ↾ (V
× V))𝑦 ∧ 𝑦𝐴𝑧) → 𝑥 ∈ (V × V)) |
21 | 15, 20 | sylbi 216 |
. . . . . . . . . . 11
⊢ (𝑥(𝐴 ∘ (1st ↾ (V ×
V)))𝑧 → 𝑥 ∈ (V ×
V)) |
22 | 21 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑥(𝐴 ∘ (1st ↾ (V ×
V)))𝑧 ∧ 𝑥(𝐵 ∘ (2nd ↾ (V ×
V)))𝑤) → 𝑥 ∈ (V ×
V)) |
23 | 14, 22 | sylbi 216 |
. . . . . . . . 9
⊢ (𝑥((𝐴 ∘ (1st ↾ (V ×
V))) ⊗ (𝐵 ∘
(2nd ↾ (V × V))))⟨𝑧, 𝑤⟩ → 𝑥 ∈ (V × V)) |
24 | 10, 23 | sylbir 234 |
. . . . . . . 8
⊢
(⟨𝑥,
⟨𝑧, 𝑤⟩⟩ ∈ ((𝐴 ∘ (1st ↾ (V ×
V))) ⊗ (𝐵 ∘
(2nd ↾ (V × V)))) → 𝑥 ∈ (V × V)) |
25 | 9, 24 | syl6bi 252 |
. . . . . . 7
⊢ (𝑦 = ⟨𝑧, 𝑤⟩ → (⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∘ (1st ↾ (V ×
V))) ⊗ (𝐵 ∘
(2nd ↾ (V × V)))) → 𝑥 ∈ (V × V))) |
26 | 25 | exlimivv 1935 |
. . . . . 6
⊢
(∃𝑧∃𝑤 𝑦 = ⟨𝑧, 𝑤⟩ → (⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∘ (1st ↾ (V ×
V))) ⊗ (𝐵 ∘
(2nd ↾ (V × V)))) → 𝑥 ∈ (V × V))) |
27 | 7, 26 | sylbi 216 |
. . . . 5
⊢ (𝑦 ∈ (V × V) →
(⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∘ (1st ↾
(V × V))) ⊗ (𝐵
∘ (2nd ↾ (V × V)))) → 𝑥 ∈ (V × V))) |
28 | 6, 27 | mpcom 38 |
. . . 4
⊢
(⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∘ (1st ↾
(V × V))) ⊗ (𝐵
∘ (2nd ↾ (V × V)))) → 𝑥 ∈ (V × V)) |
29 | 28, 6 | opelxpd 5715 |
. . 3
⊢
(⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∘ (1st ↾
(V × V))) ⊗ (𝐵
∘ (2nd ↾ (V × V)))) → ⟨𝑥, 𝑦⟩ ∈ ((V × V) × (V
× V))) |
30 | 2, 29 | relssi 5787 |
. 2
⊢ ((𝐴 ∘ (1st ↾
(V × V))) ⊗ (𝐵
∘ (2nd ↾ (V × V)))) ⊆ ((V × V) ×
(V × V)) |
31 | 1, 30 | eqsstri 4016 |
1
⊢
pprod(𝐴, 𝐵) ⊆ ((V × V) ×
(V × V)) |