Metamath Proof Explorer

Theorem hashunx

Description: The size of the union of disjoint sets is the result of the extended real addition of their sizes, analogous to hashun . (Contributed by Alexander van der Vekens, 21-Dec-2017)

Ref Expression
Assertion hashunx 
|- ( ( A e. V /\ B e. W /\ ( A i^i B ) = (/) ) -> ( # ` ( A u. B ) ) = ( ( # ` A ) +e ( # ` B ) ) )

Proof

Step Hyp Ref Expression
1 hashun 
 |-  ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( # ` ( A u. B ) ) = ( ( # ` A ) + ( # ` B ) ) )
2 1 3expa 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( A i^i B ) = (/) ) -> ( # ` ( A u. B ) ) = ( ( # ` A ) + ( # ` B ) ) )
3 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
4 3 nn0red 
 |-  ( A e. Fin -> ( # ` A ) e. RR )
5 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
6 5 nn0red 
 |-  ( B e. Fin -> ( # ` B ) e. RR )
7 4 6 anim12i 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) e. RR /\ ( # ` B ) e. RR ) )
8 7 adantr 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( A i^i B ) = (/) ) -> ( ( # ` A ) e. RR /\ ( # ` B ) e. RR ) )
9 rexadd 
 |-  ( ( ( # ` A ) e. RR /\ ( # ` B ) e. RR ) -> ( ( # ` A ) +e ( # ` B ) ) = ( ( # ` A ) + ( # ` B ) ) )
10 8 9 syl 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( A i^i B ) = (/) ) -> ( ( # ` A ) +e ( # ` B ) ) = ( ( # ` A ) + ( # ` B ) ) )
11 10 eqcomd 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( A i^i B ) = (/) ) -> ( ( # ` A ) + ( # ` B ) ) = ( ( # ` A ) +e ( # ` B ) ) )
12 2 11 eqtrd 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( A i^i B ) = (/) ) -> ( # ` ( A u. B ) ) = ( ( # ` A ) +e ( # ` B ) ) )
13 12 expcom 
 |-  ( ( A i^i B ) = (/) -> ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A u. B ) ) = ( ( # ` A ) +e ( # ` B ) ) ) )
14 13 3ad2ant3 
 |-  ( ( A e. V /\ B e. W /\ ( A i^i B ) = (/) ) -> ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A u. B ) ) = ( ( # ` A ) +e ( # ` B ) ) ) )
15 unexg 
 |-  ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )
16 unfir 
 |-  ( ( A u. B ) e. Fin -> ( A e. Fin /\ B e. Fin ) )
17 16 con3i 
 |-  ( -. ( A e. Fin /\ B e. Fin ) -> -. ( A u. B ) e. Fin )
18 hashinf 
 |-  ( ( ( A u. B ) e. _V /\ -. ( A u. B ) e. Fin ) -> ( # ` ( A u. B ) ) = +oo )
19 15 17 18 syl2anr 
 |-  ( ( -. ( A e. Fin /\ B e. Fin ) /\ ( A e. V /\ B e. W ) ) -> ( # ` ( A u. B ) ) = +oo )
20 ianor 
 |-  ( -. ( A e. Fin /\ B e. Fin ) <-> ( -. A e. Fin \/ -. B e. Fin ) )
21 simprl 
 |-  ( ( -. A e. Fin /\ ( A e. V /\ B e. W ) ) -> A e. V )
22 simprr 
 |-  ( ( -. A e. Fin /\ ( A e. V /\ B e. W ) ) -> B e. W )
23 hashnfinnn0 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( # ` A ) e/ NN0 )
24 23 ex 
 |-  ( A e. V -> ( -. A e. Fin -> ( # ` A ) e/ NN0 ) )
25 24 adantr 
 |-  ( ( A e. V /\ B e. W ) -> ( -. A e. Fin -> ( # ` A ) e/ NN0 ) )
26 25 impcom 
 |-  ( ( -. A e. Fin /\ ( A e. V /\ B e. W ) ) -> ( # ` A ) e/ NN0 )
27 hashinfxadd 
 |-  ( ( A e. V /\ B e. W /\ ( # ` A ) e/ NN0 ) -> ( ( # ` A ) +e ( # ` B ) ) = +oo )
28 21 22 26 27 syl3anc 
 |-  ( ( -. A e. Fin /\ ( A e. V /\ B e. W ) ) -> ( ( # ` A ) +e ( # ` B ) ) = +oo )
29 28 eqcomd 
 |-  ( ( -. A e. Fin /\ ( A e. V /\ B e. W ) ) -> +oo = ( ( # ` A ) +e ( # ` B ) ) )
30 29 ex 
 |-  ( -. A e. Fin -> ( ( A e. V /\ B e. W ) -> +oo = ( ( # ` A ) +e ( # ` B ) ) ) )
31 hashxrcl 
 |-  ( A e. V -> ( # ` A ) e. RR* )
32 hashxrcl 
 |-  ( B e. W -> ( # ` B ) e. RR* )
33 31 32 anim12i 
 |-  ( ( A e. V /\ B e. W ) -> ( ( # ` A ) e. RR* /\ ( # ` B ) e. RR* ) )
34 33 adantl 
 |-  ( ( -. B e. Fin /\ ( A e. V /\ B e. W ) ) -> ( ( # ` A ) e. RR* /\ ( # ` B ) e. RR* ) )
35 xaddcom 
 |-  ( ( ( # ` A ) e. RR* /\ ( # ` B ) e. RR* ) -> ( ( # ` A ) +e ( # ` B ) ) = ( ( # ` B ) +e ( # ` A ) ) )
36 34 35 syl 
 |-  ( ( -. B e. Fin /\ ( A e. V /\ B e. W ) ) -> ( ( # ` A ) +e ( # ` B ) ) = ( ( # ` B ) +e ( # ` A ) ) )
37 simprr 
 |-  ( ( -. B e. Fin /\ ( A e. V /\ B e. W ) ) -> B e. W )
38 simprl 
 |-  ( ( -. B e. Fin /\ ( A e. V /\ B e. W ) ) -> A e. V )
39 hashnfinnn0 
 |-  ( ( B e. W /\ -. B e. Fin ) -> ( # ` B ) e/ NN0 )
40 39 ex 
 |-  ( B e. W -> ( -. B e. Fin -> ( # ` B ) e/ NN0 ) )
41 40 adantl 
 |-  ( ( A e. V /\ B e. W ) -> ( -. B e. Fin -> ( # ` B ) e/ NN0 ) )
42 41 impcom 
 |-  ( ( -. B e. Fin /\ ( A e. V /\ B e. W ) ) -> ( # ` B ) e/ NN0 )
43 hashinfxadd 
 |-  ( ( B e. W /\ A e. V /\ ( # ` B ) e/ NN0 ) -> ( ( # ` B ) +e ( # ` A ) ) = +oo )
44 37 38 42 43 syl3anc 
 |-  ( ( -. B e. Fin /\ ( A e. V /\ B e. W ) ) -> ( ( # ` B ) +e ( # ` A ) ) = +oo )
45 36 44 eqtrd 
 |-  ( ( -. B e. Fin /\ ( A e. V /\ B e. W ) ) -> ( ( # ` A ) +e ( # ` B ) ) = +oo )
46 45 eqcomd 
 |-  ( ( -. B e. Fin /\ ( A e. V /\ B e. W ) ) -> +oo = ( ( # ` A ) +e ( # ` B ) ) )
47 46 ex 
 |-  ( -. B e. Fin -> ( ( A e. V /\ B e. W ) -> +oo = ( ( # ` A ) +e ( # ` B ) ) ) )
48 30 47 jaoi 
 |-  ( ( -. A e. Fin \/ -. B e. Fin ) -> ( ( A e. V /\ B e. W ) -> +oo = ( ( # ` A ) +e ( # ` B ) ) ) )
49 20 48 sylbi 
 |-  ( -. ( A e. Fin /\ B e. Fin ) -> ( ( A e. V /\ B e. W ) -> +oo = ( ( # ` A ) +e ( # ` B ) ) ) )
50 49 imp 
 |-  ( ( -. ( A e. Fin /\ B e. Fin ) /\ ( A e. V /\ B e. W ) ) -> +oo = ( ( # ` A ) +e ( # ` B ) ) )
51 19 50 eqtrd 
 |-  ( ( -. ( A e. Fin /\ B e. Fin ) /\ ( A e. V /\ B e. W ) ) -> ( # ` ( A u. B ) ) = ( ( # ` A ) +e ( # ` B ) ) )
52 51 expcom 
 |-  ( ( A e. V /\ B e. W ) -> ( -. ( A e. Fin /\ B e. Fin ) -> ( # ` ( A u. B ) ) = ( ( # ` A ) +e ( # ` B ) ) ) )
53 52 3adant3 
 |-  ( ( A e. V /\ B e. W /\ ( A i^i B ) = (/) ) -> ( -. ( A e. Fin /\ B e. Fin ) -> ( # ` ( A u. B ) ) = ( ( # ` A ) +e ( # ` B ) ) ) )
54 14 53 pm2.61d 
 |-  ( ( A e. V /\ B e. W /\ ( A i^i B ) = (/) ) -> ( # ` ( A u. B ) ) = ( ( # ` A ) +e ( # ` B ) ) )