Theorem brsslt

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

	Ref	Expression
Assertion	brsslt	⊢ ( 𝐴 <<s 𝐵 ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ ( 𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-sslt	⊢ <<s = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦 ) }
2	1	bropaex12	⊢ ( 𝐴 <<s 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
3		sseq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 ⊆ No ↔ 𝐴 ⊆ No ) )
4		raleq	⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦 ) )
5	3 4	3anbi13d	⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦 ) ↔ ( 𝐴 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦 ) ) )
6		sseq1	⊢ ( 𝑏 = 𝐵 → ( 𝑏 ⊆ No ↔ 𝐵 ⊆ No ) )
7		raleq	⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) )
8	7	ralbidv	⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) )
9	6 8	3anbi23d	⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦 ) ↔ ( 𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) ) )
10	5 9 1	brabg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 <<s 𝐵 ↔ ( 𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) ) )
11	2 10	biadanii	⊢ ( 𝐴 <<s 𝐵 ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ ( 𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) ) )