Theorem nla0003

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

	Ref	Expression
Hypotheses	nla0001.defsslt	⊢ < = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 𝑅 𝑦 ) }
	nla0001.set	⊢ ( 𝜑 → 𝐴 ∈ V )
	nla0002.sset	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
Assertion	nla0003	⊢ ( 𝜑 → 𝐴 < ∅ )

Proof

Step	Hyp	Ref	Expression
1		nla0001.defsslt	⊢ < = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 𝑅 𝑦 ) }
2		nla0001.set	⊢ ( 𝜑 → 𝐴 ∈ V )
3		nla0002.sset	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
4		0ex	⊢ ∅ ∈ V
5	4	a1i	⊢ ( 𝜑 → ∅ ∈ V )
6		0ss	⊢ ∅ ⊆ 𝑆
7	6	a1i	⊢ ( 𝜑 → ∅ ⊆ 𝑆 )
8		ral0	⊢ ∀ 𝑦 ∈ ∅ ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦
9		ralcom	⊢ ( ∀ 𝑦 ∈ ∅ ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ∅ 𝑥 𝑅 𝑦 )
10	8 9	mpbi	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ∅ 𝑥 𝑅 𝑦
11	10	a1i	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ∅ 𝑥 𝑅 𝑦 )
12	3 7 11	3jca	⊢ ( 𝜑 → ( 𝐴 ⊆ 𝑆 ∧ ∅ ⊆ 𝑆 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ∅ 𝑥 𝑅 𝑦 ) )
13	1	rp-brsslt	⊢ ( 𝐴 < ∅ ↔ ( ( 𝐴 ∈ V ∧ ∅ ∈ V ) ∧ ( 𝐴 ⊆ 𝑆 ∧ ∅ ⊆ 𝑆 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ∅ 𝑥 𝑅 𝑦 ) ) )
14	2 5 12 13	syl21anbrc	⊢ ( 𝜑 → 𝐴 < ∅ )