MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  precsexlem10 Structured version   Visualization version   GIF version

Theorem precsexlem10 28240
Description: Lemma for surreal reciprocal. Show that the union of the left sets is less than the union of the right sets. Note that this is the first theorem in the surreal numbers to require the axiom of infinity. (Contributed by Scott Fenton, 15-Mar-2025.)
Hypotheses
Ref Expression
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𝐹)
precsexlem.4 (𝜑𝐴 No )
precsexlem.5 (𝜑 → 0s <s 𝐴)
precsexlem.6 (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 No (𝑥𝑂 ·s 𝑦) = 1s ))
Assertion
Ref Expression
precsexlem10 (𝜑 (𝐿 “ ω) <<s (𝑅 “ ω))
Distinct variable groups:   𝐴,𝑎,𝑙,𝑝,𝑟,𝑥,𝑥𝑂,𝑥𝐿,𝑥𝑅,𝑦,𝑦𝐿,𝑦𝑅   𝐹,𝑙,𝑝   𝐿,𝑎,𝑙,𝑥𝐿,𝑥𝑅,𝑦𝐿,𝑦𝑅   𝑅,𝑎,𝑙,𝑟,𝑥𝐿,𝑥𝑅,𝑦𝐿,𝑦𝑅   𝜑,𝑎,𝑥𝐿,𝑥𝑅,𝑦𝐿,𝑦𝑅   𝐿,𝑟   𝜑,𝑟
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑝,𝑙,𝑥𝑂)   𝑅(𝑥,𝑦,𝑝,𝑥𝑂)   𝐹(𝑥,𝑦,𝑟,𝑎,𝑥𝑂,𝑥𝐿,𝑥𝑅,𝑦𝐿,𝑦𝑅)   𝐿(𝑥,𝑦,𝑝,𝑥𝑂)

