precsex - Metamath Proof Explorer

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

Theorem precsex 28313

Description: Every positive surreal has a reciprocal. Theorem 10(iv) of [Conway] p. 21. (Contributed by Scott Fenton, 15-Mar-2025.)

**Assertion**
Ref	Expression
precsex	⊢ ((𝐴 ∈ No ∧ 0_s <s 𝐴) → ∃𝑦 ∈ No (𝐴 ·_s 𝑦) = 1_s )

Distinct variable group: 𝑦,𝐴

Proof of Theorem precsex Dummy variables 𝑎 𝑏 𝑥 𝑥_𝑂 𝑥_𝐿 𝑥_𝑅 𝑦_𝐿 𝑦_𝑅 𝑧 𝑧_𝐿 𝑧_𝑅 𝑙 𝑚 𝑝 𝑞 𝑟 𝑠 𝑡 𝑢 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 5106	. . . 4 ⊢ (𝑧 = 𝑥_𝑂 → ( 0_s <s 𝑧 ↔ 0_s <s 𝑥_𝑂))
2		oveq1 7405	. . . . . 6 ⊢ (𝑧 = 𝑥_𝑂 → (𝑧 ·_s 𝑦) = (𝑥_𝑂 ·_s 𝑦))
3	2	eqeq1d 2766	. . . . 5 ⊢ (𝑧 = 𝑥_𝑂 → ((𝑧 ·_s 𝑦) = 1_s ↔ (𝑥_𝑂 ·_s 𝑦) = 1_s ))
4	3	rexbidv 3188	. . . 4 ⊢ (𝑧 = 𝑥_𝑂 → (∃𝑦 ∈ No (𝑧 ·_s 𝑦) = 1_s ↔ ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s ))
5	1, 4	imbi12d 346	. . 3 ⊢ (𝑧 = 𝑥_𝑂 → (( 0_s <s 𝑧 → ∃𝑦 ∈ No (𝑧 ·_s 𝑦) = 1_s ) ↔ ( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s )))
6		breq2 5106	. . . 4 ⊢ (𝑧 = 𝐴 → ( 0_s <s 𝑧 ↔ 0_s <s 𝐴))
7		oveq1 7405	. . . . . 6 ⊢ (𝑧 = 𝐴 → (𝑧 ·_s 𝑦) = (𝐴 ·_s 𝑦))
8	7	eqeq1d 2766	. . . . 5 ⊢ (𝑧 = 𝐴 → ((𝑧 ·_s 𝑦) = 1_s ↔ (𝐴 ·_s 𝑦) = 1_s ))
9	8	rexbidv 3188	. . . 4 ⊢ (𝑧 = 𝐴 → (∃𝑦 ∈ No (𝑧 ·_s 𝑦) = 1_s ↔ ∃𝑦 ∈ No (𝐴 ·_s 𝑦) = 1_s ))
10	6, 9	imbi12d 346	. . 3 ⊢ (𝑧 = 𝐴 → (( 0_s <s 𝑧 → ∃𝑦 ∈ No (𝑧 ·_s 𝑦) = 1_s ) ↔ ( 0_s <s 𝐴 → ∃𝑦 ∈ No (𝐴 ·_s 𝑦) = 1_s )))
11		eqid 2764	. . . . . . . . 9 ⊢ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩) = rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)
12	11	precsexlemcbv 28301	. . . . . . . 8 ⊢ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩) = rec((𝑝 ∈ V ↦ ⦋(1^st ‘𝑝) / 𝑙⦌⦋(2^nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ ( R ‘𝑧)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝑧) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝑧) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝑧) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ ( R ‘𝑧)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝑧) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)
13		eqid 2764	. . . . . . . 8 ⊢ (1^st ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) = (1^st ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩))
14		eqid 2764	. . . . . . . 8 ⊢ (2^nd ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) = (2^nd ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩))
15		simp1 1150	. . . . . . . 8 ⊢ ((𝑧 ∈ No ∧ 0_s <s 𝑧 ∧ ∀𝑥_𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s )) → 𝑧 ∈ No )
16		simp2 1151	. . . . . . . 8 ⊢ ((𝑧 ∈ No ∧ 0_s <s 𝑧 ∧ ∀𝑥_𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s )) → 0_s <s 𝑧)
17		simp3 1152	. . . . . . . 8 ⊢ ((𝑧 ∈ No ∧ 0_s <s 𝑧 ∧ ∀𝑥_𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s )) → ∀𝑥_𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s ))
18	12, 13, 14, 15, 16, 17	precsexlem10 28311	. . . . . . 7 ⊢ ((𝑧 ∈ No ∧ 0_s <s 𝑧 ∧ ∀𝑥_𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s )) → ∪ ((1^st ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω) <<s ∪ ((2^nd ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω))
19	18	cutscld 27878	. . . . . 6 ⊢ ((𝑧 ∈ No ∧ 0_s <s 𝑧 ∧ ∀𝑥_𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s )) → (∪ ((1^st ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω) \|s ∪ ((2^nd ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω)) ∈ No )
20		eqid 2764	. . . . . . 7 ⊢ (∪ ((1^st ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω) \|s ∪ ((2^nd ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω)) = (∪ ((1^st ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω) \|s ∪ ((2^nd ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω))
21	12, 13, 14, 15, 16, 17, 20	precsexlem11 28312	. . . . . 6 ⊢ ((𝑧 ∈ No ∧ 0_s <s 𝑧 ∧ ∀𝑥_𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s )) → (𝑧 ·_s (∪ ((1^st ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω) \|s ∪ ((2^nd ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω))) = 1_s )
22		oveq2 7406	. . . . . . . 8 ⊢ (𝑦 = (∪ ((1^st ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω) \|s ∪ ((2^nd ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω)) → (𝑧 ·_s 𝑦) = (𝑧 ·_s (∪ ((1^st ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω) \|s ∪ ((2^nd ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω))))
23	22	eqeq1d 2766	. . . . . . 7 ⊢ (𝑦 = (∪ ((1^st ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω) \|s ∪ ((2^nd ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω)) → ((𝑧 ·_s 𝑦) = 1_s ↔ (𝑧 ·_s (∪ ((1^st ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω) \|s ∪ ((2^nd ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω))) = 1_s ))
24	23	rspcev 3583	. . . . . 6 ⊢ (((∪ ((1^st ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω) \|s ∪ ((2^nd ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω)) ∈ No ∧ (𝑧 ·_s (∪ ((1^st ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω) \|s ∪ ((2^nd ∘ rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑢 ∈ ( L ‘𝑧) ∣ 0_s <s 𝑢}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 -_s 𝑧) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ ( R ‘𝑧)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 -_s 𝑧) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)) “ ω))) = 1_s ) → ∃𝑦 ∈ No (𝑧 ·_s 𝑦) = 1_s )
25	19, 21, 24	syl2anc 593	. . . . 5 ⊢ ((𝑧 ∈ No ∧ 0_s <s 𝑧 ∧ ∀𝑥_𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s )) → ∃𝑦 ∈ No (𝑧 ·_s 𝑦) = 1_s )
26	25	3exp 1133	. . . 4 ⊢ (𝑧 ∈ No → ( 0_s <s 𝑧 → (∀𝑥_𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s ) → ∃𝑦 ∈ No (𝑧 ·_s 𝑦) = 1_s )))
27	26	com23 86	. . 3 ⊢ (𝑧 ∈ No → (∀𝑥_𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s ) → ( 0_s <s 𝑧 → ∃𝑦 ∈ No (𝑧 ·_s 𝑦) = 1_s )))
28	5, 10, 27	noinds 28040	. 2 ⊢ (𝐴 ∈ No → ( 0_s <s 𝐴 → ∃𝑦 ∈ No (𝐴 ·_s 𝑦) = 1_s ))
29	28	imp 410	1 ⊢ ((𝐴 ∈ No ∧ 0_s <s 𝐴) → ∃𝑦 ∈ No (𝐴 ·_s 𝑦) = 1_s )

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1099 = wceq 1562 ∈ wcel 2144 {cab 2742 ∀wral 3078 ∃wrex 3088 {crab 3416 Vcvv 3456 ⦋csb 3854 ∪ cun 3904 ∅c0 4287 {csn 4584 ⟨cop 4590 ∪ cuni 4867 class class class wbr 5102 ↦ cmpt 5183 “ cima 5652 ∘ ccom 5653 ‘cfv 6523 (class class class)co 7398 ωcom 7848 1^st c1st 7970 2^nd c2nd 7971 reccrdg 8382 No csur 27706 <s clts 27707 |s ccuts 27854 0_s c0s 27900 1_s c1s 27901 L cleft 27920 R cright 27921 +_s cadds 28054 -_s csubs 28115 ·_s cmuls 28201 /_su cdivs 28282

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1817 ax-4 1831 ax-5 1932 ax-6 1989 ax-7 2030 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2214 ax-ext 2736 ax-rep 5229 ax-sep 5248 ax-nul 5258 ax-pow 5324 ax-pr 5392 ax-un 7720 ax-dc 10405

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1100 df-3an 1101 df-tru 1565 df-fal 1575 df-ex 1802 df-nf 1806 df-sb 2093 df-mo 2568 df-eu 2598 df-clab 2743 df-cleq 2756 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3079 df-rex 3089 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3458 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-ot 4593 df-uni 4868 df-int 4908 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5544 df-eprel 5549 df-po 5557 df-so 5558 df-fr 5602 df-se 5603 df-we 5604 df-xp 5655 df-rel 5656 df-cnv 5657 df-co 5658 df-dm 5659 df-rn 5660 df-res 5661 df-ima 5662 df-pred 6290 df-ord 6351 df-on 6352 df-lim 6353 df-suc 6354 df-iota 6479 df-fun 6525 df-fn 6526 df-f 6527 df-f1 6528 df-fo 6529 df-f1o 6530 df-fv 6531 df-riota 7355 df-ov 7401 df-oprab 7402 df-mpo 7403 df-om 7849 df-1st 7972 df-2nd 7973 df-frecs 8264 df-wrecs 8295 df-recs 8344 df-rdg 8383 df-1o 8439 df-2o 8440 df-oadd 8443 df-nadd 8638 df-no 27709 df-lts 27710 df-bday 27711 df-les 27811 df-slts 27853 df-cuts 27855 df-0s 27902 df-1s 27903 df-made 27922 df-old 27923 df-left 27925 df-right 27926 df-norec 28033 df-norec2 28044 df-adds 28055 df-negs 28116 df-subs 28117 df-muls 28202 df-divs 28283

This theorem is referenced by: recsex 28314

W3C validator