Theorem negsproplem1

Description: Lemma for surreal negation. We prove a pair of properties of surreal negation simultaneously. First, we instantiate some quantifiers. (Contributed by Scott Fenton, 2-Feb-2025)

	Ref	Expression
Hypotheses	negsproplem.1	⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
	negsproplem1.1	⊢ ( 𝜑 → 𝑋 ∈ No )
	negsproplem1.2	⊢ ( 𝜑 → 𝑌 ∈ No )
	negsproplem1.3	⊢ ( 𝜑 → ( ( bday ‘ 𝑋 ) ∪ ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) )
Assertion	negsproplem1	⊢ ( 𝜑 → ( ( -us ‘ 𝑋 ) ∈ No ∧ ( 𝑋 <s 𝑌 → ( -us ‘ 𝑌 ) <s ( -us ‘ 𝑋 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		negsproplem.1	⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
2		negsproplem1.1	⊢ ( 𝜑 → 𝑋 ∈ No )
3		negsproplem1.2	⊢ ( 𝜑 → 𝑌 ∈ No )
4		negsproplem1.3	⊢ ( 𝜑 → ( ( bday ‘ 𝑋 ) ∪ ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) )
5	2 3	jca	⊢ ( 𝜑 → ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) )
6		fveq2	⊢ ( 𝑥 = 𝑋 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝑋 ) )
7	6	uneq1d	⊢ ( 𝑥 = 𝑋 → ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝑋 ) ∪ ( bday ‘ 𝑦 ) ) )
8	7	eleq1d	⊢ ( 𝑥 = 𝑋 → ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) ↔ ( ( bday ‘ 𝑋 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) ) )
9		fveq2	⊢ ( 𝑥 = 𝑋 → ( -us ‘ 𝑥 ) = ( -us ‘ 𝑋 ) )
10	9	eleq1d	⊢ ( 𝑥 = 𝑋 → ( ( -us ‘ 𝑥 ) ∈ No ↔ ( -us ‘ 𝑋 ) ∈ No ) )
11		breq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 <s 𝑦 ↔ 𝑋 <s 𝑦 ) )
12	9	breq2d	⊢ ( 𝑥 = 𝑋 → ( ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ↔ ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑋 ) ) )
13	11 12	imbi12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ↔ ( 𝑋 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑋 ) ) ) )
14	10 13	anbi12d	⊢ ( 𝑥 = 𝑋 → ( ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ↔ ( ( -us ‘ 𝑋 ) ∈ No ∧ ( 𝑋 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑋 ) ) ) ) )
15	8 14	imbi12d	⊢ ( 𝑥 = 𝑋 → ( ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ↔ ( ( ( bday ‘ 𝑋 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑋 ) ∈ No ∧ ( 𝑋 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑋 ) ) ) ) ) )
16		fveq2	⊢ ( 𝑦 = 𝑌 → ( bday ‘ 𝑦 ) = ( bday ‘ 𝑌 ) )
17	16	uneq2d	⊢ ( 𝑦 = 𝑌 → ( ( bday ‘ 𝑋 ) ∪ ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝑋 ) ∪ ( bday ‘ 𝑌 ) ) )
18	17	eleq1d	⊢ ( 𝑦 = 𝑌 → ( ( ( bday ‘ 𝑋 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) ↔ ( ( bday ‘ 𝑋 ) ∪ ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) ) )
19		breq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 <s 𝑦 ↔ 𝑋 <s 𝑌 ) )
20		fveq2	⊢ ( 𝑦 = 𝑌 → ( -us ‘ 𝑦 ) = ( -us ‘ 𝑌 ) )
21	20	breq1d	⊢ ( 𝑦 = 𝑌 → ( ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑋 ) ↔ ( -us ‘ 𝑌 ) <s ( -us ‘ 𝑋 ) ) )
22	19 21	imbi12d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑋 ) ) ↔ ( 𝑋 <s 𝑌 → ( -us ‘ 𝑌 ) <s ( -us ‘ 𝑋 ) ) ) )
23	22	anbi2d	⊢ ( 𝑦 = 𝑌 → ( ( ( -us ‘ 𝑋 ) ∈ No ∧ ( 𝑋 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑋 ) ) ) ↔ ( ( -us ‘ 𝑋 ) ∈ No ∧ ( 𝑋 <s 𝑌 → ( -us ‘ 𝑌 ) <s ( -us ‘ 𝑋 ) ) ) ) )
24	18 23	imbi12d	⊢ ( 𝑦 = 𝑌 → ( ( ( ( bday ‘ 𝑋 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑋 ) ∈ No ∧ ( 𝑋 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑋 ) ) ) ) ↔ ( ( ( bday ‘ 𝑋 ) ∪ ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑋 ) ∈ No ∧ ( 𝑋 <s 𝑌 → ( -us ‘ 𝑌 ) <s ( -us ‘ 𝑋 ) ) ) ) ) )
25	15 24	rspc2v	⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) → ( ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) → ( ( ( bday ‘ 𝑋 ) ∪ ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑋 ) ∈ No ∧ ( 𝑋 <s 𝑌 → ( -us ‘ 𝑌 ) <s ( -us ‘ 𝑋 ) ) ) ) ) )
26	5 1 4 25	syl3c	⊢ ( 𝜑 → ( ( -us ‘ 𝑋 ) ∈ No ∧ ( 𝑋 <s 𝑌 → ( -us ‘ 𝑌 ) <s ( -us ‘ 𝑋 ) ) ) )