Metamath Proof Explorer

Theorem brsslt

Description: Binary relation form of the surreal set less-than relation. (Contributed by Scott Fenton, 8-Dec-2021)

Ref Expression
Assertion brsslt ⊢ A ≪ s B ↔ A ∈ V ∧ B ∈ V ∧ A ⊆ No ∧ B ⊆ No ∧ ∀ x ∈ A ∀ y ∈ B x < s y

Proof

Step Hyp Ref Expression
1 df-sslt ⊢ ≪ s = a b | a ⊆ No ∧ b ⊆ No ∧ ∀ x ∈ a ∀ y ∈ b x < s y
2 1 bropaex12 ⊢ A ≪ s B → A ∈ V ∧ B ∈ V
3 sseq1 ⊢ a = A → a ⊆ No ↔ A ⊆ No
4 raleq ⊢ a = A → ∀ x ∈ a ∀ y ∈ b x < s y ↔ ∀ x ∈ A ∀ y ∈ b x < s y
5 3 4 3anbi13d ⊢ a = A → a ⊆ No ∧ b ⊆ No ∧ ∀ x ∈ a ∀ y ∈ b x < s y ↔ A ⊆ No ∧ b ⊆ No ∧ ∀ x ∈ A ∀ y ∈ b x < s y
6 sseq1 ⊢ b = B → b ⊆ No ↔ B ⊆ No
7 raleq ⊢ b = B → ∀ y ∈ b x < s y ↔ ∀ y ∈ B x < s y
8 7 ralbidv ⊢ b = B → ∀ x ∈ A ∀ y ∈ b x < s y ↔ ∀ x ∈ A ∀ y ∈ B x < s y
9 6 8 3anbi23d ⊢ b = B → A ⊆ No ∧ b ⊆ No ∧ ∀ x ∈ A ∀ y ∈ b x < s y ↔ A ⊆ No ∧ B ⊆ No ∧ ∀ x ∈ A ∀ y ∈ B x < s y
10 5 9 1 brabg ⊢ A ∈ V ∧ B ∈ V → A ≪ s B ↔ A ⊆ No ∧ B ⊆ No ∧ ∀ x ∈ A ∀ y ∈ B x < s y
11 2 10 biadanii ⊢ A ≪ s B ↔ A ∈ V ∧ B ∈ V ∧ A ⊆ No ∧ B ⊆ No ∧ ∀ x ∈ A ∀ y ∈ B x < s y