Step |
Hyp |
Ref |
Expression |
0 |
|
clcv |
|-
|
1 |
|
vw |
|- w |
2 |
|
cvv |
|- _V |
3 |
|
vt |
|- t |
4 |
|
vu |
|- u |
5 |
3
|
cv |
|- t |
6 |
|
clss |
|- LSubSp |
7 |
1
|
cv |
|- w |
8 |
7 6
|
cfv |
|- ( LSubSp ` w ) |
9 |
5 8
|
wcel |
|- t e. ( LSubSp ` w ) |
10 |
4
|
cv |
|- u |
11 |
10 8
|
wcel |
|- u e. ( LSubSp ` w ) |
12 |
9 11
|
wa |
|- ( t e. ( LSubSp ` w ) /\ u e. ( LSubSp ` w ) ) |
13 |
5 10
|
wpss |
|- t C. u |
14 |
|
vs |
|- s |
15 |
14
|
cv |
|- s |
16 |
5 15
|
wpss |
|- t C. s |
17 |
15 10
|
wpss |
|- s C. u |
18 |
16 17
|
wa |
|- ( t C. s /\ s C. u ) |
19 |
18 14 8
|
wrex |
|- E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) |
20 |
19
|
wn |
|- -. E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) |
21 |
13 20
|
wa |
|- ( t C. u /\ -. E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) ) |
22 |
12 21
|
wa |
|- ( ( t e. ( LSubSp ` w ) /\ u e. ( LSubSp ` w ) ) /\ ( t C. u /\ -. E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) ) ) |
23 |
22 3 4
|
copab |
|- { <. t , u >. | ( ( t e. ( LSubSp ` w ) /\ u e. ( LSubSp ` w ) ) /\ ( t C. u /\ -. E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) ) ) } |
24 |
1 2 23
|
cmpt |
|- ( w e. _V |-> { <. t , u >. | ( ( t e. ( LSubSp ` w ) /\ u e. ( LSubSp ` w ) ) /\ ( t C. u /\ -. E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) ) ) } ) |
25 |
0 24
|
wceq |
|- { <. t , u >. | ( ( t e. ( LSubSp ` w ) /\ u e. ( LSubSp ` w ) ) /\ ( t C. u /\ -. E. s e. ( LSubSp ` w ) ( t C. s /\ s C. u ) ) ) } ) |