Step |
Hyp |
Ref |
Expression |
1 |
|
undif2 |
|- ( A u. ( B \ A ) ) = ( A u. B ) |
2 |
1
|
fveq2i |
|- ( # ` ( A u. ( B \ A ) ) ) = ( # ` ( A u. B ) ) |
3 |
|
diffi |
|- ( B e. Fin -> ( B \ A ) e. Fin ) |
4 |
|
disjdif |
|- ( A i^i ( B \ A ) ) = (/) |
5 |
|
hashun |
|- ( ( A e. Fin /\ ( B \ A ) e. Fin /\ ( A i^i ( B \ A ) ) = (/) ) -> ( # ` ( A u. ( B \ A ) ) ) = ( ( # ` A ) + ( # ` ( B \ A ) ) ) ) |
6 |
4 5
|
mp3an3 |
|- ( ( A e. Fin /\ ( B \ A ) e. Fin ) -> ( # ` ( A u. ( B \ A ) ) ) = ( ( # ` A ) + ( # ` ( B \ A ) ) ) ) |
7 |
3 6
|
sylan2 |
|- ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A u. ( B \ A ) ) ) = ( ( # ` A ) + ( # ` ( B \ A ) ) ) ) |
8 |
2 7
|
eqtr3id |
|- ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A u. B ) ) = ( ( # ` A ) + ( # ` ( B \ A ) ) ) ) |
9 |
3
|
adantl |
|- ( ( A e. Fin /\ B e. Fin ) -> ( B \ A ) e. Fin ) |
10 |
|
hashcl |
|- ( ( B \ A ) e. Fin -> ( # ` ( B \ A ) ) e. NN0 ) |
11 |
9 10
|
syl |
|- ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( B \ A ) ) e. NN0 ) |
12 |
11
|
nn0red |
|- ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( B \ A ) ) e. RR ) |
13 |
|
hashcl |
|- ( B e. Fin -> ( # ` B ) e. NN0 ) |
14 |
13
|
adantl |
|- ( ( A e. Fin /\ B e. Fin ) -> ( # ` B ) e. NN0 ) |
15 |
14
|
nn0red |
|- ( ( A e. Fin /\ B e. Fin ) -> ( # ` B ) e. RR ) |
16 |
|
hashcl |
|- ( A e. Fin -> ( # ` A ) e. NN0 ) |
17 |
16
|
adantr |
|- ( ( A e. Fin /\ B e. Fin ) -> ( # ` A ) e. NN0 ) |
18 |
17
|
nn0red |
|- ( ( A e. Fin /\ B e. Fin ) -> ( # ` A ) e. RR ) |
19 |
|
simpr |
|- ( ( A e. Fin /\ B e. Fin ) -> B e. Fin ) |
20 |
|
difss |
|- ( B \ A ) C_ B |
21 |
|
ssdomg |
|- ( B e. Fin -> ( ( B \ A ) C_ B -> ( B \ A ) ~<_ B ) ) |
22 |
19 20 21
|
mpisyl |
|- ( ( A e. Fin /\ B e. Fin ) -> ( B \ A ) ~<_ B ) |
23 |
|
hashdom |
|- ( ( ( B \ A ) e. Fin /\ B e. Fin ) -> ( ( # ` ( B \ A ) ) <_ ( # ` B ) <-> ( B \ A ) ~<_ B ) ) |
24 |
9 23
|
sylancom |
|- ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` ( B \ A ) ) <_ ( # ` B ) <-> ( B \ A ) ~<_ B ) ) |
25 |
22 24
|
mpbird |
|- ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( B \ A ) ) <_ ( # ` B ) ) |
26 |
12 15 18 25
|
leadd2dd |
|- ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) + ( # ` ( B \ A ) ) ) <_ ( ( # ` A ) + ( # ` B ) ) ) |
27 |
8 26
|
eqbrtrd |
|- ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A u. B ) ) <_ ( ( # ` A ) + ( # ` B ) ) ) |