Theorem sltval

Description: The value of the surreal less than relationship. (Contributed by Scott Fenton, 14-Jun-2011)

	Ref	Expression
Assertion	sltval	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑓 = 𝐴 → ( 𝑓 ∈ No ↔ 𝐴 ∈ No ) )
2	1	anbi1d	⊢ ( 𝑓 = 𝐴 → ( ( 𝑓 ∈ No ∧ 𝑔 ∈ No ) ↔ ( 𝐴 ∈ No ∧ 𝑔 ∈ No ) ) )
3		fveq1	⊢ ( 𝑓 = 𝐴 → ( 𝑓 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) )
4	3	eqeq1d	⊢ ( 𝑓 = 𝐴 → ( ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ↔ ( 𝐴 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ) )
5	4	ralbidv	⊢ ( 𝑓 = 𝐴 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ) )
6		fveq1	⊢ ( 𝑓 = 𝐴 → ( 𝑓 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
7	6	breq1d	⊢ ( 𝑓 = 𝐴 → ( ( 𝑓 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) ↔ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) ) )
8	5 7	anbi12d	⊢ ( 𝑓 = 𝐴 → ( ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) ) ) )
9	8	rexbidv	⊢ ( 𝑓 = 𝐴 → ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) ) ) )
10	2 9	anbi12d	⊢ ( 𝑓 = 𝐴 → ( ( ( 𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) ) ) ↔ ( ( 𝐴 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) ) ) ) )
11		eleq1	⊢ ( 𝑔 = 𝐵 → ( 𝑔 ∈ No ↔ 𝐵 ∈ No ) )
12	11	anbi2d	⊢ ( 𝑔 = 𝐵 → ( ( 𝐴 ∈ No ∧ 𝑔 ∈ No ) ↔ ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ) )
13		fveq1	⊢ ( 𝑔 = 𝐵 → ( 𝑔 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) )
14	13	eqeq2d	⊢ ( 𝑔 = 𝐵 → ( ( 𝐴 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ↔ ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) )
15	14	ralbidv	⊢ ( 𝑔 = 𝐵 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) )
16		fveq1	⊢ ( 𝑔 = 𝐵 → ( 𝑔 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
17	16	breq2d	⊢ ( 𝑔 = 𝐵 → ( ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) ↔ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
18	15 17	anbi12d	⊢ ( 𝑔 = 𝐵 → ( ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ) )
19	18	rexbidv	⊢ ( 𝑔 = 𝐵 → ( ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ) )
20	12 19	anbi12d	⊢ ( 𝑔 = 𝐵 → ( ( ( 𝐴 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) ) ) ↔ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ) ) )
21		df-slt	⊢ <s = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) ) ) }
22	10 20 21	brabg	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 ↔ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ) ) )
23	22	bianabs	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ) )