Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Functions
elfunsALTV5
Next ⟩
elfunsALTVfunALTV
Metamath Proof Explorer
Ascii
Unicode
Theorem
elfunsALTV5
Description:
Elementhood in the class of functions.
(Contributed by
Peter Mazsa
, 5-Sep-2021)
Ref
Expression
Assertion
elfunsALTV5
⊢
F
∈
FunsALTV
↔
∀
x
∈
ran
⁡
F
∀
y
∈
ran
⁡
F
x
=
y
∨
x
F
-1
∩
y
F
-1
=
∅
∧
F
∈
Rels
Proof
Step
Hyp
Ref
Expression
1
elfunsALTV
⊢
F
∈
FunsALTV
↔
≀
F
∈
CnvRefRels
∧
F
∈
Rels
2
cosselcnvrefrels5
⊢
≀
F
∈
CnvRefRels
↔
∀
x
∈
ran
⁡
F
∀
y
∈
ran
⁡
F
x
=
y
∨
x
F
-1
∩
y
F
-1
=
∅
∧
≀
F
∈
Rels
3
cosselrels
⊢
F
∈
Rels
→
≀
F
∈
Rels
4
3
biantrud
⊢
F
∈
Rels
→
∀
x
∈
ran
⁡
F
∀
y
∈
ran
⁡
F
x
=
y
∨
x
F
-1
∩
y
F
-1
=
∅
↔
∀
x
∈
ran
⁡
F
∀
y
∈
ran
⁡
F
x
=
y
∨
x
F
-1
∩
y
F
-1
=
∅
∧
≀
F
∈
Rels
5
2
4
bitr4id
⊢
F
∈
Rels
→
≀
F
∈
CnvRefRels
↔
∀
x
∈
ran
⁡
F
∀
y
∈
ran
⁡
F
x
=
y
∨
x
F
-1
∩
y
F
-1
=
∅
6
5
pm5.32ri
⊢
≀
F
∈
CnvRefRels
∧
F
∈
Rels
↔
∀
x
∈
ran
⁡
F
∀
y
∈
ran
⁡
F
x
=
y
∨
x
F
-1
∩
y
F
-1
=
∅
∧
F
∈
Rels
7
1
6
bitri
⊢
F
∈
FunsALTV
↔
∀
x
∈
ran
⁡
F
∀
y
∈
ran
⁡
F
x
=
y
∨
x
F
-1
∩
y
F
-1
=
∅
∧
F
∈
Rels