Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Surreal Numbers
elno3
Next ⟩
sltval2
Metamath Proof Explorer
Ascii
Unicode
Theorem
elno3
Description:
Another condition for membership in
No
.
(Contributed by
Scott Fenton
, 14-Apr-2012)
Ref
Expression
Assertion
elno3
⊢
A
∈
No
↔
A
:
dom
⁡
A
⟶
1
𝑜
2
𝑜
∧
dom
⁡
A
∈
On
Proof
Step
Hyp
Ref
Expression
1
3anan32
⊢
Fun
⁡
A
∧
dom
⁡
A
∈
On
∧
ran
⁡
A
⊆
1
𝑜
2
𝑜
↔
Fun
⁡
A
∧
ran
⁡
A
⊆
1
𝑜
2
𝑜
∧
dom
⁡
A
∈
On
2
elno2
⊢
A
∈
No
↔
Fun
⁡
A
∧
dom
⁡
A
∈
On
∧
ran
⁡
A
⊆
1
𝑜
2
𝑜
3
df-f
⊢
A
:
dom
⁡
A
⟶
1
𝑜
2
𝑜
↔
A
Fn
dom
⁡
A
∧
ran
⁡
A
⊆
1
𝑜
2
𝑜
4
funfn
⊢
Fun
⁡
A
↔
A
Fn
dom
⁡
A
5
4
anbi1i
⊢
Fun
⁡
A
∧
ran
⁡
A
⊆
1
𝑜
2
𝑜
↔
A
Fn
dom
⁡
A
∧
ran
⁡
A
⊆
1
𝑜
2
𝑜
6
3
5
bitr4i
⊢
A
:
dom
⁡
A
⟶
1
𝑜
2
𝑜
↔
Fun
⁡
A
∧
ran
⁡
A
⊆
1
𝑜
2
𝑜
7
6
anbi1i
⊢
A
:
dom
⁡
A
⟶
1
𝑜
2
𝑜
∧
dom
⁡
A
∈
On
↔
Fun
⁡
A
∧
ran
⁡
A
⊆
1
𝑜
2
𝑜
∧
dom
⁡
A
∈
On
8
1
2
7
3bitr4i
⊢
A
∈
No
↔
A
:
dom
⁡
A
⟶
1
𝑜
2
𝑜
∧
dom
⁡
A
∈
On