Theorem precsexlem7

Description: Lemma for surreal reciprocal. Show that R is non-strictly increasing in its argument. (Contributed by Scott Fenton, 15-Mar-2025)

	Ref	Expression
Hypotheses	precsexlem.1	⊢ 𝐹 = rec ( ( 𝑝 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑙 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑟 ⦌ ⟨ ( 𝑙 ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) , ( 𝑟 ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) ⟩ ) , ⟨ { 0s } , ∅ ⟩ )
	precsexlem.2	⊢ 𝐿 = ( 1st ∘ 𝐹 )
	precsexlem.3	⊢ 𝑅 = ( 2nd ∘ 𝐹 )
Assertion	precsexlem7	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝐼 ⊆ 𝐽 ) → ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		precsexlem.1	⊢ 𝐹 = rec ( ( 𝑝 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑙 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑟 ⦌ ⟨ ( 𝑙 ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) , ( 𝑟 ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) ⟩ ) , ⟨ { 0s } , ∅ ⟩ )
2		precsexlem.2	⊢ 𝐿 = ( 1st ∘ 𝐹 )
3		precsexlem.3	⊢ 𝑅 = ( 2nd ∘ 𝐹 )
4		nnawordex	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ( 𝐼 ⊆ 𝐽 ↔ ∃ 𝑘 ∈ ω ( 𝐼 +o 𝑘 ) = 𝐽 ) )
5		oveq2	⊢ ( 𝑘 = ∅ → ( 𝐼 +o 𝑘 ) = ( 𝐼 +o ∅ ) )
6	5	fveq2d	⊢ ( 𝑘 = ∅ → ( 𝑅 ‘ ( 𝐼 +o 𝑘 ) ) = ( 𝑅 ‘ ( 𝐼 +o ∅ ) ) )
7	6	sseq2d	⊢ ( 𝑘 = ∅ → ( ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ ( 𝐼 +o 𝑘 ) ) ↔ ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ ( 𝐼 +o ∅ ) ) ) )
8		oveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐼 +o 𝑘 ) = ( 𝐼 +o 𝑗 ) )
9	8	fveq2d	⊢ ( 𝑘 = 𝑗 → ( 𝑅 ‘ ( 𝐼 +o 𝑘 ) ) = ( 𝑅 ‘ ( 𝐼 +o 𝑗 ) ) )
10	9	sseq2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ ( 𝐼 +o 𝑘 ) ) ↔ ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ ( 𝐼 +o 𝑗 ) ) ) )
11		oveq2	⊢ ( 𝑘 = suc 𝑗 → ( 𝐼 +o 𝑘 ) = ( 𝐼 +o suc 𝑗 ) )
12	11	fveq2d	⊢ ( 𝑘 = suc 𝑗 → ( 𝑅 ‘ ( 𝐼 +o 𝑘 ) ) = ( 𝑅 ‘ ( 𝐼 +o suc 𝑗 ) ) )
13	12	sseq2d	⊢ ( 𝑘 = suc 𝑗 → ( ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ ( 𝐼 +o 𝑘 ) ) ↔ ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ ( 𝐼 +o suc 𝑗 ) ) ) )
14		nna0	⊢ ( 𝐼 ∈ ω → ( 𝐼 +o ∅ ) = 𝐼 )
15	14	fveq2d	⊢ ( 𝐼 ∈ ω → ( 𝑅 ‘ ( 𝐼 +o ∅ ) ) = ( 𝑅 ‘ 𝐼 ) )
16	15	eqimsscd	⊢ ( 𝐼 ∈ ω → ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ ( 𝐼 +o ∅ ) ) )
17		nnacl	⊢ ( ( 𝐼 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝐼 +o 𝑗 ) ∈ ω )
18		ssun1	⊢ ( 𝑅 ‘ ( 𝐼 +o 𝑗 ) ) ⊆ ( ( 𝑅 ‘ ( 𝐼 +o 𝑗 ) ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ ( 𝐼 +o 𝑗 ) ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ ( 𝐼 +o 𝑗 ) ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) )
19	1 2 3	precsexlem5	⊢ ( ( 𝐼 +o 𝑗 ) ∈ ω → ( 𝑅 ‘ suc ( 𝐼 +o 𝑗 ) ) = ( ( 𝑅 ‘ ( 𝐼 +o 𝑗 ) ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ ( 𝐼 +o 𝑗 ) ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ ( 𝐼 +o 𝑗 ) ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) )
20	18 19	sseqtrrid	⊢ ( ( 𝐼 +o 𝑗 ) ∈ ω → ( 𝑅 ‘ ( 𝐼 +o 𝑗 ) ) ⊆ ( 𝑅 ‘ suc ( 𝐼 +o 𝑗 ) ) )
21	17 20	syl	⊢ ( ( 𝐼 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑅 ‘ ( 𝐼 +o 𝑗 ) ) ⊆ ( 𝑅 ‘ suc ( 𝐼 +o 𝑗 ) ) )
22		nnasuc	⊢ ( ( 𝐼 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝐼 +o suc 𝑗 ) = suc ( 𝐼 +o 𝑗 ) )
23	22	fveq2d	⊢ ( ( 𝐼 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑅 ‘ ( 𝐼 +o suc 𝑗 ) ) = ( 𝑅 ‘ suc ( 𝐼 +o 𝑗 ) ) )
24	21 23	sseqtrrd	⊢ ( ( 𝐼 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑅 ‘ ( 𝐼 +o 𝑗 ) ) ⊆ ( 𝑅 ‘ ( 𝐼 +o suc 𝑗 ) ) )
25		sstr2	⊢ ( ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ ( 𝐼 +o 𝑗 ) ) → ( ( 𝑅 ‘ ( 𝐼 +o 𝑗 ) ) ⊆ ( 𝑅 ‘ ( 𝐼 +o suc 𝑗 ) ) → ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ ( 𝐼 +o suc 𝑗 ) ) ) )
26	24 25	syl5com	⊢ ( ( 𝐼 ∈ ω ∧ 𝑗 ∈ ω ) → ( ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ ( 𝐼 +o 𝑗 ) ) → ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ ( 𝐼 +o suc 𝑗 ) ) ) )
27	26	expcom	⊢ ( 𝑗 ∈ ω → ( 𝐼 ∈ ω → ( ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ ( 𝐼 +o 𝑗 ) ) → ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ ( 𝐼 +o suc 𝑗 ) ) ) ) )
28	7 10 13 16 27	finds2	⊢ ( 𝑘 ∈ ω → ( 𝐼 ∈ ω → ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ ( 𝐼 +o 𝑘 ) ) ) )
29	28	impcom	⊢ ( ( 𝐼 ∈ ω ∧ 𝑘 ∈ ω ) → ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ ( 𝐼 +o 𝑘 ) ) )
30		fveq2	⊢ ( ( 𝐼 +o 𝑘 ) = 𝐽 → ( 𝑅 ‘ ( 𝐼 +o 𝑘 ) ) = ( 𝑅 ‘ 𝐽 ) )
31	30	sseq2d	⊢ ( ( 𝐼 +o 𝑘 ) = 𝐽 → ( ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ ( 𝐼 +o 𝑘 ) ) ↔ ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ 𝐽 ) ) )
32	29 31	syl5ibcom	⊢ ( ( 𝐼 ∈ ω ∧ 𝑘 ∈ ω ) → ( ( 𝐼 +o 𝑘 ) = 𝐽 → ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ 𝐽 ) ) )
33	32	rexlimdva	⊢ ( 𝐼 ∈ ω → ( ∃ 𝑘 ∈ ω ( 𝐼 +o 𝑘 ) = 𝐽 → ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ 𝐽 ) ) )
34	33	adantr	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ( ∃ 𝑘 ∈ ω ( 𝐼 +o 𝑘 ) = 𝐽 → ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ 𝐽 ) ) )
35	4 34	sylbid	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ( 𝐼 ⊆ 𝐽 → ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ 𝐽 ) ) )
36	35	3impia	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝐼 ⊆ 𝐽 ) → ( 𝑅 ‘ 𝐼 ) ⊆ ( 𝑅 ‘ 𝐽 ) )