Metamath Proof Explorer

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.defslts ⊢ < ˙ = a b | a ⊆ S ∧ b ⊆ S ∧ ∀ x ∈ a ∀ y ∈ b x R y
nla0001.set ⊢ φ → A ∈ V
nla0002.sset ⊢ φ → A ⊆ S
Assertion nla0003 ⊢ φ → A < ˙ ∅

Proof

Step Hyp Ref Expression
1 nla0001.defslts ⊢ < ˙ = a b | a ⊆ S ∧ b ⊆ S ∧ ∀ x ∈ a ∀ y ∈ b x R y
2 nla0001.set ⊢ φ → A ∈ V
3 nla0002.sset ⊢ φ → A ⊆ S
4 0ex ⊢ ∅ ∈ V
5 4 a1i ⊢ φ → ∅ ∈ V
6 0ss ⊢ ∅ ⊆ S
7 6 a1i ⊢ φ → ∅ ⊆ S
8 ral0 ⊢ ∀ y ∈ ∅ ∀ x ∈ A x R y
9 ralcom ⊢ ∀ y ∈ ∅ ∀ x ∈ A x R y ↔ ∀ x ∈ A ∀ y ∈ ∅ x R y
10 8 9 mpbi ⊢ ∀ x ∈ A ∀ y ∈ ∅ x R y
11 10 a1i ⊢ φ → ∀ x ∈ A ∀ y ∈ ∅ x R y
12 3 7 11 3jca ⊢ φ → A ⊆ S ∧ ∅ ⊆ S ∧ ∀ x ∈ A ∀ y ∈ ∅ x R y
13 1 rp-brsslt ⊢ A < ˙ ∅ ↔ A ∈ V ∧ ∅ ∈ V ∧ A ⊆ S ∧ ∅ ⊆ S ∧ ∀ x ∈ A ∀ y ∈ ∅ x R y
14 2 5 12 13 syl21anbrc ⊢ φ → A < ˙ ∅