Theorem lrrecval

Description: The next step in the development of the surreals is to establish induction and recursion across left and right sets. To that end, we are going to develop a relationship R that is founded, partial, and set-like across the surreals. This first theorem just establishes the value of R . (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Hypothesis	lrrec.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) }
Assertion	lrrecval	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 𝑅 𝐵 ↔ 𝐴 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lrrec.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) }
2		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ↔ 𝐴 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) )
3		fveq2	⊢ ( 𝑦 = 𝐵 → ( L ‘ 𝑦 ) = ( L ‘ 𝐵 ) )
4		fveq2	⊢ ( 𝑦 = 𝐵 → ( R ‘ 𝑦 ) = ( R ‘ 𝐵 ) )
5	3 4	uneq12d	⊢ ( 𝑦 = 𝐵 → ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) = ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) )
6	5	eleq2d	⊢ ( 𝑦 = 𝐵 → ( 𝐴 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ↔ 𝐴 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ) )
7	2 6 1	brabg	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 𝑅 𝐵 ↔ 𝐴 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ) )