Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Relations and Functions
Functions - misc additions
f1mptrn
Next ⟩
dfimafnf
Metamath Proof Explorer
Ascii
Unicode
Theorem
f1mptrn
Description:
Express injection for a mapping operation.
(Contributed by
Thierry Arnoux
, 3-May-2020)
Ref
Expression
Hypotheses
f1mptrn.1
⊢
φ
∧
x
∈
A
→
B
∈
C
f1mptrn.2
⊢
φ
∧
y
∈
C
→
∃!
x
∈
A
y
=
B
Assertion
f1mptrn
⊢
φ
→
Fun
⁡
x
∈
A
⟼
B
-1
Proof
Step
Hyp
Ref
Expression
1
f1mptrn.1
⊢
φ
∧
x
∈
A
→
B
∈
C
2
f1mptrn.2
⊢
φ
∧
y
∈
C
→
∃!
x
∈
A
y
=
B
3
1
ralrimiva
⊢
φ
→
∀
x
∈
A
B
∈
C
4
2
ralrimiva
⊢
φ
→
∀
y
∈
C
∃!
x
∈
A
y
=
B
5
eqid
⊢
x
∈
A
⟼
B
=
x
∈
A
⟼
B
6
5
f1ompt
⊢
x
∈
A
⟼
B
:
A
⟶
1-1 onto
C
↔
∀
x
∈
A
B
∈
C
∧
∀
y
∈
C
∃!
x
∈
A
y
=
B
7
dff1o2
⊢
x
∈
A
⟼
B
:
A
⟶
1-1 onto
C
↔
x
∈
A
⟼
B
Fn
A
∧
Fun
⁡
x
∈
A
⟼
B
-1
∧
ran
⁡
x
∈
A
⟼
B
=
C
8
7
simp2bi
⊢
x
∈
A
⟼
B
:
A
⟶
1-1 onto
C
→
Fun
⁡
x
∈
A
⟼
B
-1
9
6
8
sylbir
⊢
∀
x
∈
A
B
∈
C
∧
∀
y
∈
C
∃!
x
∈
A
y
=
B
→
Fun
⁡
x
∈
A
⟼
B
-1
10
3
4
9
syl2anc
⊢
φ
→
Fun
⁡
x
∈
A
⟼
B
-1