| Step | Hyp | Ref
| Expression |
| 1 | | pjpm.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
| 2 | | pjpm.l |
. . . . 5
⊢ 𝐿 = (LSubSp‘𝑊) |
| 3 | | eqid 2737 |
. . . . 5
⊢
(ocv‘𝑊) =
(ocv‘𝑊) |
| 4 | | eqid 2737 |
. . . . 5
⊢
(proj1‘𝑊) = (proj1‘𝑊) |
| 5 | | pjpm.k |
. . . . 5
⊢ 𝐾 = (proj‘𝑊) |
| 6 | 1, 2, 3, 4, 5 | pjfval 21726 |
. . . 4
⊢ 𝐾 = ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) |
| 7 | | inss1 4237 |
. . . 4
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) ⊆ (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) |
| 8 | 6, 7 | eqsstri 4030 |
. . 3
⊢ 𝐾 ⊆ (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) |
| 9 | | funmpt 6604 |
. . 3
⊢ Fun
(𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) |
| 10 | | funss 6585 |
. . 3
⊢ (𝐾 ⊆ (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) → (Fun (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) → Fun 𝐾)) |
| 11 | 8, 9, 10 | mp2 9 |
. 2
⊢ Fun 𝐾 |
| 12 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) = (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) |
| 13 | | ovexd 7466 |
. . . . . 6
⊢ (𝑥 ∈ 𝐿 → (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥)) ∈ V) |
| 14 | 12, 13 | fmpti 7132 |
. . . . 5
⊢ (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))):𝐿⟶V |
| 15 | | fssxp 6763 |
. . . . 5
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))):𝐿⟶V → (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ⊆ (𝐿 × V)) |
| 16 | | ssrin 4242 |
. . . . 5
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ⊆ (𝐿 × V) → ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) ⊆ ((𝐿 × V) ∩ (V × (𝑉 ↑m 𝑉)))) |
| 17 | 14, 15, 16 | mp2b 10 |
. . . 4
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) ⊆ ((𝐿 × V) ∩ (V × (𝑉 ↑m 𝑉))) |
| 18 | 6, 17 | eqsstri 4030 |
. . 3
⊢ 𝐾 ⊆ ((𝐿 × V) ∩ (V × (𝑉 ↑m 𝑉))) |
| 19 | | inxp 5842 |
. . . 4
⊢ ((𝐿 × V) ∩ (V ×
(𝑉 ↑m 𝑉))) = ((𝐿 ∩ V) × (V ∩ (𝑉 ↑m 𝑉))) |
| 20 | | inv1 4398 |
. . . . 5
⊢ (𝐿 ∩ V) = 𝐿 |
| 21 | | incom 4209 |
. . . . . 6
⊢ (V ∩
(𝑉 ↑m 𝑉)) = ((𝑉 ↑m 𝑉) ∩ V) |
| 22 | | inv1 4398 |
. . . . . 6
⊢ ((𝑉 ↑m 𝑉) ∩ V) = (𝑉 ↑m 𝑉) |
| 23 | 21, 22 | eqtri 2765 |
. . . . 5
⊢ (V ∩
(𝑉 ↑m 𝑉)) = (𝑉 ↑m 𝑉) |
| 24 | 20, 23 | xpeq12i 5713 |
. . . 4
⊢ ((𝐿 ∩ V) × (V ∩
(𝑉 ↑m 𝑉))) = (𝐿 × (𝑉 ↑m 𝑉)) |
| 25 | 19, 24 | eqtri 2765 |
. . 3
⊢ ((𝐿 × V) ∩ (V ×
(𝑉 ↑m 𝑉))) = (𝐿 × (𝑉 ↑m 𝑉)) |
| 26 | 18, 25 | sseqtri 4032 |
. 2
⊢ 𝐾 ⊆ (𝐿 × (𝑉 ↑m 𝑉)) |
| 27 | | ovex 7464 |
. . 3
⊢ (𝑉 ↑m 𝑉) ∈ V |
| 28 | 2 | fvexi 6920 |
. . 3
⊢ 𝐿 ∈ V |
| 29 | 27, 28 | elpm 8913 |
. 2
⊢ (𝐾 ∈ ((𝑉 ↑m 𝑉) ↑pm 𝐿) ↔ (Fun 𝐾 ∧ 𝐾 ⊆ (𝐿 × (𝑉 ↑m 𝑉)))) |
| 30 | 11, 26, 29 | mpbir2an 711 |
1
⊢ 𝐾 ∈ ((𝑉 ↑m 𝑉) ↑pm 𝐿) |