Database
BASIC LINEAR ALGEBRA
Abstract multivariate polynomials
Definition and basic properties
psrbag
Next ⟩
psrbagf
Metamath Proof Explorer
Ascii
Unicode
Theorem
psrbag
Description:
Elementhood in the set of finite bags.
(Contributed by
Mario Carneiro
, 29-Dec-2014)
Ref
Expression
Hypothesis
psrbag.d
⊢
D
=
f
∈
ℕ
0
I
|
f
-1
ℕ
∈
Fin
Assertion
psrbag
⊢
I
∈
V
→
F
∈
D
↔
F
:
I
⟶
ℕ
0
∧
F
-1
ℕ
∈
Fin
Proof
Step
Hyp
Ref
Expression
1
psrbag.d
⊢
D
=
f
∈
ℕ
0
I
|
f
-1
ℕ
∈
Fin
2
cnveq
⊢
f
=
F
→
f
-1
=
F
-1
3
2
imaeq1d
⊢
f
=
F
→
f
-1
ℕ
=
F
-1
ℕ
4
3
eleq1d
⊢
f
=
F
→
f
-1
ℕ
∈
Fin
↔
F
-1
ℕ
∈
Fin
5
4
1
elrab2
⊢
F
∈
D
↔
F
∈
ℕ
0
I
∧
F
-1
ℕ
∈
Fin
6
nn0ex
⊢
ℕ
0
∈
V
7
elmapg
⊢
ℕ
0
∈
V
∧
I
∈
V
→
F
∈
ℕ
0
I
↔
F
:
I
⟶
ℕ
0
8
6
7
mpan
⊢
I
∈
V
→
F
∈
ℕ
0
I
↔
F
:
I
⟶
ℕ
0
9
8
anbi1d
⊢
I
∈
V
→
F
∈
ℕ
0
I
∧
F
-1
ℕ
∈
Fin
↔
F
:
I
⟶
ℕ
0
∧
F
-1
ℕ
∈
Fin
10
5
9
syl5bb
⊢
I
∈
V
→
F
∈
D
↔
F
:
I
⟶
ℕ
0
∧
F
-1
ℕ
∈
Fin