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 ffvelrn
 |-  ( ( # : _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 ) )