Step |
Hyp |
Ref |
Expression |
1 |
|
carsgval.1 |
|- ( ph -> O e. V ) |
2 |
|
carsgval.2 |
|- ( ph -> M : ~P O --> ( 0 [,] +oo ) ) |
3 |
|
difelcarsg.1 |
|- ( ph -> A e. ( toCaraSiga ` M ) ) |
4 |
|
inelcarsg.1 |
|- ( ( ph /\ a e. ~P O /\ b e. ~P O ) -> ( M ` ( a u. b ) ) <_ ( ( M ` a ) +e ( M ` b ) ) ) |
5 |
|
inelcarsg.2 |
|- ( ph -> B e. ( toCaraSiga ` M ) ) |
6 |
1 2 3
|
elcarsgss |
|- ( ph -> A C_ O ) |
7 |
|
dfss4 |
|- ( A C_ O <-> ( O \ ( O \ A ) ) = A ) |
8 |
6 7
|
sylib |
|- ( ph -> ( O \ ( O \ A ) ) = A ) |
9 |
1 2 5
|
elcarsgss |
|- ( ph -> B C_ O ) |
10 |
|
dfss4 |
|- ( B C_ O <-> ( O \ ( O \ B ) ) = B ) |
11 |
9 10
|
sylib |
|- ( ph -> ( O \ ( O \ B ) ) = B ) |
12 |
8 11
|
uneq12d |
|- ( ph -> ( ( O \ ( O \ A ) ) u. ( O \ ( O \ B ) ) ) = ( A u. B ) ) |
13 |
|
difindi |
|- ( O \ ( ( O \ A ) i^i ( O \ B ) ) ) = ( ( O \ ( O \ A ) ) u. ( O \ ( O \ B ) ) ) |
14 |
1 2 3
|
difelcarsg |
|- ( ph -> ( O \ A ) e. ( toCaraSiga ` M ) ) |
15 |
1 2 5
|
difelcarsg |
|- ( ph -> ( O \ B ) e. ( toCaraSiga ` M ) ) |
16 |
1 2 14 4 15
|
inelcarsg |
|- ( ph -> ( ( O \ A ) i^i ( O \ B ) ) e. ( toCaraSiga ` M ) ) |
17 |
1 2 16
|
difelcarsg |
|- ( ph -> ( O \ ( ( O \ A ) i^i ( O \ B ) ) ) e. ( toCaraSiga ` M ) ) |
18 |
13 17
|
eqeltrrid |
|- ( ph -> ( ( O \ ( O \ A ) ) u. ( O \ ( O \ B ) ) ) e. ( toCaraSiga ` M ) ) |
19 |
12 18
|
eqeltrrd |
|- ( ph -> ( A u. B ) e. ( toCaraSiga ` M ) ) |