Step |
Hyp |
Ref |
Expression |
1 |
|
spansnpj.1 |
|- A C_ ~H |
2 |
|
spansnpj.2 |
|- B e. ~H |
3 |
|
ococss |
|- ( A C_ ~H -> A C_ ( _|_ ` ( _|_ ` A ) ) ) |
4 |
1 3
|
ax-mp |
|- A C_ ( _|_ ` ( _|_ ` A ) ) |
5 |
|
occl |
|- ( A C_ ~H -> ( _|_ ` A ) e. CH ) |
6 |
1 5
|
ax-mp |
|- ( _|_ ` A ) e. CH |
7 |
6
|
chssii |
|- ( _|_ ` A ) C_ ~H |
8 |
6 2
|
pjclii |
|- ( ( projh ` ( _|_ ` A ) ) ` B ) e. ( _|_ ` A ) |
9 |
|
snssi |
|- ( ( ( projh ` ( _|_ ` A ) ) ` B ) e. ( _|_ ` A ) -> { ( ( projh ` ( _|_ ` A ) ) ` B ) } C_ ( _|_ ` A ) ) |
10 |
8 9
|
ax-mp |
|- { ( ( projh ` ( _|_ ` A ) ) ` B ) } C_ ( _|_ ` A ) |
11 |
|
spanss |
|- ( ( ( _|_ ` A ) C_ ~H /\ { ( ( projh ` ( _|_ ` A ) ) ` B ) } C_ ( _|_ ` A ) ) -> ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) C_ ( span ` ( _|_ ` A ) ) ) |
12 |
7 10 11
|
mp2an |
|- ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) C_ ( span ` ( _|_ ` A ) ) |
13 |
6
|
chshii |
|- ( _|_ ` A ) e. SH |
14 |
|
spanid |
|- ( ( _|_ ` A ) e. SH -> ( span ` ( _|_ ` A ) ) = ( _|_ ` A ) ) |
15 |
13 14
|
ax-mp |
|- ( span ` ( _|_ ` A ) ) = ( _|_ ` A ) |
16 |
12 15
|
sseqtri |
|- ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) C_ ( _|_ ` A ) |
17 |
6 2
|
pjhclii |
|- ( ( projh ` ( _|_ ` A ) ) ` B ) e. ~H |
18 |
17
|
spansnchi |
|- ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) e. CH |
19 |
18 6
|
chsscon3i |
|- ( ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) C_ ( _|_ ` A ) <-> ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) ) |
20 |
16 19
|
mpbi |
|- ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) |
21 |
4 20
|
sstri |
|- A C_ ( _|_ ` ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) |