Theorem 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 ∧ 0s <s 𝐴 ) → ∃ 𝑦 ∈ No ( 𝐴 ·s 𝑦 ) = 1s )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑧 = 𝑥𝑂 → ( 0s <s 𝑧 ↔ 0s <s 𝑥𝑂 ) )
2		oveq1	⊢ ( 𝑧 = 𝑥𝑂 → ( 𝑧 ·s 𝑦 ) = ( 𝑥𝑂 ·s 𝑦 ) )
3	2	eqeq1d	⊢ ( 𝑧 = 𝑥𝑂 → ( ( 𝑧 ·s 𝑦 ) = 1s ↔ ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
4	3	rexbidv	⊢ ( 𝑧 = 𝑥𝑂 → ( ∃ 𝑦 ∈ No ( 𝑧 ·s 𝑦 ) = 1s ↔ ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
5	1 4	imbi12d	⊢ ( 𝑧 = 𝑥𝑂 → ( ( 0s <s 𝑧 → ∃ 𝑦 ∈ No ( 𝑧 ·s 𝑦 ) = 1s ) ↔ ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) ) )
6		breq2	⊢ ( 𝑧 = 𝐴 → ( 0s <s 𝑧 ↔ 0s <s 𝐴 ) )
7		oveq1	⊢ ( 𝑧 = 𝐴 → ( 𝑧 ·s 𝑦 ) = ( 𝐴 ·s 𝑦 ) )
8	7	eqeq1d	⊢ ( 𝑧 = 𝐴 → ( ( 𝑧 ·s 𝑦 ) = 1s ↔ ( 𝐴 ·s 𝑦 ) = 1s ) )
9	8	rexbidv	⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑦 ∈ No ( 𝑧 ·s 𝑦 ) = 1s ↔ ∃ 𝑦 ∈ No ( 𝐴 ·s 𝑦 ) = 1s ) )
10	6 9	imbi12d	⊢ ( 𝑧 = 𝐴 → ( ( 0s <s 𝑧 → ∃ 𝑦 ∈ No ( 𝑧 ·s 𝑦 ) = 1s ) ↔ ( 0s <s 𝐴 → ∃ 𝑦 ∈ No ( 𝐴 ·s 𝑦 ) = 1s ) ) )
11		eqid	⊢ 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 } , ∅ ⟩ ) = 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 } , ∅ ⟩ )
12	11	precsexlemcbv	⊢ 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 } , ∅ ⟩ ) = 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 } , ∅ ⟩ )
13		eqid	⊢ ( 1st ∘ 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 } , ∅ ⟩ ) ) = ( 1st ∘ 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 } , ∅ ⟩ ) )
14		eqid	⊢ ( 2nd ∘ 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 } , ∅ ⟩ ) ) = ( 2nd ∘ 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 } , ∅ ⟩ ) )
15		simp1	⊢ ( ( 𝑧 ∈ No ∧ 0s <s 𝑧 ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) ) → 𝑧 ∈ No )
16		simp2	⊢ ( ( 𝑧 ∈ No ∧ 0s <s 𝑧 ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) ) → 0s <s 𝑧 )
17		simp3	⊢ ( ( 𝑧 ∈ No ∧ 0s <s 𝑧 ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
18	12 13 14 15 16 17	precsexlem10	⊢ ( ( 𝑧 ∈ No ∧ 0s <s 𝑧 ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) ) → ∪ ( ( 1st ∘ 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 } , ∅ ⟩ ) ) “ ω ) <<s ∪ ( ( 2nd ∘ 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 } , ∅ ⟩ ) ) “ ω ) )
19	18	scutcld	⊢ ( ( 𝑧 ∈ No ∧ 0s <s 𝑧 ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) ) → ( ∪ ( ( 1st ∘ 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 } , ∅ ⟩ ) ) “ ω ) |s ∪ ( ( 2nd ∘ 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 } , ∅ ⟩ ) ) “ ω ) ) ∈ No )
20		eqid	⊢ ( ∪ ( ( 1st ∘ 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 } , ∅ ⟩ ) ) “ ω ) |s ∪ ( ( 2nd ∘ 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 } , ∅ ⟩ ) ) “ ω ) ) = ( ∪ ( ( 1st ∘ 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 } , ∅ ⟩ ) ) “ ω ) |s ∪ ( ( 2nd ∘ 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 } , ∅ ⟩ ) ) “ ω ) )
21	12 13 14 15 16 17 20	precsexlem11	⊢ ( ( 𝑧 ∈ No ∧ 0s <s 𝑧 ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) ) → ( 𝑧 ·s ( ∪ ( ( 1st ∘ 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 } , ∅ ⟩ ) ) “ ω ) |s ∪ ( ( 2nd ∘ 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 } , ∅ ⟩ ) ) “ ω ) ) ) = 1s )
22		oveq2	⊢ ( 𝑦 = ( ∪ ( ( 1st ∘ 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 } , ∅ ⟩ ) ) “ ω ) |s ∪ ( ( 2nd ∘ 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 } , ∅ ⟩ ) ) “ ω ) ) → ( 𝑧 ·s 𝑦 ) = ( 𝑧 ·s ( ∪ ( ( 1st ∘ 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 } , ∅ ⟩ ) ) “ ω ) |s ∪ ( ( 2nd ∘ 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 } , ∅ ⟩ ) ) “ ω ) ) ) )
23	22	eqeq1d	⊢ ( 𝑦 = ( ∪ ( ( 1st ∘ 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 } , ∅ ⟩ ) ) “ ω ) |s ∪ ( ( 2nd ∘ 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 } , ∅ ⟩ ) ) “ ω ) ) → ( ( 𝑧 ·s 𝑦 ) = 1s ↔ ( 𝑧 ·s ( ∪ ( ( 1st ∘ 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 } , ∅ ⟩ ) ) “ ω ) |s ∪ ( ( 2nd ∘ 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 } , ∅ ⟩ ) ) “ ω ) ) ) = 1s ) )
24	23	rspcev	⊢ ( ( ( ∪ ( ( 1st ∘ 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 } , ∅ ⟩ ) ) “ ω ) |s ∪ ( ( 2nd ∘ 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 } , ∅ ⟩ ) ) “ ω ) ) ∈ No ∧ ( 𝑧 ·s ( ∪ ( ( 1st ∘ 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 } , ∅ ⟩ ) ) “ ω ) |s ∪ ( ( 2nd ∘ 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 } , ∅ ⟩ ) ) “ ω ) ) ) = 1s ) → ∃ 𝑦 ∈ No ( 𝑧 ·s 𝑦 ) = 1s )
25	19 21 24	syl2anc	⊢ ( ( 𝑧 ∈ No ∧ 0s <s 𝑧 ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) ) → ∃ 𝑦 ∈ No ( 𝑧 ·s 𝑦 ) = 1s )
26	25	3exp	⊢ ( 𝑧 ∈ No → ( 0s <s 𝑧 → ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) → ∃ 𝑦 ∈ No ( 𝑧 ·s 𝑦 ) = 1s ) ) )
27	26	com23	⊢ ( 𝑧 ∈ No → ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) → ( 0s <s 𝑧 → ∃ 𝑦 ∈ No ( 𝑧 ·s 𝑦 ) = 1s ) ) )
28	5 10 27	noinds	⊢ ( 𝐴 ∈ No → ( 0s <s 𝐴 → ∃ 𝑦 ∈ No ( 𝐴 ·s 𝑦 ) = 1s ) )
29	28	imp	⊢ ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) → ∃ 𝑦 ∈ No ( 𝐴 ·s 𝑦 ) = 1s )