Step |
Hyp |
Ref |
Expression |
1 |
|
tc2.1 |
|- A e. _V |
2 |
1
|
ssex |
|- ( B C_ A -> B e. _V ) |
3 |
|
tcvalg |
|- ( B e. _V -> ( TC ` B ) = |^| { x | ( B C_ x /\ Tr x ) } ) |
4 |
2 3
|
syl |
|- ( B C_ A -> ( TC ` B ) = |^| { x | ( B C_ x /\ Tr x ) } ) |
5 |
|
sstr2 |
|- ( B C_ A -> ( A C_ x -> B C_ x ) ) |
6 |
5
|
anim1d |
|- ( B C_ A -> ( ( A C_ x /\ Tr x ) -> ( B C_ x /\ Tr x ) ) ) |
7 |
6
|
ss2abdv |
|- ( B C_ A -> { x | ( A C_ x /\ Tr x ) } C_ { x | ( B C_ x /\ Tr x ) } ) |
8 |
|
intss |
|- ( { x | ( A C_ x /\ Tr x ) } C_ { x | ( B C_ x /\ Tr x ) } -> |^| { x | ( B C_ x /\ Tr x ) } C_ |^| { x | ( A C_ x /\ Tr x ) } ) |
9 |
7 8
|
syl |
|- ( B C_ A -> |^| { x | ( B C_ x /\ Tr x ) } C_ |^| { x | ( A C_ x /\ Tr x ) } ) |
10 |
|
tcvalg |
|- ( A e. _V -> ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) } ) |
11 |
1 10
|
ax-mp |
|- ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) } |
12 |
9 11
|
sseqtrrdi |
|- ( B C_ A -> |^| { x | ( B C_ x /\ Tr x ) } C_ ( TC ` A ) ) |
13 |
4 12
|
eqsstrd |
|- ( B C_ A -> ( TC ` B ) C_ ( TC ` A ) ) |