Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Quantifier-free definitions
dfon4
Next ⟩
brtxpsd
Metamath Proof Explorer
Ascii
Unicode
Theorem
dfon4
Description:
Another quantifier-free definition of
On
.
(Contributed by
Scott Fenton
, 4-May-2014)
Ref
Expression
Assertion
dfon4
⊢
On
=
V
∖
𝖲𝖲𝖾𝗍
∖
I
∪
E
𝖳𝗋𝖺𝗇𝗌
Proof
Step
Hyp
Ref
Expression
1
dfon3
⊢
On
=
V
∖
ran
⁡
𝖲𝖲𝖾𝗍
∩
𝖳𝗋𝖺𝗇𝗌
×
V
∖
I
∪
E
2
df-ima
⊢
𝖲𝖲𝖾𝗍
∖
I
∪
E
𝖳𝗋𝖺𝗇𝗌
=
ran
⁡
𝖲𝖲𝖾𝗍
∖
I
∪
E
↾
𝖳𝗋𝖺𝗇𝗌
3
df-res
⊢
𝖲𝖲𝖾𝗍
∖
I
∪
E
↾
𝖳𝗋𝖺𝗇𝗌
=
𝖲𝖲𝖾𝗍
∖
I
∪
E
∩
𝖳𝗋𝖺𝗇𝗌
×
V
4
indif1
⊢
𝖲𝖲𝖾𝗍
∖
I
∪
E
∩
𝖳𝗋𝖺𝗇𝗌
×
V
=
𝖲𝖲𝖾𝗍
∩
𝖳𝗋𝖺𝗇𝗌
×
V
∖
I
∪
E
5
3
4
eqtri
⊢
𝖲𝖲𝖾𝗍
∖
I
∪
E
↾
𝖳𝗋𝖺𝗇𝗌
=
𝖲𝖲𝖾𝗍
∩
𝖳𝗋𝖺𝗇𝗌
×
V
∖
I
∪
E
6
5
rneqi
⊢
ran
⁡
𝖲𝖲𝖾𝗍
∖
I
∪
E
↾
𝖳𝗋𝖺𝗇𝗌
=
ran
⁡
𝖲𝖲𝖾𝗍
∩
𝖳𝗋𝖺𝗇𝗌
×
V
∖
I
∪
E
7
2
6
eqtri
⊢
𝖲𝖲𝖾𝗍
∖
I
∪
E
𝖳𝗋𝖺𝗇𝗌
=
ran
⁡
𝖲𝖲𝖾𝗍
∩
𝖳𝗋𝖺𝗇𝗌
×
V
∖
I
∪
E
8
7
difeq2i
⊢
V
∖
𝖲𝖲𝖾𝗍
∖
I
∪
E
𝖳𝗋𝖺𝗇𝗌
=
V
∖
ran
⁡
𝖲𝖲𝖾𝗍
∩
𝖳𝗋𝖺𝗇𝗌
×
V
∖
I
∪
E
9
1
8
eqtr4i
⊢
On
=
V
∖
𝖲𝖲𝖾𝗍
∖
I
∪
E
𝖳𝗋𝖺𝗇𝗌