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 brslts . (Originally by Scott Fenton, 8-Dec-2021.) (Contributed by RP, 28-Nov-2023)

	Ref	Expression
Hypothesis	nla0001.defslts	⊢ < = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 𝑅 𝑦 ) }
Assertion	rp-brsslt	⊢ ( 𝐴 < 𝐵 ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 𝑅 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nla0001.defslts	⊢ < = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 𝑅 𝑦 ) }
2		sseq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 ⊆ 𝑆 ↔ 𝐴 ⊆ 𝑆 ) )
3		raleq	⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 𝑅 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑏 𝑥 𝑅 𝑦 ) )
4	2 3	3anbi13d	⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 𝑅 𝑦 ) ↔ ( 𝐴 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑏 𝑥 𝑅 𝑦 ) ) )
5		sseq1	⊢ ( 𝑏 = 𝐵 → ( 𝑏 ⊆ 𝑆 ↔ 𝐵 ⊆ 𝑆 ) )
6		raleq	⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑦 ∈ 𝑏 𝑥 𝑅 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 𝑥 𝑅 𝑦 ) )
7	6	ralbidv	⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑏 𝑥 𝑅 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 𝑅 𝑦 ) )
8	5 7	3anbi23d	⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑏 𝑥 𝑅 𝑦 ) ↔ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 𝑅 𝑦 ) ) )
9	4 8 1	bropabg	⊢ ( 𝐴 < 𝐵 ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ ( 𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 𝑅 𝑦 ) ) )