Step | Hyp | Ref
| Expression |
1 | | pjpm.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
2 | | pjpm.l |
. . . . 5
⊢ 𝐿 = (LSubSp‘𝑊) |
3 | | eqid 2622 |
. . . . 5
⊢
(ocv‘𝑊) =
(ocv‘𝑊) |
4 | | eqid 2622 |
. . . . 5
⊢
(proj1‘𝑊) = (proj1‘𝑊) |
5 | | pjpm.k |
. . . . 5
⊢ 𝐾 = (proj‘𝑊) |
6 | 1, 2, 3, 4, 5 | pjfval 20050 |
. . . 4
⊢ 𝐾 = ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ∩ (V × (𝑉 ↑𝑚 𝑉))) |
7 | | inss1 3833 |
. . . 4
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ∩ (V × (𝑉 ↑𝑚 𝑉))) ⊆ (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) |
8 | 6, 7 | eqsstri 3635 |
. . 3
⊢ 𝐾 ⊆ (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) |
9 | | funmpt 5926 |
. . 3
⊢ Fun
(𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) |
10 | | funss 5907 |
. . 3
⊢ (𝐾 ⊆ (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) → (Fun (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) → Fun 𝐾)) |
11 | 8, 9, 10 | mp2 9 |
. 2
⊢ Fun 𝐾 |
12 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) = (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) |
13 | | ovexd 6680 |
. . . . . 6
⊢ (𝑥 ∈ 𝐿 → (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥)) ∈ V) |
14 | 12, 13 | fmpti 6383 |
. . . . 5
⊢ (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))):𝐿⟶V |
15 | | fssxp 6060 |
. . . . 5
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))):𝐿⟶V → (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ⊆ (𝐿 × V)) |
16 | | ssrin 3838 |
. . . . 5
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ⊆ (𝐿 × V) → ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ∩ (V × (𝑉 ↑𝑚 𝑉))) ⊆ ((𝐿 × V) ∩ (V × (𝑉 ↑𝑚
𝑉)))) |
17 | 14, 15, 16 | mp2b 10 |
. . . 4
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ∩ (V × (𝑉 ↑𝑚 𝑉))) ⊆ ((𝐿 × V) ∩ (V × (𝑉 ↑𝑚
𝑉))) |
18 | 6, 17 | eqsstri 3635 |
. . 3
⊢ 𝐾 ⊆ ((𝐿 × V) ∩ (V × (𝑉 ↑𝑚
𝑉))) |
19 | | inxp 5254 |
. . . 4
⊢ ((𝐿 × V) ∩ (V ×
(𝑉
↑𝑚 𝑉))) = ((𝐿 ∩ V) × (V ∩ (𝑉 ↑𝑚
𝑉))) |
20 | | inv1 3970 |
. . . . 5
⊢ (𝐿 ∩ V) = 𝐿 |
21 | | incom 3805 |
. . . . . 6
⊢ (V ∩
(𝑉
↑𝑚 𝑉)) = ((𝑉 ↑𝑚 𝑉) ∩ V) |
22 | | inv1 3970 |
. . . . . 6
⊢ ((𝑉 ↑𝑚
𝑉) ∩ V) = (𝑉 ↑𝑚
𝑉) |
23 | 21, 22 | eqtri 2644 |
. . . . 5
⊢ (V ∩
(𝑉
↑𝑚 𝑉)) = (𝑉 ↑𝑚 𝑉) |
24 | 20, 23 | xpeq12i 5137 |
. . . 4
⊢ ((𝐿 ∩ V) × (V ∩
(𝑉
↑𝑚 𝑉))) = (𝐿 × (𝑉 ↑𝑚 𝑉)) |
25 | 19, 24 | eqtri 2644 |
. . 3
⊢ ((𝐿 × V) ∩ (V ×
(𝑉
↑𝑚 𝑉))) = (𝐿 × (𝑉 ↑𝑚 𝑉)) |
26 | 18, 25 | sseqtri 3637 |
. 2
⊢ 𝐾 ⊆ (𝐿 × (𝑉 ↑𝑚 𝑉)) |
27 | | ovex 6678 |
. . 3
⊢ (𝑉 ↑𝑚
𝑉) ∈
V |
28 | | fvex 6201 |
. . . 4
⊢
(LSubSp‘𝑊)
∈ V |
29 | 2, 28 | eqeltri 2697 |
. . 3
⊢ 𝐿 ∈ V |
30 | 27, 29 | elpm 7888 |
. 2
⊢ (𝐾 ∈ ((𝑉 ↑𝑚 𝑉) ↑pm
𝐿) ↔ (Fun 𝐾 ∧ 𝐾 ⊆ (𝐿 × (𝑉 ↑𝑚 𝑉)))) |
31 | 11, 26, 30 | mpbir2an 955 |
1
⊢ 𝐾 ∈ ((𝑉 ↑𝑚 𝑉) ↑pm
𝐿) |