Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Short Studies
General Observations
sn1dom
Next ⟩
pr2dom
Metamath Proof Explorer
Ascii
Unicode
Theorem
sn1dom
Description:
A singleton is dominated by ordinal one.
(Contributed by
RP
, 29-Oct-2023)
Ref
Expression
Assertion
sn1dom
⊢
A
≼
1
𝑜
Proof
Step
Hyp
Ref
Expression
1
ensn1g
⊢
A
∈
V
→
A
≈
1
𝑜
2
1on
⊢
1
𝑜
∈
On
3
domrefg
⊢
1
𝑜
∈
On
→
1
𝑜
≼
1
𝑜
4
2
3
ax-mp
⊢
1
𝑜
≼
1
𝑜
5
endomtr
⊢
A
≈
1
𝑜
∧
1
𝑜
≼
1
𝑜
→
A
≼
1
𝑜
6
1
4
5
sylancl
⊢
A
∈
V
→
A
≼
1
𝑜
7
snprc
⊢
¬
A
∈
V
↔
A
=
∅
8
snex
⊢
A
∈
V
9
eqeng
⊢
A
∈
V
→
A
=
∅
→
A
≈
∅
10
8
9
ax-mp
⊢
A
=
∅
→
A
≈
∅
11
7
10
sylbi
⊢
¬
A
∈
V
→
A
≈
∅
12
0domg
⊢
1
𝑜
∈
On
→
∅
≼
1
𝑜
13
2
12
ax-mp
⊢
∅
≼
1
𝑜
14
endomtr
⊢
A
≈
∅
∧
∅
≼
1
𝑜
→
A
≼
1
𝑜
15
11
13
14
sylancl
⊢
¬
A
∈
V
→
A
≼
1
𝑜
16
6
15
pm2.61i
⊢
A
≼
1
𝑜