Theorem precsexlem10 28160

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.

Step	Hyp	Ref	Expression
1		fo1st 7968	. . . . . . . 8 ⊢ 1st :V–onto→V
2		fofun 6756	. . . . . . . 8 ⊢ (1st :V–onto→V → Fun 1st )
3	1, 2	ax-mp 5	. . . . . . 7 ⊢ Fun 1st
4		rdgfun 8362	. . . . . . . 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 }, ∅⟩)
6	5	funeqi 6522	. . . . . . . 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 }, ∅⟩))
7	4, 6	mpbir 231	. . . . . . 7 ⊢ Fun 𝐹
8		funco 6541	. . . . . . 7 ⊢ ((Fun 1st ∧ Fun 𝐹) → Fun (1st ∘ 𝐹))
9	3, 7, 8	mp2an 692	. . . . . 6 ⊢ Fun (1st ∘ 𝐹)
10		precsexlem.2	. . . . . . 7 ⊢ 𝐿 = (1st ∘ 𝐹)
11	10	funeqi 6522	. . . . . 6 ⊢ (Fun 𝐿 ↔ Fun (1st ∘ 𝐹))
12	9, 11	mpbir 231	. . . . 5 ⊢ Fun 𝐿
13		dcomex 10379	. . . . . 6 ⊢ ω ∈ V
14	13	funimaex 6589	. . . . 5 ⊢ (Fun 𝐿 → (𝐿 “ ω) ∈ V)
15	12, 14	ax-mp 5	. . . 4 ⊢ (𝐿 “ ω) ∈ V
16	15	uniex 7698	. . 3 ⊢ ∪ (𝐿 “ ω) ∈ V
17	16	a1i 11	. 2 ⊢ (𝜑 → ∪ (𝐿 “ ω) ∈ V)
18		fo2nd 7969	. . . . . . . 8 ⊢ 2nd :V–onto→V
19		fofun 6756	. . . . . . . 8 ⊢ (2nd :V–onto→V → Fun 2nd )
20	18, 19	ax-mp 5	. . . . . . 7 ⊢ Fun 2nd
21		funco 6541	. . . . . . 7 ⊢ ((Fun 2nd ∧ Fun 𝐹) → Fun (2nd ∘ 𝐹))
22	20, 7, 21	mp2an 692	. . . . . 6 ⊢ Fun (2nd ∘ 𝐹)
23		precsexlem.3	. . . . . . 7 ⊢ 𝑅 = (2nd ∘ 𝐹)
24	23	funeqi 6522	. . . . . 6 ⊢ (Fun 𝑅 ↔ Fun (2nd ∘ 𝐹))
25	22, 24	mpbir 231	. . . . 5 ⊢ Fun 𝑅
26	13	funimaex 6589	. . . . 5 ⊢ (Fun 𝑅 → (𝑅 “ ω) ∈ V)
27	25, 26	ax-mp 5	. . . 4 ⊢ (𝑅 “ ω) ∈ V
28	27	uniex 7698	. . 3 ⊢ ∪ (𝑅 “ ω) ∈ V
29	28	a1i 11	. 2 ⊢ (𝜑 → ∪ (𝑅 “ ω) ∈ V)
30		funiunfv 7205	. . . 4 ⊢ (Fun 𝐿 → ∪ 𝑖 ∈ ω (𝐿‘𝑖) = ∪ (𝐿 “ ω))
31	12, 30	ax-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 ))
35	5, 10, 23, 32, 33, 34	precsexlem8 28158	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ ω) → ((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No ))
36	35	simpld 494	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ω) → (𝐿‘𝑖) ⊆ No )
37	36	iunssd 5009	. . 3 ⊢ (𝜑 → ∪ 𝑖 ∈ ω (𝐿‘𝑖) ⊆ No )
38	31, 37	eqsstrrid 3983	. 2 ⊢ (𝜑 → ∪ (𝐿 “ ω) ⊆ No )
39		funiunfv 7205	. . . 4 ⊢ (Fun 𝑅 → ∪ 𝑖 ∈ ω (𝑅‘𝑖) = ∪ (𝑅 “ ω))
40	25, 39	ax-mp 5	. . 3 ⊢ ∪ 𝑖 ∈ ω (𝑅‘𝑖) = ∪ (𝑅 “ ω)
41	35	simprd 495	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ω) → (𝑅‘𝑖) ⊆ No )
42	41	iunssd 5009	. . 3 ⊢ (𝜑 → ∪ 𝑖 ∈ ω (𝑅‘𝑖) ⊆ No )
43	40, 42	eqsstrrid 3983	. 2 ⊢ (𝜑 → ∪ (𝑅 “ ω) ⊆ No )
44	31	eleq2i 2820	. . . . . . 7 ⊢ (𝑏 ∈ ∪ 𝑖 ∈ ω (𝐿‘𝑖) ↔ 𝑏 ∈ ∪ (𝐿 “ ω))
45		eliun 4955	. . . . . . 7 ⊢ (𝑏 ∈ ∪ 𝑖 ∈ ω (𝐿‘𝑖) ↔ ∃𝑖 ∈ ω 𝑏 ∈ (𝐿‘𝑖))
46	44, 45	bitr3i 277	. . . . . 6 ⊢ (𝑏 ∈ ∪ (𝐿 “ ω) ↔ ∃𝑖 ∈ ω 𝑏 ∈ (𝐿‘𝑖))
47		funiunfv 7205	. . . . . . . . 9 ⊢ (Fun 𝑅 → ∪ 𝑗 ∈ ω (𝑅‘𝑗) = ∪ (𝑅 “ ω))
48	25, 47	ax-mp 5	. . . . . . . 8 ⊢ ∪ 𝑗 ∈ ω (𝑅‘𝑗) = ∪ (𝑅 “ ω)
49	48	eleq2i 2820	. . . . . . 7 ⊢ (𝑐 ∈ ∪ 𝑗 ∈ ω (𝑅‘𝑗) ↔ 𝑐 ∈ ∪ (𝑅 “ ω))
50		eliun 4955	. . . . . . 7 ⊢ (𝑐 ∈ ∪ 𝑗 ∈ ω (𝑅‘𝑗) ↔ ∃𝑗 ∈ ω 𝑐 ∈ (𝑅‘𝑗))
51	49, 50	bitr3i 277	. . . . . 6 ⊢ (𝑐 ∈ ∪ (𝑅 “ ω) ↔ ∃𝑗 ∈ ω 𝑐 ∈ (𝑅‘𝑗))
52	46, 51	anbi12i 628	. . . . 5 ⊢ ((𝑏 ∈ ∪ (𝐿 “ ω) ∧ 𝑐 ∈ ∪ (𝑅 “ ω)) ↔ (∃𝑖 ∈ ω 𝑏 ∈ (𝐿‘𝑖) ∧ ∃𝑗 ∈ ω 𝑐 ∈ (𝑅‘𝑗)))
53		reeanv 3207	. . . . 5 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑏 ∈ (𝐿‘𝑖) ∧ 𝑐 ∈ (𝑅‘𝑗)) ↔ (∃𝑖 ∈ ω 𝑏 ∈ (𝐿‘𝑖) ∧ ∃𝑗 ∈ ω 𝑐 ∈ (𝑅‘𝑗)))
54	52, 53	bitr4i 278	. . . 4 ⊢ ((𝑏 ∈ ∪ (𝐿 “ ω) ∧ 𝑐 ∈ ∪ (𝑅 “ ω)) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑏 ∈ (𝐿‘𝑖) ∧ 𝑐 ∈ (𝑅‘𝑗)))
55		omun 7845	. . . . . . . . 9 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖 ∪ 𝑗) ∈ ω)
56		ssun1 4137	. . . . . . . . . 10 ⊢ 𝑖 ⊆ (𝑖 ∪ 𝑗)
57	5, 10, 23	precsexlem6 28156	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ω ∧ (𝑖 ∪ 𝑗) ∈ ω ∧ 𝑖 ⊆ (𝑖 ∪ 𝑗)) → (𝐿‘𝑖) ⊆ (𝐿‘(𝑖 ∪ 𝑗)))
58	56, 57	mp3an3 1452	. . . . . . . . 9 ⊢ ((𝑖 ∈ ω ∧ (𝑖 ∪ 𝑗) ∈ ω) → (𝐿‘𝑖) ⊆ (𝐿‘(𝑖 ∪ 𝑗)))
59	55, 58	syldan 591	. . . . . . . 8 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝐿‘𝑖) ⊆ (𝐿‘(𝑖 ∪ 𝑗)))
60	59	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → (𝐿‘𝑖) ⊆ (𝐿‘(𝑖 ∪ 𝑗)))
61	60	sseld 3942	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → (𝑏 ∈ (𝐿‘𝑖) → 𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗))))
62		simpr 484	. . . . . . . . 9 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → 𝑗 ∈ ω)
63		ssun2 4138	. . . . . . . . . 10 ⊢ 𝑗 ⊆ (𝑖 ∪ 𝑗)
64	5, 10, 23	precsexlem7 28157	. . . . . . . . . 10 ⊢ ((𝑗 ∈ ω ∧ (𝑖 ∪ 𝑗) ∈ ω ∧ 𝑗 ⊆ (𝑖 ∪ 𝑗)) → (𝑅‘𝑗) ⊆ (𝑅‘(𝑖 ∪ 𝑗)))
65	63, 64	mp3an3 1452	. . . . . . . . 9 ⊢ ((𝑗 ∈ ω ∧ (𝑖 ∪ 𝑗) ∈ ω) → (𝑅‘𝑗) ⊆ (𝑅‘(𝑖 ∪ 𝑗)))
66	62, 55, 65	syl2anc 584	. . . . . . . 8 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑅‘𝑗) ⊆ (𝑅‘(𝑖 ∪ 𝑗)))
67	66	sseld 3942	. . . . . . 7 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑐 ∈ (𝑅‘𝑗) → 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗))))
68	67	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → (𝑐 ∈ (𝑅‘𝑗) → 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗))))
69	32	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → 𝐴 ∈ No )
70	5, 10, 23, 32, 33, 34	precsexlem8 28158	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → ((𝐿‘(𝑖 ∪ 𝑗)) ⊆ No ∧ (𝑅‘(𝑖 ∪ 𝑗)) ⊆ No ))
71	70	simpld 494	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → (𝐿‘(𝑖 ∪ 𝑗)) ⊆ No )
72	71	sselda 3943	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ 𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗))) → 𝑏 ∈ No )
73	72	adantrr 717	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → 𝑏 ∈ No )
74	69, 73	mulscld 28080	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → (𝐴 ·s 𝑏) ∈ No )
75	70	simprd 495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → (𝑅‘(𝑖 ∪ 𝑗)) ⊆ No )
76	75	sselda 3943	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗))) → 𝑐 ∈ No )
77	76	adantrl 716	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → 𝑐 ∈ No )
78	69, 77	mulscld 28080	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → (𝐴 ·s 𝑐) ∈ No )
79	74, 78	jca 511	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → ((𝐴 ·s 𝑏) ∈ No ∧ (𝐴 ·s 𝑐) ∈ No ))
80	5, 10, 23, 32, 33, 34	precsexlem9 28159	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → (∀𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗))(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)) 1s <s (𝐴 ·s 𝑐)))
81	80	simpld 494	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → ∀𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗))(𝐴 ·s 𝑏) <s 1s )
82		rsp 3223	. . . . . . . . . . . . 13 ⊢ (∀𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗))(𝐴 ·s 𝑏) <s 1s → (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) → (𝐴 ·s 𝑏) <s 1s ))
83	81, 82	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) → (𝐴 ·s 𝑏) <s 1s ))
84	80	simprd 495	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → ∀𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)) 1s <s (𝐴 ·s 𝑐))
85		rsp 3223	. . . . . . . . . . . . 13 ⊢ (∀𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)) 1s <s (𝐴 ·s 𝑐) → (𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)) → 1s <s (𝐴 ·s 𝑐)))
86	84, 85	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → (𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)) → 1s <s (𝐴 ·s 𝑐)))
87	83, 86	anim12d 609	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → ((𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗))) → ((𝐴 ·s 𝑏) <s 1s ∧ 1s <s (𝐴 ·s 𝑐))))
88	87	imp 406	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → ((𝐴 ·s 𝑏) <s 1s ∧ 1s <s (𝐴 ·s 𝑐)))
89		1sno 27778	. . . . . . . . . . 11 ⊢ 1s ∈ No
90		slttr 27694	. . . . . . . . . . 11 ⊢ (((𝐴 ·s 𝑏) ∈ No ∧ 1s ∈ No ∧ (𝐴 ·s 𝑐) ∈ No ) → (((𝐴 ·s 𝑏) <s 1s ∧ 1s <s (𝐴 ·s 𝑐)) → (𝐴 ·s 𝑏) <s (𝐴 ·s 𝑐)))
91	89, 90	mp3an2 1451	. . . . . . . . . 10 ⊢ (((𝐴 ·s 𝑏) ∈ No ∧ (𝐴 ·s 𝑐) ∈ No ) → (((𝐴 ·s 𝑏) <s 1s ∧ 1s <s (𝐴 ·s 𝑐)) → (𝐴 ·s 𝑏) <s (𝐴 ·s 𝑐)))
92	79, 88, 91	sylc 65	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → (𝐴 ·s 𝑏) <s (𝐴 ·s 𝑐))
93	33	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → 0s <s 𝐴)
94	73, 77, 69, 93	sltmul2d 28117	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → (𝑏 <s 𝑐 ↔ (𝐴 ·s 𝑏) <s (𝐴 ·s 𝑐)))
95	92, 94	mpbird 257	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → 𝑏 <s 𝑐)
96	95	ex 412	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → ((𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗))) → 𝑏 <s 𝑐))
97	55, 96	sylan2 593	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗))) → 𝑏 <s 𝑐))
98	61, 68, 97	syl2and 608	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑏 ∈ (𝐿‘𝑖) ∧ 𝑐 ∈ (𝑅‘𝑗)) → 𝑏 <s 𝑐))
99	98	rexlimdvva 3192	. . . 4 ⊢ (𝜑 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑏 ∈ (𝐿‘𝑖) ∧ 𝑐 ∈ (𝑅‘𝑗)) → 𝑏 <s 𝑐))
100	54, 99	biimtrid 242	. . 3 ⊢ (𝜑 → ((𝑏 ∈ ∪ (𝐿 “ ω) ∧ 𝑐 ∈ ∪ (𝑅 “ ω)) → 𝑏 <s 𝑐))
101	100	3impib 1116	. 2 ⊢ ((𝜑 ∧ 𝑏 ∈ ∪ (𝐿 “ ω) ∧ 𝑐 ∈ ∪ (𝑅 “ ω)) → 𝑏 <s 𝑐)
102	17, 29, 38, 43, 101	ssltd 27739	1 ⊢ (𝜑 → ∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {cab 2707  ∀wral 3044  ∃wrex 3053  {crab 3402  Vcvv 3444  ⦋csb 3859   ∪ cun 3909   ⊆ wss 3911  ∅c0 4292  {csn 4585  ⟨cop 4591  ∪ cuni 4867  ∪ ciun 4951   class class class wbr 5102   ↦ cmpt 5183   “ cima 5634   ∘ ccom 5635  Fun wfun 6494  –onto→wfo 6498  ‘cfv 6500  (class class class)co 7370  ωcom 7823  1^st c1st 7946  2^nd c2nd 7947  reccrdg 8355   No csur 27586   <s cslt 27587   <<s csslt 27728   0_s c0s 27773   1_s c1s 27774   L cleft 27792   R cright 27793   +_s cadds 27908   -_s csubs 27968   ·_s cmuls 28051   /_su cdivs 28132

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7692  ax-dc 10378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-ot 4594  df-uni 4868  df-int 4907  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6263  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6453  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-om 7824  df-1st 7948  df-2nd 7949  df-frecs 8238  df-wrecs 8269  df-recs 8318  df-rdg 8356  df-1o 8412  df-2o 8413  df-oadd 8416  df-nadd 8608  df-no 27589  df-slt 27590  df-bday 27591  df-sle 27692  df-sslt 27729  df-scut 27731  df-0s 27775  df-1s 27776  df-made 27794  df-old 27795  df-left 27797  df-right 27798  df-norec 27887  df-norec2 27898  df-adds 27909  df-negs 27969  df-subs 27970  df-muls 28052  df-divs 28133

This theorem is referenced by:  precsexlem11  28161  precsex  28162