Step |
Hyp |
Ref |
Expression |
0 |
|
clcv |
⊢ ⋖L |
1 |
|
vw |
⊢ 𝑤 |
2 |
|
cvv |
⊢ V |
3 |
|
vt |
⊢ 𝑡 |
4 |
|
vu |
⊢ 𝑢 |
5 |
3
|
cv |
⊢ 𝑡 |
6 |
|
clss |
⊢ LSubSp |
7 |
1
|
cv |
⊢ 𝑤 |
8 |
7 6
|
cfv |
⊢ ( LSubSp ‘ 𝑤 ) |
9 |
5 8
|
wcel |
⊢ 𝑡 ∈ ( LSubSp ‘ 𝑤 ) |
10 |
4
|
cv |
⊢ 𝑢 |
11 |
10 8
|
wcel |
⊢ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) |
12 |
9 11
|
wa |
⊢ ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) |
13 |
5 10
|
wpss |
⊢ 𝑡 ⊊ 𝑢 |
14 |
|
vs |
⊢ 𝑠 |
15 |
14
|
cv |
⊢ 𝑠 |
16 |
5 15
|
wpss |
⊢ 𝑡 ⊊ 𝑠 |
17 |
15 10
|
wpss |
⊢ 𝑠 ⊊ 𝑢 |
18 |
16 17
|
wa |
⊢ ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) |
19 |
18 14 8
|
wrex |
⊢ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) |
20 |
19
|
wn |
⊢ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) |
21 |
13 20
|
wa |
⊢ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) |
22 |
12 21
|
wa |
⊢ ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) |
23 |
22 3 4
|
copab |
⊢ { 〈 𝑡 , 𝑢 〉 ∣ ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } |
24 |
1 2 23
|
cmpt |
⊢ ( 𝑤 ∈ V ↦ { 〈 𝑡 , 𝑢 〉 ∣ ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } ) |
25 |
0 24
|
wceq |
⊢ ⋖L = ( 𝑤 ∈ V ↦ { 〈 𝑡 , 𝑢 〉 ∣ ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } ) |