Proof of Theorem precsexlem10
Dummy variables 𝑖 𝑗 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fo1st 8034 . . . . . . . 8 1st :V–onto→V
2 fofun 6821 . . . . . . . 8 (1st :V–onto→V → Fun 1st )
31, 2ax-mp 5 . . . . . . 7 Fun 1st
4 rdgfun 8456 . . . . . . . 8 Fun 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 }, ∅⟩)
5 precsexlem.1 . . . . . . . . 9 𝐹 = 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 }, ∅⟩)
65funeqi 6587 . . . . . . . 8 (Fun 𝐹 ↔ Fun 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 }, ∅⟩))
74, 6mpbir 231 . . . . . . 7 Fun 𝐹
8 funco 6606 . . . . . . 7 ((Fun 1st ∧ Fun 𝐹) → Fun (1st𝐹))
93, 7, 8mp2an 692 . . . . . 6 Fun (1st𝐹)
10 precsexlem.2 . . . . . . 7 𝐿 = (1st𝐹)
1110funeqi 6587 . . . . . 6 (Fun 𝐿 ↔ Fun (1st𝐹))
129, 11mpbir 231 . . . . 5 Fun 𝐿
13 dcomex 10487 . . . . . 6 ω ∈ V
1413funimaex 6655 . . . . 5 (Fun 𝐿 → (𝐿 “ ω) ∈ V)
1512, 14ax-mp 5 . . . 4 (𝐿 “ ω) ∈ V
1615uniex 7761 . . 3 (𝐿 “ ω) ∈ V
1716a1i 11 . 2 (𝜑 (𝐿 “ ω) ∈ V)
18 fo2nd 8035 . . . . . . . 8 2nd :V–onto→V
19 fofun 6821 . . . . . . . 8 (2nd :V–onto→V → Fun 2nd )
2018, 19ax-mp 5 . . . . . . 7 Fun 2nd
21 funco 6606 . . . . . . 7 ((Fun 2nd ∧ Fun 𝐹) → Fun (2nd𝐹))
2220, 7, 21mp2an 692 . . . . . 6 Fun (2nd𝐹)
23 precsexlem.3 . . . . . . 7 𝑅 = (2nd𝐹)
2423funeqi 6587 . . . . . 6 (Fun 𝑅 ↔ Fun (2nd𝐹))
2522, 24mpbir 231 . . . . 5 Fun 𝑅
2613funimaex 6655 . . . . 5 (Fun 𝑅 → (𝑅 “ ω) ∈ V)
2725, 26ax-mp 5 . . . 4 (𝑅 “ ω) ∈ V
2827uniex 7761 . . 3 (𝑅 “ ω) ∈ V
2928a1i 11 . 2 (𝜑 (𝑅 “ ω) ∈ V)
30 funiunfv 7268 . . . 4 (Fun 𝐿 𝑖 ∈ ω (𝐿𝑖) = (𝐿 “ ω))
3112, 30ax-mp 5 . . 3 𝑖 ∈ ω (𝐿𝑖) = (𝐿 “ ω)
32 precsexlem.4 . . . . . 6 (𝜑𝐴 No )
33 precsexlem.5 . . . . . 6 (𝜑 → 0s <s 𝐴)
34 precsexlem.6 . . . . . 6 (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 No (𝑥𝑂 ·s 𝑦) = 1s ))
355, 10, 23, 32, 33, 34precsexlem8 28238 . . . . 5 ((𝜑𝑖 ∈ ω) → ((𝐿𝑖) ⊆ No ∧ (𝑅𝑖) ⊆ No ))
3635simpld 494 . . . 4 ((𝜑𝑖 ∈ ω) → (𝐿𝑖) ⊆ No )
3736iunssd 5050 . . 3 (𝜑 𝑖 ∈ ω (𝐿𝑖) ⊆ No )
3831, 37eqsstrrid 4023 . 2 (𝜑 (𝐿 “ ω) ⊆ No )
39 funiunfv 7268 . . . 4 (Fun 𝑅 𝑖 ∈ ω (𝑅𝑖) = (𝑅 “ ω))
4025, 39ax-mp 5 . . 3 𝑖 ∈ ω (𝑅𝑖) = (𝑅 “ ω)
4135simprd 495 . . . 4 ((𝜑𝑖 ∈ ω) → (𝑅𝑖) ⊆ No )
4241iunssd 5050 . . 3 (𝜑 𝑖 ∈ ω (𝑅𝑖) ⊆ No )
4340, 42eqsstrrid 4023 . 2 (𝜑 (𝑅 “ ω) ⊆ No )
4431eleq2i 2833 . . . . . . 7 (𝑏 𝑖 ∈ ω (𝐿𝑖) ↔ 𝑏 (𝐿 “ ω))
45 eliun 4995 . . . . . . 7 (𝑏 𝑖 ∈ ω (𝐿𝑖) ↔ ∃𝑖 ∈ ω 𝑏 ∈ (𝐿𝑖))
4644, 45bitr3i 277 . . . . . 6 (𝑏 (𝐿 “ ω) ↔ ∃𝑖 ∈ ω 𝑏 ∈ (𝐿𝑖))
47 funiunfv 7268 . . . . . . . . 9 (Fun 𝑅 𝑗 ∈ ω (𝑅𝑗) = (𝑅 “ ω))
4825, 47ax-mp 5 . . . . . . . 8 𝑗 ∈ ω (𝑅𝑗) = (𝑅 “ ω)
4948eleq2i 2833 . . . . . . 7 (𝑐 𝑗 ∈ ω (𝑅𝑗) ↔ 𝑐 (𝑅 “ ω))
50 eliun 4995 . . . . . . 7 (𝑐 𝑗 ∈ ω (𝑅𝑗) ↔ ∃𝑗 ∈ ω 𝑐 ∈ (𝑅𝑗))
5149, 50bitr3i 277 . . . . . 6 (𝑐 (𝑅 “ ω) ↔ ∃𝑗 ∈ ω 𝑐 ∈ (𝑅𝑗))
5246, 51anbi12i 628 . . . . 5 ((𝑏 (𝐿 “ ω) ∧ 𝑐 (𝑅 “ ω)) ↔ (∃𝑖 ∈ ω 𝑏 ∈ (𝐿𝑖) ∧ ∃𝑗 ∈ ω 𝑐 ∈ (𝑅𝑗)))
53 reeanv 3229 . . . . 5 (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑏 ∈ (𝐿𝑖) ∧ 𝑐 ∈ (𝑅𝑗)) ↔ (∃𝑖 ∈ ω 𝑏 ∈ (𝐿𝑖) ∧ ∃𝑗 ∈ ω 𝑐 ∈ (𝑅𝑗)))
5452, 53bitr4i 278 . . . 4 ((𝑏 (𝐿 “ ω) ∧ 𝑐 (𝑅 “ ω)) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑏 ∈ (𝐿𝑖) ∧ 𝑐 ∈ (𝑅𝑗)))
55 omun 7909 . . . . . . . . 9 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖𝑗) ∈ ω)
56 ssun1 4178 . . . . . . . . . 10 𝑖 ⊆ (𝑖𝑗)
575, 10, 23precsexlem6 28236 . . . . . . . . . 10 ((𝑖 ∈ ω ∧ (𝑖𝑗) ∈ ω ∧ 𝑖 ⊆ (𝑖𝑗)) → (𝐿𝑖) ⊆ (𝐿‘(𝑖𝑗)))
5856, 57mp3an3 1452 . . . . . . . . 9 ((𝑖 ∈ ω ∧ (𝑖𝑗) ∈ ω) → (𝐿𝑖) ⊆ (𝐿‘(𝑖𝑗)))
5955, 58syldan 591 . . . . . . . 8 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝐿𝑖) ⊆ (𝐿‘(𝑖𝑗)))
6059adantl 481 . . . . . . 7 ((𝜑 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → (𝐿𝑖) ⊆ (𝐿‘(𝑖𝑗)))
6160sseld 3982 . . . . . 6 ((𝜑 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → (𝑏 ∈ (𝐿𝑖) → 𝑏 ∈ (𝐿‘(𝑖𝑗))))
62 simpr 484 . . . . . . . . 9 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → 𝑗 ∈ ω)
63 ssun2 4179 . . . . . . . . . 10 𝑗 ⊆ (𝑖𝑗)
645, 10, 23precsexlem7 28237 . . . . . . . . . 10 ((𝑗 ∈ ω ∧ (𝑖𝑗) ∈ ω ∧ 𝑗 ⊆ (𝑖𝑗)) → (𝑅𝑗) ⊆ (𝑅‘(𝑖𝑗)))
6563, 64mp3an3 1452 . . . . . . . . 9 ((𝑗 ∈ ω ∧ (𝑖𝑗) ∈ ω) → (𝑅𝑗) ⊆ (𝑅‘(𝑖𝑗)))
6662, 55, 65syl2anc 584 . . . . . . . 8 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑅𝑗) ⊆ (𝑅‘(𝑖𝑗)))
6766sseld 3982 . . . . . . 7 ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑐 ∈ (𝑅𝑗) → 𝑐 ∈ (𝑅‘(𝑖𝑗))))
6867adantl 481 . . . . . 6 ((𝜑 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → (𝑐 ∈ (𝑅𝑗) → 𝑐 ∈ (𝑅‘(𝑖𝑗))))
6932ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖𝑗)))) → 𝐴 No )
705, 10, 23, 32, 33, 34precsexlem8 28238 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖𝑗) ∈ ω) → ((𝐿‘(𝑖𝑗)) ⊆ No ∧ (𝑅‘(𝑖𝑗)) ⊆ No ))
7170simpld 494 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖𝑗) ∈ ω) → (𝐿‘(𝑖𝑗)) ⊆ No )
7271sselda 3983 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑗) ∈ ω) ∧ 𝑏 ∈ (𝐿‘(𝑖𝑗))) → 𝑏 No )
7372adantrr 717 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖𝑗)))) → 𝑏 No )
7469, 73mulscld 28161 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖𝑗)))) → (𝐴 ·s 𝑏) ∈ No )
7570simprd 495 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖𝑗) ∈ ω) → (𝑅‘(𝑖𝑗)) ⊆ No )
7675sselda 3983 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖𝑗) ∈ ω) ∧ 𝑐 ∈ (𝑅‘(𝑖𝑗))) → 𝑐 No )
7776adantrl 716 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖𝑗)))) → 𝑐 No )
7869, 77mulscld 28161 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖𝑗)))) → (𝐴 ·s 𝑐) ∈ No )
7974, 78jca 511 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖𝑗)))) → ((𝐴 ·s 𝑏) ∈ No ∧ (𝐴 ·s 𝑐) ∈ No ))
805, 10, 23, 32, 33, 34precsexlem9 28239 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖𝑗) ∈ ω) → (∀𝑏 ∈ (𝐿‘(𝑖𝑗))(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘(𝑖𝑗)) 1s <s (𝐴 ·s 𝑐)))
8180simpld 494 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖𝑗) ∈ ω) → ∀𝑏 ∈ (𝐿‘(𝑖𝑗))(𝐴 ·s 𝑏) <s 1s )
82 rsp 3247 . . . . . . . . . . . . 13 (∀𝑏 ∈ (𝐿‘(𝑖𝑗))(𝐴 ·s 𝑏) <s 1s → (𝑏 ∈ (𝐿‘(𝑖𝑗)) → (𝐴 ·s 𝑏) <s 1s ))
8381, 82syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖𝑗) ∈ ω) → (𝑏 ∈ (𝐿‘(𝑖𝑗)) → (𝐴 ·s 𝑏) <s 1s ))
8480simprd 495 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖𝑗) ∈ ω) → ∀𝑐 ∈ (𝑅‘(𝑖𝑗)) 1s <s (𝐴 ·s 𝑐))
85 rsp 3247 . . . . . . . . . . . . 13 (∀𝑐 ∈ (𝑅‘(𝑖𝑗)) 1s <s (𝐴 ·s 𝑐) → (𝑐 ∈ (𝑅‘(𝑖𝑗)) → 1s <s (𝐴 ·s 𝑐)))
8684, 85syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖𝑗) ∈ ω) → (𝑐 ∈ (𝑅‘(𝑖𝑗)) → 1s <s (𝐴 ·s 𝑐)))
8783, 86anim12d 609 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖𝑗) ∈ ω) → ((𝑏 ∈ (𝐿‘(𝑖𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖𝑗))) → ((𝐴 ·s 𝑏) <s 1s ∧ 1s <s (𝐴 ·s 𝑐))))
8887imp 406 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖𝑗)))) → ((𝐴 ·s 𝑏) <s 1s ∧ 1s <s (𝐴 ·s 𝑐)))
89 1sno 27872 . . . . . . . . . . 11 1s No
90 slttr 27792 . . . . . . . . . . 11 (((𝐴 ·s 𝑏) ∈ No ∧ 1s No ∧ (𝐴 ·s 𝑐) ∈ No ) → (((𝐴 ·s 𝑏) <s 1s ∧ 1s <s (𝐴 ·s 𝑐)) → (𝐴 ·s 𝑏) <s (𝐴 ·s 𝑐)))
9189, 90mp3an2 1451 . . . . . . . . . 10 (((𝐴 ·s 𝑏) ∈ No ∧ (𝐴 ·s 𝑐) ∈ No ) → (((𝐴 ·s 𝑏) <s 1s ∧ 1s <s (𝐴 ·s 𝑐)) → (𝐴 ·s 𝑏) <s (𝐴 ·s 𝑐)))
9279, 88, 91sylc 65 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖𝑗)))) → (𝐴 ·s 𝑏) <s (𝐴 ·s 𝑐))
9333ad2antrr 726 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖𝑗)))) → 0s <s 𝐴)
9473, 77, 69, 93sltmul2d 28198 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖𝑗)))) → (𝑏 <s 𝑐 ↔ (𝐴 ·s 𝑏) <s (𝐴 ·s 𝑐)))
9592, 94mpbird 257 . . . . . . . 8 (((𝜑 ∧ (𝑖𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖𝑗)))) → 𝑏 <s 𝑐)
9695ex 412 . . . . . . 7 ((𝜑 ∧ (𝑖𝑗) ∈ ω) → ((𝑏 ∈ (𝐿‘(𝑖𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖𝑗))) → 𝑏 <s 𝑐))
9755, 96sylan2 593 . . . . . 6 ((𝜑 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑏 ∈ (𝐿‘(𝑖𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖𝑗))) → 𝑏 <s 𝑐))
9861, 68, 97syl2and 608 . . . . 5 ((𝜑 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑏 ∈ (𝐿𝑖) ∧ 𝑐 ∈ (𝑅𝑗)) → 𝑏 <s 𝑐))
9998rexlimdvva 3213 . . . 4 (𝜑 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑏 ∈ (𝐿𝑖) ∧ 𝑐 ∈ (𝑅𝑗)) → 𝑏 <s 𝑐))
10054, 99biimtrid 242 . . 3 (𝜑 → ((𝑏 (𝐿 “ ω) ∧ 𝑐 (𝑅 “ ω)) → 𝑏 <s 𝑐))
1011003impib 1117 . 2 ((𝜑𝑏 (𝐿 “ ω) ∧ 𝑐 (𝑅 “ ω)) → 𝑏 <s 𝑐)
10217, 29, 38, 43, 101ssltd 27836 1 (𝜑 (𝐿 “ ω) <<s (𝑅 “ ω))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  {cab 2714  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  csb 3899  cun 3949  wss 3951  c0 4333  {csn 4626  cop 4632   cuni 4907   ciun 4991   class class class wbr 5143  cmpt 5225  cima 5688  ccom 5689  Fun wfun 6555  ontowfo 6559  cfv 6561  (class class class)co 7431  ωcom 7887  1st c1st 8012  2nd c2nd 8013  reccrdg 8449   No csur 27684   <s cslt 27685   <<s csslt 27825   0s c0s 27867   1s c1s 27868   L cleft 27884   R cright 27885   +s cadds 27992   -s csubs 28052   ·s cmuls 28132   /su cdivs 28213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-dc 10486
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-ot 4635  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-nadd 8704  df-no 27687  df-slt 27688  df-bday 27689  df-sle 27790  df-sslt 27826  df-scut 27828  df-0s 27869  df-1s 27870  df-made 27886  df-old 27887  df-left 27889  df-right 27890  df-norec 27971  df-norec2 27982  df-adds 27993  df-negs 28053  df-subs 28054  df-muls 28133  df-divs 28214
This theorem is referenced by:  precsexlem11  28241  precsex  28242
  Copyright terms: Public domain W3C validator