Database
REAL AND COMPLEX NUMBERS
Elementary limits and convergence
Finite and infinite sums
hash2iun
Next ⟩
hash2iun1dif1
Metamath Proof Explorer
Ascii
Unicode
Theorem
hash2iun
Description:
The cardinality of a nested disjoint indexed union.
(Contributed by
AV
, 9-Jan-2022)
Ref
Expression
Hypotheses
hash2iun.a
⊢
φ
→
A
∈
Fin
hash2iun.b
⊢
φ
∧
x
∈
A
→
B
∈
Fin
hash2iun.c
⊢
φ
∧
x
∈
A
∧
y
∈
B
→
C
∈
Fin
hash2iun.da
⊢
φ
→
Disj
x
∈
A
⋃
y
∈
B
C
hash2iun.db
⊢
φ
∧
x
∈
A
→
Disj
y
∈
B
C
Assertion
hash2iun
⊢
φ
→
⋃
x
∈
A
⋃
y
∈
B
C
=
∑
x
∈
A
∑
y
∈
B
C
Proof
Step
Hyp
Ref
Expression
1
hash2iun.a
⊢
φ
→
A
∈
Fin
2
hash2iun.b
⊢
φ
∧
x
∈
A
→
B
∈
Fin
3
hash2iun.c
⊢
φ
∧
x
∈
A
∧
y
∈
B
→
C
∈
Fin
4
hash2iun.da
⊢
φ
→
Disj
x
∈
A
⋃
y
∈
B
C
5
hash2iun.db
⊢
φ
∧
x
∈
A
→
Disj
y
∈
B
C
6
3
3expa
⊢
φ
∧
x
∈
A
∧
y
∈
B
→
C
∈
Fin
7
6
ralrimiva
⊢
φ
∧
x
∈
A
→
∀
y
∈
B
C
∈
Fin
8
iunfi
⊢
B
∈
Fin
∧
∀
y
∈
B
C
∈
Fin
→
⋃
y
∈
B
C
∈
Fin
9
2
7
8
syl2anc
⊢
φ
∧
x
∈
A
→
⋃
y
∈
B
C
∈
Fin
10
1
9
4
hashiun
⊢
φ
→
⋃
x
∈
A
⋃
y
∈
B
C
=
∑
x
∈
A
⋃
y
∈
B
C
11
2
6
5
hashiun
⊢
φ
∧
x
∈
A
→
⋃
y
∈
B
C
=
∑
y
∈
B
C
12
11
sumeq2dv
⊢
φ
→
∑
x
∈
A
⋃
y
∈
B
C
=
∑
x
∈
A
∑
y
∈
B
C
13
10
12
eqtrd
⊢
φ
→
⋃
x
∈
A
⋃
y
∈
B
C
=
∑
x
∈
A
∑
y
∈
B
C