Metamath Proof Explorer

Theorem precsexlem6

Description: Lemma for surreal reciprocal. Show that L 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 precsexlem6 ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝐼 ⊆ 𝐽 ) → ( 𝐿 ‘ 𝐼 ) ⊆ ( 𝐿 ‘ 𝐽 ) )

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 𝑗 ) ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ ( 𝐼 +o 𝑗 ) ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ ( 𝐼 +o 𝑗 ) ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) )
19 1 2 3 precsexlem4 ⊢ ( ( 𝐼 +o 𝑗 ) ∈ ω → ( 𝐿 ‘ suc ( 𝐼 +o 𝑗 ) ) = ( ( 𝐿 ‘ ( 𝐼 +o 𝑗 ) ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ ( 𝐼 +o 𝑗 ) ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ ( 𝐼 +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 ⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝐼 ⊆ 𝐽 ) → ( 𝐿 ‘ 𝐼 ) ⊆ ( 𝐿 ‘ 𝐽 ) )