Metamath Proof Explorer

Theorem hasheuni

Description: The cardinality of a disjoint union, not necessarily finite. cf. hashuni . (Contributed by Thierry Arnoux, 19-Nov-2016) (Revised by Thierry Arnoux, 2-Jan-2017) (Revised by Thierry Arnoux, 20-Jun-2017)

Ref Expression
Assertion hasheuni 
|- ( ( A e. V /\ Disj_ x e. A x ) -> ( # ` U. A ) = sum* x e. A ( # ` x ) )

Proof

Step Hyp Ref Expression
1 nfdisj1 
 |-  F/ x Disj_ x e. A x
2 nfv 
 |-  F/ x A e. Fin
3 nfv 
 |-  F/ x A C_ Fin
4 1 2 3 nf3an 
 |-  F/ x ( Disj_ x e. A x /\ A e. Fin /\ A C_ Fin )
5 simp2 
 |-  ( ( Disj_ x e. A x /\ A e. Fin /\ A C_ Fin ) -> A e. Fin )
6 simp3 
 |-  ( ( Disj_ x e. A x /\ A e. Fin /\ A C_ Fin ) -> A C_ Fin )
7 simp1 
 |-  ( ( Disj_ x e. A x /\ A e. Fin /\ A C_ Fin ) -> Disj_ x e. A x )
8 4 5 6 7 hashunif 
 |-  ( ( Disj_ x e. A x /\ A e. Fin /\ A C_ Fin ) -> ( # ` U. A ) = sum_ x e. A ( # ` x ) )
9 simpl 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> A e. Fin )
10 dfss3 
 |-  ( A C_ Fin <-> A. x e. A x e. Fin )
11 hashcl 
 |-  ( x e. Fin -> ( # ` x ) e. NN0 )
12 nn0re 
 |-  ( ( # ` x ) e. NN0 -> ( # ` x ) e. RR )
13 nn0ge0 
 |-  ( ( # ` x ) e. NN0 -> 0 <_ ( # ` x ) )
14 elrege0 
 |-  ( ( # ` x ) e. ( 0 [,) +oo ) <-> ( ( # ` x ) e. RR /\ 0 <_ ( # ` x ) ) )
15 12 13 14 sylanbrc 
 |-  ( ( # ` x ) e. NN0 -> ( # ` x ) e. ( 0 [,) +oo ) )
16 11 15 syl 
 |-  ( x e. Fin -> ( # ` x ) e. ( 0 [,) +oo ) )
17 16 ralimi 
 |-  ( A. x e. A x e. Fin -> A. x e. A ( # ` x ) e. ( 0 [,) +oo ) )
18 10 17 sylbi 
 |-  ( A C_ Fin -> A. x e. A ( # ` x ) e. ( 0 [,) +oo ) )
19 18 r19.21bi 
 |-  ( ( A C_ Fin /\ x e. A ) -> ( # ` x ) e. ( 0 [,) +oo ) )
20 19 adantll 
 |-  ( ( ( A e. Fin /\ A C_ Fin ) /\ x e. A ) -> ( # ` x ) e. ( 0 [,) +oo ) )
21 9 20 esumpfinval 
 |-  ( ( A e. Fin /\ A C_ Fin ) -> sum* x e. A ( # ` x ) = sum_ x e. A ( # ` x ) )
22 21 3adant1 
 |-  ( ( Disj_ x e. A x /\ A e. Fin /\ A C_ Fin ) -> sum* x e. A ( # ` x ) = sum_ x e. A ( # ` x ) )
23 8 22 eqtr4d 
 |-  ( ( Disj_ x e. A x /\ A e. Fin /\ A C_ Fin ) -> ( # ` U. A ) = sum* x e. A ( # ` x ) )
24 23 3adant1l 
 |-  ( ( ( A e. V /\ Disj_ x e. A x ) /\ A e. Fin /\ A C_ Fin ) -> ( # ` U. A ) = sum* x e. A ( # ` x ) )
25 24 3expa 
 |-  ( ( ( ( A e. V /\ Disj_ x e. A x ) /\ A e. Fin ) /\ A C_ Fin ) -> ( # ` U. A ) = sum* x e. A ( # ` x ) )
26 uniexg 
 |-  ( A e. V -> U. A e. _V )
27 10 notbii 
 |-  ( -. A C_ Fin <-> -. A. x e. A x e. Fin )
28 rexnal 
 |-  ( E. x e. A -. x e. Fin <-> -. A. x e. A x e. Fin )
29 27 28 bitr4i 
 |-  ( -. A C_ Fin <-> E. x e. A -. x e. Fin )
30 elssuni 
 |-  ( x e. A -> x C_ U. A )
31 ssfi 
 |-  ( ( U. A e. Fin /\ x C_ U. A ) -> x e. Fin )
32 31 expcom 
 |-  ( x C_ U. A -> ( U. A e. Fin -> x e. Fin ) )
33 32 con3d 
 |-  ( x C_ U. A -> ( -. x e. Fin -> -. U. A e. Fin ) )
34 30 33 syl 
 |-  ( x e. A -> ( -. x e. Fin -> -. U. A e. Fin ) )
35 34 rexlimiv 
 |-  ( E. x e. A -. x e. Fin -> -. U. A e. Fin )
36 29 35 sylbi 
 |-  ( -. A C_ Fin -> -. U. A e. Fin )
37 hashinf 
 |-  ( ( U. A e. _V /\ -. U. A e. Fin ) -> ( # ` U. A ) = +oo )
38 26 36 37 syl2an 
 |-  ( ( A e. V /\ -. A C_ Fin ) -> ( # ` U. A ) = +oo )
39 vex 
 |-  x e. _V
40 hashinf 
 |-  ( ( x e. _V /\ -. x e. Fin ) -> ( # ` x ) = +oo )
41 39 40 mpan 
 |-  ( -. x e. Fin -> ( # ` x ) = +oo )
42 41 reximi 
 |-  ( E. x e. A -. x e. Fin -> E. x e. A ( # ` x ) = +oo )
43 29 42 sylbi 
 |-  ( -. A C_ Fin -> E. x e. A ( # ` x ) = +oo )
44 nfv 
 |-  F/ x A e. V
45 nfre1 
 |-  F/ x E. x e. A ( # ` x ) = +oo
46 44 45 nfan 
 |-  F/ x ( A e. V /\ E. x e. A ( # ` x ) = +oo )
47 simpl 
 |-  ( ( A e. V /\ E. x e. A ( # ` x ) = +oo ) -> A e. V )
48 hashf2 
 |-  # : _V --> ( 0 [,] +oo )
49 ffvelcdm 
 |-  ( ( # : _V --> ( 0 [,] +oo ) /\ x e. _V ) -> ( # ` x ) e. ( 0 [,] +oo ) )
50 48 39 49 mp2an 
 |-  ( # ` x ) e. ( 0 [,] +oo )
51 50 a1i 
 |-  ( ( ( A e. V /\ E. x e. A ( # ` x ) = +oo ) /\ x e. A ) -> ( # ` x ) e. ( 0 [,] +oo ) )
52 simpr 
 |-  ( ( A e. V /\ E. x e. A ( # ` x ) = +oo ) -> E. x e. A ( # ` x ) = +oo )
53 46 47 51 52 esumpinfval 
 |-  ( ( A e. V /\ E. x e. A ( # ` x ) = +oo ) -> sum* x e. A ( # ` x ) = +oo )
54 43 53 sylan2 
 |-  ( ( A e. V /\ -. A C_ Fin ) -> sum* x e. A ( # ` x ) = +oo )
55 38 54 eqtr4d 
 |-  ( ( A e. V /\ -. A C_ Fin ) -> ( # ` U. A ) = sum* x e. A ( # ` x ) )
56 55 3adant2 
 |-  ( ( A e. V /\ A e. Fin /\ -. A C_ Fin ) -> ( # ` U. A ) = sum* x e. A ( # ` x ) )
57 56 3adant1r 
 |-  ( ( ( A e. V /\ Disj_ x e. A x ) /\ A e. Fin /\ -. A C_ Fin ) -> ( # ` U. A ) = sum* x e. A ( # ` x ) )
58 57 3expa 
 |-  ( ( ( ( A e. V /\ Disj_ x e. A x ) /\ A e. Fin ) /\ -. A C_ Fin ) -> ( # ` U. A ) = sum* x e. A ( # ` x ) )
59 25 58 pm2.61dan 
 |-  ( ( ( A e. V /\ Disj_ x e. A x ) /\ A e. Fin ) -> ( # ` U. A ) = sum* x e. A ( # ` x ) )
60 pwfi 
 |-  ( U. A e. Fin <-> ~P U. A e. Fin )
61 pwuni 
 |-  A C_ ~P U. A
62 ssfi 
 |-  ( ( ~P U. A e. Fin /\ A C_ ~P U. A ) -> A e. Fin )
63 61 62 mpan2 
 |-  ( ~P U. A e. Fin -> A e. Fin )
64 60 63 sylbi 
 |-  ( U. A e. Fin -> A e. Fin )
65 64 con3i 
 |-  ( -. A e. Fin -> -. U. A e. Fin )
66 26 65 37 syl2an 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( # ` U. A ) = +oo )
67 nftru 
 |-  F/ x T.
68 unrab 
 |-  ( { x e. A | ( # ` x ) = 0 } u. { x e. A | -. ( # ` x ) = 0 } ) = { x e. A | ( ( # ` x ) = 0 \/ -. ( # ` x ) = 0 ) }
69 exmid 
 |-  ( ( # ` x ) = 0 \/ -. ( # ` x ) = 0 )
70 69 rgenw 
 |-  A. x e. A ( ( # ` x ) = 0 \/ -. ( # ` x ) = 0 )
71 rabid2 
 |-  ( A = { x e. A | ( ( # ` x ) = 0 \/ -. ( # ` x ) = 0 ) } <-> A. x e. A ( ( # ` x ) = 0 \/ -. ( # ` x ) = 0 ) )
72 70 71 mpbir 
 |-  A = { x e. A | ( ( # ` x ) = 0 \/ -. ( # ` x ) = 0 ) }
73 68 72 eqtr4i 
 |-  ( { x e. A | ( # ` x ) = 0 } u. { x e. A | -. ( # ` x ) = 0 } ) = A
74 73 a1i 
 |-  ( T. -> ( { x e. A | ( # ` x ) = 0 } u. { x e. A | -. ( # ` x ) = 0 } ) = A )
75 67 74 esumeq1d 
 |-  ( T. -> sum* x e. ( { x e. A | ( # ` x ) = 0 } u. { x e. A | -. ( # ` x ) = 0 } ) ( # ` x ) = sum* x e. A ( # ` x ) )
76 75 mptru 
 |-  sum* x e. ( { x e. A | ( # ` x ) = 0 } u. { x e. A | -. ( # ` x ) = 0 } ) ( # ` x ) = sum* x e. A ( # ` x )
77 nfrab1 
 |-  F/_ x { x e. A | ( # ` x ) = 0 }
78 nfrab1 
 |-  F/_ x { x e. A | -. ( # ` x ) = 0 }
79 rabexg 
 |-  ( A e. V -> { x e. A | ( # ` x ) = 0 } e. _V )
80 rabexg 
 |-  ( A e. V -> { x e. A | -. ( # ` x ) = 0 } e. _V )
81 rabnc 
 |-  ( { x e. A | ( # ` x ) = 0 } i^i { x e. A | -. ( # ` x ) = 0 } ) = (/)
82 81 a1i 
 |-  ( A e. V -> ( { x e. A | ( # ` x ) = 0 } i^i { x e. A | -. ( # ` x ) = 0 } ) = (/) )
83 50 a1i 
 |-  ( ( A e. V /\ x e. { x e. A | ( # ` x ) = 0 } ) -> ( # ` x ) e. ( 0 [,] +oo ) )
84 50 a1i 
 |-  ( ( A e. V /\ x e. { x e. A | -. ( # ` x ) = 0 } ) -> ( # ` x ) e. ( 0 [,] +oo ) )
85 44 77 78 79 80 82 83 84 esumsplit 
 |-  ( A e. V -> sum* x e. ( { x e. A | ( # ` x ) = 0 } u. { x e. A | -. ( # ` x ) = 0 } ) ( # ` x ) = ( sum* x e. { x e. A | ( # ` x ) = 0 } ( # ` x ) +e sum* x e. { x e. A | -. ( # ` x ) = 0 } ( # ` x ) ) )
86 76 85 eqtr3id 
 |-  ( A e. V -> sum* x e. A ( # ` x ) = ( sum* x e. { x e. A | ( # ` x ) = 0 } ( # ` x ) +e sum* x e. { x e. A | -. ( # ` x ) = 0 } ( # ` x ) ) )
87 86 adantr 
 |-  ( ( A e. V /\ -. A e. Fin ) -> sum* x e. A ( # ` x ) = ( sum* x e. { x e. A | ( # ` x ) = 0 } ( # ` x ) +e sum* x e. { x e. A | -. ( # ` x ) = 0 } ( # ` x ) ) )
88 nfv 
 |-  F/ x ( A e. V /\ -. A e. Fin )
89 80 adantr 
 |-  ( ( A e. V /\ -. A e. Fin ) -> { x e. A | -. ( # ` x ) = 0 } e. _V )
90 simpr 
 |-  ( ( A e. V /\ -. A e. Fin ) -> -. A e. Fin )
91 dfrab3 
 |-  { x e. A | ( # ` x ) = 0 } = ( A i^i { x | ( # ` x ) = 0 } )
92 hasheq0 
 |-  ( x e. _V -> ( ( # ` x ) = 0 <-> x = (/) ) )
93 39 92 ax-mp 
 |-  ( ( # ` x ) = 0 <-> x = (/) )
94 93 abbii 
 |-  { x | ( # ` x ) = 0 } = { x | x = (/) }
95 df-sn 
 |-  { (/) } = { x | x = (/) }
96 94 95 eqtr4i 
 |-  { x | ( # ` x ) = 0 } = { (/) }
97 96 ineq2i 
 |-  ( A i^i { x | ( # ` x ) = 0 } ) = ( A i^i { (/) } )
98 91 97 eqtri 
 |-  { x e. A | ( # ` x ) = 0 } = ( A i^i { (/) } )
99 snfi 
 |-  { (/) } e. Fin
100 inss2 
 |-  ( A i^i { (/) } ) C_ { (/) }
101 ssfi 
 |-  ( ( { (/) } e. Fin /\ ( A i^i { (/) } ) C_ { (/) } ) -> ( A i^i { (/) } ) e. Fin )
102 99 100 101 mp2an 
 |-  ( A i^i { (/) } ) e. Fin
103 98 102 eqeltri 
 |-  { x e. A | ( # ` x ) = 0 } e. Fin
104 103 a1i 
 |-  ( ( A e. V /\ -. A e. Fin ) -> { x e. A | ( # ` x ) = 0 } e. Fin )
105 difinf 
 |-  ( ( -. A e. Fin /\ { x e. A | ( # ` x ) = 0 } e. Fin ) -> -. ( A \ { x e. A | ( # ` x ) = 0 } ) e. Fin )
106 90 104 105 syl2anc 
 |-  ( ( A e. V /\ -. A e. Fin ) -> -. ( A \ { x e. A | ( # ` x ) = 0 } ) e. Fin )
107 notrab 
 |-  ( A \ { x e. A | ( # ` x ) = 0 } ) = { x e. A | -. ( # ` x ) = 0 }
108 107 eleq1i 
 |-  ( ( A \ { x e. A | ( # ` x ) = 0 } ) e. Fin <-> { x e. A | -. ( # ` x ) = 0 } e. Fin )
109 106 108 sylnib 
 |-  ( ( A e. V /\ -. A e. Fin ) -> -. { x e. A | -. ( # ` x ) = 0 } e. Fin )
110 50 a1i 
 |-  ( ( ( A e. V /\ -. A e. Fin ) /\ x e. { x e. A | -. ( # ` x ) = 0 } ) -> ( # ` x ) e. ( 0 [,] +oo ) )
111 39 a1i 
 |-  ( ( ( A e. V /\ -. A e. Fin ) /\ x e. { x e. A | -. ( # ` x ) = 0 } ) -> x e. _V )
112 simpr 
 |-  ( ( ( A e. V /\ -. A e. Fin ) /\ x e. { x e. A | -. ( # ` x ) = 0 } ) -> x e. { x e. A | -. ( # ` x ) = 0 } )
113 rabid 
 |-  ( x e. { x e. A | -. ( # ` x ) = 0 } <-> ( x e. A /\ -. ( # ` x ) = 0 ) )
114 112 113 sylib 
 |-  ( ( ( A e. V /\ -. A e. Fin ) /\ x e. { x e. A | -. ( # ` x ) = 0 } ) -> ( x e. A /\ -. ( # ` x ) = 0 ) )
115 114 simprd 
 |-  ( ( ( A e. V /\ -. A e. Fin ) /\ x e. { x e. A | -. ( # ` x ) = 0 } ) -> -. ( # ` x ) = 0 )
116 93 biimpri 
 |-  ( x = (/) -> ( # ` x ) = 0 )
117 116 necon3bi 
 |-  ( -. ( # ` x ) = 0 -> x =/= (/) )
118 115 117 syl 
 |-  ( ( ( A e. V /\ -. A e. Fin ) /\ x e. { x e. A | -. ( # ` x ) = 0 } ) -> x =/= (/) )
119 hashge1 
 |-  ( ( x e. _V /\ x =/= (/) ) -> 1 <_ ( # ` x ) )
120 111 118 119 syl2anc 
 |-  ( ( ( A e. V /\ -. A e. Fin ) /\ x e. { x e. A | -. ( # ` x ) = 0 } ) -> 1 <_ ( # ` x ) )
121 1xr 
 |-  1 e. RR*
122 121 a1i 
 |-  ( ( A e. V /\ -. A e. Fin ) -> 1 e. RR* )
123 0lt1 
 |-  0 < 1
124 123 a1i 
 |-  ( ( A e. V /\ -. A e. Fin ) -> 0 < 1 )
125 88 78 89 109 110 120 122 124 esumpinfsum 
 |-  ( ( A e. V /\ -. A e. Fin ) -> sum* x e. { x e. A | -. ( # ` x ) = 0 } ( # ` x ) = +oo )
126 125 oveq2d 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( sum* x e. { x e. A | ( # ` x ) = 0 } ( # ` x ) +e sum* x e. { x e. A | -. ( # ` x ) = 0 } ( # ` x ) ) = ( sum* x e. { x e. A | ( # ` x ) = 0 } ( # ` x ) +e +oo ) )
127 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
128 79 adantr 
 |-  ( ( A e. V /\ -. A e. Fin ) -> { x e. A | ( # ` x ) = 0 } e. _V )
129 50 a1i 
 |-  ( ( ( A e. V /\ -. A e. Fin ) /\ x e. { x e. A | ( # ` x ) = 0 } ) -> ( # ` x ) e. ( 0 [,] +oo ) )
130 129 ralrimiva 
 |-  ( ( A e. V /\ -. A e. Fin ) -> A. x e. { x e. A | ( # ` x ) = 0 } ( # ` x ) e. ( 0 [,] +oo ) )
131 77 esumcl 
 |-  ( ( { x e. A | ( # ` x ) = 0 } e. _V /\ A. x e. { x e. A | ( # ` x ) = 0 } ( # ` x ) e. ( 0 [,] +oo ) ) -> sum* x e. { x e. A | ( # ` x ) = 0 } ( # ` x ) e. ( 0 [,] +oo ) )
132 128 130 131 syl2anc 
 |-  ( ( A e. V /\ -. A e. Fin ) -> sum* x e. { x e. A | ( # ` x ) = 0 } ( # ` x ) e. ( 0 [,] +oo ) )
133 127 132 sselid 
 |-  ( ( A e. V /\ -. A e. Fin ) -> sum* x e. { x e. A | ( # ` x ) = 0 } ( # ` x ) e. RR* )
134 xrge0neqmnf 
 |-  ( sum* x e. { x e. A | ( # ` x ) = 0 } ( # ` x ) e. ( 0 [,] +oo ) -> sum* x e. { x e. A | ( # ` x ) = 0 } ( # ` x ) =/= -oo )
135 132 134 syl 
 |-  ( ( A e. V /\ -. A e. Fin ) -> sum* x e. { x e. A | ( # ` x ) = 0 } ( # ` x ) =/= -oo )
136 xaddpnf1 
 |-  ( ( sum* x e. { x e. A | ( # ` x ) = 0 } ( # ` x ) e. RR* /\ sum* x e. { x e. A | ( # ` x ) = 0 } ( # ` x ) =/= -oo ) -> ( sum* x e. { x e. A | ( # ` x ) = 0 } ( # ` x ) +e +oo ) = +oo )
137 133 135 136 syl2anc 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( sum* x e. { x e. A | ( # ` x ) = 0 } ( # ` x ) +e +oo ) = +oo )
138 87 126 137 3eqtrd 
 |-  ( ( A e. V /\ -. A e. Fin ) -> sum* x e. A ( # ` x ) = +oo )
139 66 138 eqtr4d 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( # ` U. A ) = sum* x e. A ( # ` x ) )
140 139 adantlr 
 |-  ( ( ( A e. V /\ Disj_ x e. A x ) /\ -. A e. Fin ) -> ( # ` U. A ) = sum* x e. A ( # ` x ) )
141 59 140 pm2.61dan 
 |-  ( ( A e. V /\ Disj_ x e. A x ) -> ( # ` U. A ) = sum* x e. A ( # ` x ) )