Theorem negsprop

Description: Show closure and ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	negsprop	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( -us ‘ 𝐴 ) ∈ No ∧ ( 𝐴 <s 𝐵 → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		bdayon	⊢ ( bday ‘ 𝐴 ) ∈ On
2		bdayon	⊢ ( bday ‘ 𝐵 ) ∈ On
3	1 2	onun2i	⊢ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) ∈ On
4		risset	⊢ ( ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) ∈ On ↔ ∃ 𝑎 ∈ On 𝑎 = ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) )
5	3 4	mpbi	⊢ ∃ 𝑎 ∈ On 𝑎 = ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) )
6		eqeq1	⊢ ( 𝑎 = 𝑏 → ( 𝑎 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) ↔ 𝑏 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) ) )
7	6	imbi1d	⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) ) ↔ ( 𝑏 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) ) ) )
8	7	2ralbidv	⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑝 ∈ No ∀ 𝑞 ∈ No ( 𝑎 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) ) ↔ ∀ 𝑝 ∈ No ∀ 𝑞 ∈ No ( 𝑏 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) ) ) )
9		fveq2	⊢ ( 𝑝 = 𝑥 → ( bday ‘ 𝑝 ) = ( bday ‘ 𝑥 ) )
10	9	uneq1d	⊢ ( 𝑝 = 𝑥 → ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑞 ) ) )
11	10	eqeq2d	⊢ ( 𝑝 = 𝑥 → ( 𝑏 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) ↔ 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑞 ) ) ) )
12		fveq2	⊢ ( 𝑝 = 𝑥 → ( -us ‘ 𝑝 ) = ( -us ‘ 𝑥 ) )
13	12	eleq1d	⊢ ( 𝑝 = 𝑥 → ( ( -us ‘ 𝑝 ) ∈ No ↔ ( -us ‘ 𝑥 ) ∈ No ) )
14		breq1	⊢ ( 𝑝 = 𝑥 → ( 𝑝 <s 𝑞 ↔ 𝑥 <s 𝑞 ) )
15	12	breq2d	⊢ ( 𝑝 = 𝑥 → ( ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ↔ ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑥 ) ) )
16	14 15	imbi12d	⊢ ( 𝑝 = 𝑥 → ( ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ↔ ( 𝑥 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑥 ) ) ) )
17	13 16	anbi12d	⊢ ( 𝑝 = 𝑥 → ( ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) ↔ ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑥 ) ) ) ) )
18	11 17	imbi12d	⊢ ( 𝑝 = 𝑥 → ( ( 𝑏 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) ) ↔ ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑥 ) ) ) ) ) )
19		fveq2	⊢ ( 𝑞 = 𝑦 → ( bday ‘ 𝑞 ) = ( bday ‘ 𝑦 ) )
20	19	uneq2d	⊢ ( 𝑞 = 𝑦 → ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑞 ) ) = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) )
21	20	eqeq2d	⊢ ( 𝑞 = 𝑦 → ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑞 ) ) ↔ 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ) )
22		breq2	⊢ ( 𝑞 = 𝑦 → ( 𝑥 <s 𝑞 ↔ 𝑥 <s 𝑦 ) )
23		fveq2	⊢ ( 𝑞 = 𝑦 → ( -us ‘ 𝑞 ) = ( -us ‘ 𝑦 ) )
24	23	breq1d	⊢ ( 𝑞 = 𝑦 → ( ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑥 ) ↔ ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) )
25	22 24	imbi12d	⊢ ( 𝑞 = 𝑦 → ( ( 𝑥 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑥 ) ) ↔ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) )
26	25	anbi2d	⊢ ( 𝑞 = 𝑦 → ( ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑥 ) ) ) ↔ ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
27	21 26	imbi12d	⊢ ( 𝑞 = 𝑦 → ( ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑥 ) ) ) ) ↔ ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ) )
28	18 27	cbvral2vw	⊢ ( ∀ 𝑝 ∈ No ∀ 𝑞 ∈ No ( 𝑏 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) ) ↔ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
29	8 28	bitrdi	⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑝 ∈ No ∀ 𝑞 ∈ No ( 𝑎 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) ) ↔ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ) )
30		raleq	⊢ ( 𝑎 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ↔ ∀ 𝑏 ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ) )
31		ralrot3	⊢ ( ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑏 ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ↔ ∀ 𝑏 ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
32		r19.23v	⊢ ( ∀ 𝑏 ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ↔ ( ∃ 𝑏 ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
33		risset	⊢ ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) ↔ ∃ 𝑏 ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) )
34	33	imbi1i	⊢ ( ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ↔ ( ∃ 𝑏 ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
35	32 34	bitr4i	⊢ ( ∀ 𝑏 ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ↔ ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
36	35	2ralbii	⊢ ( ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑏 ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ↔ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
37	31 36	bitr3i	⊢ ( ∀ 𝑏 ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ↔ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
38	30 37	bitrdi	⊢ ( 𝑎 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ↔ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ) )
39		simpr	⊢ ( ( ( 𝑝 ∈ No ∧ 𝑞 ∈ No ) ∧ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
40		simpll	⊢ ( ( ( 𝑝 ∈ No ∧ 𝑞 ∈ No ) ∧ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ) → 𝑝 ∈ No )
41	39 40	negsproplem3	⊢ ( ( ( 𝑝 ∈ No ∧ 𝑞 ∈ No ) ∧ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ) → ( ( -us ‘ 𝑝 ) ∈ No ∧ ( -us “ ( R ‘ 𝑝 ) ) <<s { ( -us ‘ 𝑝 ) } ∧ { ( -us ‘ 𝑝 ) } <<s ( -us “ ( L ‘ 𝑝 ) ) ) )
42	41	simp1d	⊢ ( ( ( 𝑝 ∈ No ∧ 𝑞 ∈ No ) ∧ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ) → ( -us ‘ 𝑝 ) ∈ No )
43		simplr	⊢ ( ( ( ( 𝑝 ∈ No ∧ 𝑞 ∈ No ) ∧ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ) ∧ 𝑝 <s 𝑞 ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
44		simplll	⊢ ( ( ( ( 𝑝 ∈ No ∧ 𝑞 ∈ No ) ∧ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ) ∧ 𝑝 <s 𝑞 ) → 𝑝 ∈ No )
45		simpllr	⊢ ( ( ( ( 𝑝 ∈ No ∧ 𝑞 ∈ No ) ∧ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ) ∧ 𝑝 <s 𝑞 ) → 𝑞 ∈ No )
46		simpr	⊢ ( ( ( ( 𝑝 ∈ No ∧ 𝑞 ∈ No ) ∧ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ) ∧ 𝑝 <s 𝑞 ) → 𝑝 <s 𝑞 )
47	43 44 45 46	negsproplem7	⊢ ( ( ( ( 𝑝 ∈ No ∧ 𝑞 ∈ No ) ∧ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ) ∧ 𝑝 <s 𝑞 ) → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) )
48	47	ex	⊢ ( ( ( 𝑝 ∈ No ∧ 𝑞 ∈ No ) ∧ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ) → ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) )
49	42 48	jca	⊢ ( ( ( 𝑝 ∈ No ∧ 𝑞 ∈ No ) ∧ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ) → ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) )
50	49	expcom	⊢ ( ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) → ( ( 𝑝 ∈ No ∧ 𝑞 ∈ No ) → ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) ) )
51	38 50	biimtrdi	⊢ ( 𝑎 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) → ( ( 𝑝 ∈ No ∧ 𝑞 ∈ No ) → ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) ) ) )
52	51	com3l	⊢ ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) → ( ( 𝑝 ∈ No ∧ 𝑞 ∈ No ) → ( 𝑎 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) ) ) )
53	52	ralrimivv	⊢ ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) → ∀ 𝑝 ∈ No ∀ 𝑞 ∈ No ( 𝑎 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) ) )
54	53	a1i	⊢ ( 𝑎 ∈ On → ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( 𝑏 = ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) → ∀ 𝑝 ∈ No ∀ 𝑞 ∈ No ( 𝑎 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) ) ) )
55	29 54	tfis2	⊢ ( 𝑎 ∈ On → ∀ 𝑝 ∈ No ∀ 𝑞 ∈ No ( 𝑎 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) ) )
56		fveq2	⊢ ( 𝑝 = 𝐴 → ( bday ‘ 𝑝 ) = ( bday ‘ 𝐴 ) )
57	56	uneq1d	⊢ ( 𝑝 = 𝐴 → ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) = ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝑞 ) ) )
58	57	eqeq2d	⊢ ( 𝑝 = 𝐴 → ( 𝑎 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) ↔ 𝑎 = ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝑞 ) ) ) )
59		fveq2	⊢ ( 𝑝 = 𝐴 → ( -us ‘ 𝑝 ) = ( -us ‘ 𝐴 ) )
60	59	eleq1d	⊢ ( 𝑝 = 𝐴 → ( ( -us ‘ 𝑝 ) ∈ No ↔ ( -us ‘ 𝐴 ) ∈ No ) )
61		breq1	⊢ ( 𝑝 = 𝐴 → ( 𝑝 <s 𝑞 ↔ 𝐴 <s 𝑞 ) )
62	59	breq2d	⊢ ( 𝑝 = 𝐴 → ( ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ↔ ( -us ‘ 𝑞 ) <s ( -us ‘ 𝐴 ) ) )
63	61 62	imbi12d	⊢ ( 𝑝 = 𝐴 → ( ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ↔ ( 𝐴 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝐴 ) ) ) )
64	60 63	anbi12d	⊢ ( 𝑝 = 𝐴 → ( ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) ↔ ( ( -us ‘ 𝐴 ) ∈ No ∧ ( 𝐴 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝐴 ) ) ) ) )
65	58 64	imbi12d	⊢ ( 𝑝 = 𝐴 → ( ( 𝑎 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) ) ↔ ( 𝑎 = ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝐴 ) ∈ No ∧ ( 𝐴 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝐴 ) ) ) ) ) )
66		fveq2	⊢ ( 𝑞 = 𝐵 → ( bday ‘ 𝑞 ) = ( bday ‘ 𝐵 ) )
67	66	uneq2d	⊢ ( 𝑞 = 𝐵 → ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝑞 ) ) = ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) )
68	67	eqeq2d	⊢ ( 𝑞 = 𝐵 → ( 𝑎 = ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝑞 ) ) ↔ 𝑎 = ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) ) )
69		breq2	⊢ ( 𝑞 = 𝐵 → ( 𝐴 <s 𝑞 ↔ 𝐴 <s 𝐵 ) )
70		fveq2	⊢ ( 𝑞 = 𝐵 → ( -us ‘ 𝑞 ) = ( -us ‘ 𝐵 ) )
71	70	breq1d	⊢ ( 𝑞 = 𝐵 → ( ( -us ‘ 𝑞 ) <s ( -us ‘ 𝐴 ) ↔ ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) )
72	69 71	imbi12d	⊢ ( 𝑞 = 𝐵 → ( ( 𝐴 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝐴 ) ) ↔ ( 𝐴 <s 𝐵 → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) ) )
73	72	anbi2d	⊢ ( 𝑞 = 𝐵 → ( ( ( -us ‘ 𝐴 ) ∈ No ∧ ( 𝐴 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝐴 ) ) ) ↔ ( ( -us ‘ 𝐴 ) ∈ No ∧ ( 𝐴 <s 𝐵 → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) ) ) )
74	68 73	imbi12d	⊢ ( 𝑞 = 𝐵 → ( ( 𝑎 = ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝐴 ) ∈ No ∧ ( 𝐴 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝐴 ) ) ) ) ↔ ( 𝑎 = ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝐴 ) ∈ No ∧ ( 𝐴 <s 𝐵 → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) ) ) ) )
75	65 74	rspc2v	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∀ 𝑝 ∈ No ∀ 𝑞 ∈ No ( 𝑎 = ( ( bday ‘ 𝑝 ) ∪ ( bday ‘ 𝑞 ) ) → ( ( -us ‘ 𝑝 ) ∈ No ∧ ( 𝑝 <s 𝑞 → ( -us ‘ 𝑞 ) <s ( -us ‘ 𝑝 ) ) ) ) → ( 𝑎 = ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝐴 ) ∈ No ∧ ( 𝐴 <s 𝐵 → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) ) ) ) )
76	55 75	syl5com	⊢ ( 𝑎 ∈ On → ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑎 = ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝐴 ) ∈ No ∧ ( 𝐴 <s 𝐵 → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) ) ) ) )
77	76	com23	⊢ ( 𝑎 ∈ On → ( 𝑎 = ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( -us ‘ 𝐴 ) ∈ No ∧ ( 𝐴 <s 𝐵 → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) ) ) ) )
78	77	rexlimiv	⊢ ( ∃ 𝑎 ∈ On 𝑎 = ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( -us ‘ 𝐴 ) ∈ No ∧ ( 𝐴 <s 𝐵 → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) ) ) )
79	5 78	ax-mp	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( -us ‘ 𝐴 ) ∈ No ∧ ( 𝐴 <s 𝐵 → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) ) )