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.defslts	⊢ < = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 𝑅 𝑦 ) }
Assertion	nla0001	⊢ ( 𝜑 → ∅ < ∅ )

Proof

Step	Hyp	Ref	Expression
1		nla0001.defslts	⊢ < = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 𝑅 𝑦 ) }
2		0ex	⊢ ∅ ∈ V
3	2	a1i	⊢ ( 𝜑 → ∅ ∈ V )
4		0ss	⊢ ∅ ⊆ 𝑆
5	4	a1i	⊢ ( 𝜑 → ∅ ⊆ 𝑆 )
6	1 3 5	nla0002	⊢ ( 𝜑 → ∅ < ∅ )