Database
TG (TARSKI-GROTHENDIECK) SET THEORY
Inaccessibles
Tarski classes
tsk1
Next ⟩
tsk2
Metamath Proof Explorer
Ascii
Unicode
Theorem
tsk1
Description:
One is an element of a nonempty Tarski class.
(Contributed by
FL
, 22-Feb-2011)
Ref
Expression
Assertion
tsk1
⊢
T
∈
Tarski
∧
T
≠
∅
→
1
𝑜
∈
T
Proof
Step
Hyp
Ref
Expression
1
df1o2
⊢
1
𝑜
=
∅
2
tsk0
⊢
T
∈
Tarski
∧
T
≠
∅
→
∅
∈
T
3
tsksn
⊢
T
∈
Tarski
∧
∅
∈
T
→
∅
∈
T
4
2
3
syldan
⊢
T
∈
Tarski
∧
T
≠
∅
→
∅
∈
T
5
1
4
eqeltrid
⊢
T
∈
Tarski
∧
T
≠
∅
→
1
𝑜
∈
T