Metamath Proof Explorer

Theorem rp-brsslt

Description: Binary relation form of a relation, .< , which has been extended from relation R to subsets of class S . Usually, we will assume R Or S . Definition in Alling, p. 2. Generalization of brsslt . (Originally by Scott Fenton, 8-Dec-2021.) (Contributed by RP, 28-Nov-2023)

Ref Expression
Hypothesis nla0001.defsslt ⊢ < ˙ = a b | a ⊆ S ∧ b ⊆ S ∧ ∀ x ∈ a ∀ y ∈ b x R y
Assertion rp-brsslt ⊢ A < ˙ B ↔ A ∈ V ∧ B ∈ V ∧ A ⊆ S ∧ B ⊆ S ∧ ∀ x ∈ A ∀ y ∈ B x R y

Proof

Step Hyp Ref Expression
1 nla0001.defsslt ⊢ < ˙ = a b | a ⊆ S ∧ b ⊆ S ∧ ∀ x ∈ a ∀ y ∈ b x R y
2 sseq1 ⊢ a = A → a ⊆ S ↔ A ⊆ S
3 raleq ⊢ a = A → ∀ x ∈ a ∀ y ∈ b x R y ↔ ∀ x ∈ A ∀ y ∈ b x R y
4 2 3 3anbi13d ⊢ a = A → a ⊆ S ∧ b ⊆ S ∧ ∀ x ∈ a ∀ y ∈ b x R y ↔ A ⊆ S ∧ b ⊆ S ∧ ∀ x ∈ A ∀ y ∈ b x R y
5 sseq1 ⊢ b = B → b ⊆ S ↔ B ⊆ S
6 raleq ⊢ b = B → ∀ y ∈ b x R y ↔ ∀ y ∈ B x R y
7 6 ralbidv ⊢ b = B → ∀ x ∈ A ∀ y ∈ b x R y ↔ ∀ x ∈ A ∀ y ∈ B x R y
8 5 7 3anbi23d ⊢ b = B → A ⊆ S ∧ b ⊆ S ∧ ∀ x ∈ A ∀ y ∈ b x R y ↔ A ⊆ S ∧ B ⊆ S ∧ ∀ x ∈ A ∀ y ∈ B x R y
9 4 8 1 bropabg ⊢ A < ˙ B ↔ A ∈ V ∧ B ∈ V ∧ A ⊆ S ∧ B ⊆ S ∧ ∀ x ∈ A ∀ y ∈ B x R y