Metamath Proof Explorer

Theorem nla0001

Description: Extending a linear order to subsets, the empty set is less than itself. Note in Alling, p. 3. (Contributed by RP, 28-Nov-2023)

Ref Expression
Hypothesis nla0001.defsslt 
|- .< = { <. a , b >. | ( a C_ S /\ b C_ S /\ A. x e. a A. y e. b x R y ) }
Assertion nla0001 
|- ( ph -> (/) .< (/) )

Proof

Step Hyp Ref Expression
1 nla0001.defsslt 
 |-  .< = { <. a , b >. | ( a C_ S /\ b C_ S /\ A. x e. a A. y e. b x R y ) }
2 0ex 
 |-  (/) e. _V
3 2 a1i 
 |-  ( ph -> (/) e. _V )
4 0ss 
 |-  (/) C_ S
5 4 a1i 
 |-  ( ph -> (/) C_ S )
6 1 3 5 nla0002 
 |-  ( ph -> (/) .< (/) )