precsex

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

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

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑧 = 𝑥_𝑂 → ( 0_s <s 𝑧 ↔ 0_s <s 𝑥_𝑂 ) )
2		oveq1	⊢ ( 𝑧 = 𝑥_𝑂 → ( 𝑧 ·_s 𝑦 ) = ( 𝑥_𝑂 ·_s 𝑦 ) )
3	2	eqeq1d	⊢ ( 𝑧 = 𝑥_𝑂 → ( ( 𝑧 ·_s 𝑦 ) = 1_s ↔ ( 𝑥_𝑂 ·_s 𝑦 ) = 1_s ) )
4	3	rexbidv	⊢ ( 𝑧 = 𝑥_𝑂 → ( ∃ 𝑦 ∈ No ( 𝑧 ·_s 𝑦 ) = 1_s ↔ ∃ 𝑦 ∈ No ( 𝑥_𝑂 ·_s 𝑦 ) = 1_s ) )
5	1 4	imbi12d	⊢ ( 𝑧 = 𝑥_𝑂 → ( ( 0_s <s 𝑧 → ∃ 𝑦 ∈ No ( 𝑧 ·_s 𝑦 ) = 1_s ) ↔ ( 0_s <s 𝑥_𝑂 → ∃ 𝑦 ∈ No ( 𝑥_𝑂 ·_s 𝑦 ) = 1_s ) ) )
6		breq2	⊢ ( 𝑧 = 𝐴 → ( 0_s <s 𝑧 ↔ 0_s <s 𝐴 ) )
7		oveq1	⊢ ( 𝑧 = 𝐴 → ( 𝑧 ·_s 𝑦 ) = ( 𝐴 ·_s 𝑦 ) )
8	7	eqeq1d	⊢ ( 𝑧 = 𝐴 → ( ( 𝑧 ·_s 𝑦 ) = 1_s ↔ ( 𝐴 ·_s 𝑦 ) = 1_s ) )
9	8	rexbidv	⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑦 ∈ No ( 𝑧 ·_s 𝑦 ) = 1_s ↔ ∃ 𝑦 ∈ No ( 𝐴 ·_s 𝑦 ) = 1_s ) )
10	6 9	imbi12d	⊢ ( 𝑧 = 𝐴 → ( ( 0_s <s 𝑧 → ∃ 𝑦 ∈ No ( 𝑧 ·_s 𝑦 ) = 1_s ) ↔ ( 0_s <s 𝐴 → ∃ 𝑦 ∈ No ( 𝐴 ·_s 𝑦 ) = 1_s ) ) )
11		eqid	⊢ 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	⊢ 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	⊢ ( 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	⊢ ( 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	⊢ ( ( 𝑧 ∈ No ∧ 0_s <s 𝑧 ∧ ∀ 𝑥_𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 0_s <s 𝑥_𝑂 → ∃ 𝑦 ∈ No ( 𝑥_𝑂 ·_s 𝑦 ) = 1_s ) ) → 𝑧 ∈ No )
16		simp2	⊢ ( ( 𝑧 ∈ No ∧ 0_s <s 𝑧 ∧ ∀ 𝑥_𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 0_s <s 𝑥_𝑂 → ∃ 𝑦 ∈ No ( 𝑥_𝑂 ·_s 𝑦 ) = 1_s ) ) → 0_s <s 𝑧 )
17		simp3	⊢ ( ( 𝑧 ∈ 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	⊢ ( ( 𝑧 ∈ 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	scutcld	⊢ ( ( 𝑧 ∈ 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	⊢ ( ∪ ( ( 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	⊢ ( ( 𝑧 ∈ 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	⊢ ( 𝑦 = ( ∪ ( ( 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	⊢ ( 𝑦 = ( ∪ ( ( 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	⊢ ( ( ( ∪ ( ( 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	⊢ ( ( 𝑧 ∈ No ∧ 0_s <s 𝑧 ∧ ∀ 𝑥_𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 0_s <s 𝑥_𝑂 → ∃ 𝑦 ∈ No ( 𝑥_𝑂 ·_s 𝑦 ) = 1_s ) ) → ∃ 𝑦 ∈ No ( 𝑧 ·_s 𝑦 ) = 1_s )
26	25	3exp	⊢ ( 𝑧 ∈ No → ( 0_s <s 𝑧 → ( ∀ 𝑥_𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 0_s <s 𝑥_𝑂 → ∃ 𝑦 ∈ No ( 𝑥_𝑂 ·_s 𝑦 ) = 1_s ) → ∃ 𝑦 ∈ No ( 𝑧 ·_s 𝑦 ) = 1_s ) ) )
27	26	com23	⊢ ( 𝑧 ∈ No → ( ∀ 𝑥_𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 0_s <s 𝑥_𝑂 → ∃ 𝑦 ∈ No ( 𝑥_𝑂 ·_s 𝑦 ) = 1_s ) → ( 0_s <s 𝑧 → ∃ 𝑦 ∈ No ( 𝑧 ·_s 𝑦 ) = 1_s ) ) )
28	5 10 27	noinds	⊢ ( 𝐴 ∈ No → ( 0_s <s 𝐴 → ∃ 𝑦 ∈ No ( 𝐴 ·_s 𝑦 ) = 1_s ) )
29	28	imp	⊢ ( ( 𝐴 ∈ No ∧ 0_s <s 𝐴 ) → ∃ 𝑦 ∈ No ( 𝐴 ·_s 𝑦 ) = 1_s )

Metamath Proof Explorer

Theorem precsex

Proof