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	$$⊢\left(A\in \mathrm{No}\wedge 0_s{<}_{s}A\right)\to \exists y\in \mathrm{No}A{\cdot }_{s}y=1_s$$

Proof

Step	Hyp	Ref	Expression
1		breq2	Could not format ( z = xO -> ( 0s 0s ( 0s 0s
2		oveq1	Could not format ( z = xO -> ( z x.s y ) = ( xO x.s y ) ) : No typesetting found for |- ( z = xO -> ( z x.s y ) = ( xO x.s y ) ) with typecode |-
3	2	eqeq1d	Could not format ( z = xO -> ( ( z x.s y ) = 1s <-> ( xO x.s y ) = 1s ) ) : No typesetting found for |- ( z = xO -> ( ( z x.s y ) = 1s <-> ( xO x.s y ) = 1s ) ) with typecode |-
4	3	rexbidv	Could not format ( z = xO -> ( E. y e. No ( z x.s y ) = 1s <-> E. y e. No ( xO x.s y ) = 1s ) ) : No typesetting found for |- ( z = xO -> ( E. y e. No ( z x.s y ) = 1s <-> E. y e. No ( xO x.s y ) = 1s ) ) with typecode |-
5	1 4	imbi12d	Could not format ( z = xO -> ( ( 0s E. y e. No ( z x.s y ) = 1s ) <-> ( 0s E. y e. No ( xO x.s y ) = 1s ) ) ) : No typesetting found for |- ( z = xO -> ( ( 0s E. y e. No ( z x.s y ) = 1s ) <-> ( 0s E. y e. No ( xO x.s y ) = 1s ) ) ) with typecode |-
6		breq2	$$⊢z=A\to \left(0_s{<}_{s}z\leftrightarrow 0_s{<}_{s}A\right)$$
7		oveq1	$$⊢z=A\to z{\cdot }_{s}y=A{\cdot }_{s}y$$
8	7	eqeq1d	$$⊢z=A\to \left(z{\cdot }_{s}y=1_s\leftrightarrow A{\cdot }_{s}y=1_s\right)$$
9	8	rexbidv	$$⊢z=A\to \left(\exists y\in \mathrm{No}z{\cdot }_{s}y=1_s\leftrightarrow \exists y\in \mathrm{No}A{\cdot }_{s}y=1_s\right)$$
10	6 9	imbi12d	$$⊢z=A\to \left(\left(0_s{<}_{s}z\to \exists y\in \mathrm{No}z{\cdot }_{s}y=1_s\right)\leftrightarrow \left(0_s{<}_{s}A\to \exists y\in \mathrm{No}A{\cdot }_{s}y=1_s\right)\right)$$
11		eqid	Could not format rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) = rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) : No typesetting found for |- rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) = rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) with typecode |-
12	11	precsexlemcbv	Could not format rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` z ) E. yL e. l a = ( ( 1s +s ( ( xR -s z ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) : No typesetting found for |- rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` z ) E. yL e. l a = ( ( 1s +s ( ( xR -s z ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) with typecode |-
13		eqid	Could not format ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) = ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) : No typesetting found for |- ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) = ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) with typecode |-
14		eqid	Could not format ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) = ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) : No typesetting found for |- ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) = ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) with typecode |-
15		simp1	Could not format ( ( z e. No /\ 0s E. y e. No ( xO x.s y ) = 1s ) ) -> z e. No ) : No typesetting found for |- ( ( z e. No /\ 0s E. y e. No ( xO x.s y ) = 1s ) ) -> z e. No ) with typecode |-
16		simp2	Could not format ( ( z e. No /\ 0s E. y e. No ( xO x.s y ) = 1s ) ) -> 0s E. y e. No ( xO x.s y ) = 1s ) ) -> 0s
17		simp3	Could not format ( ( z e. No /\ 0s E. y e. No ( xO x.s y ) = 1s ) ) -> A. xO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) : No typesetting found for |- ( ( z e. No /\ 0s E. y e. No ( xO x.s y ) = 1s ) ) -> A. xO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) with typecode |-
18	12 13 14 15 16 17	precsexlem10	Could not format ( ( z e. No /\ 0s E. y e. No ( xO x.s y ) = 1s ) ) -> U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) < [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) : No typesetting found for |- ( ( z e. No /\ 0s E. y e. No ( xO x.s y ) = 1s ) ) -> U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) < [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) with typecode |-
19	18	scutcld	Could not format ( ( z e. No /\ 0s E. y e. No ( xO x.s y ) = 1s ) ) -> ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) e. No ) : No typesetting found for |- ( ( z e. No /\ 0s E. y e. No ( xO x.s y ) = 1s ) ) -> ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) e. No ) with typecode |-
20		eqid	Could not format ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) = ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) : No typesetting found for |- ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) = ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) with typecode |-
21	12 13 14 15 16 17 20	precsexlem11	Could not format ( ( z e. No /\ 0s E. y e. No ( xO x.s y ) = 1s ) ) -> ( z x.s ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) ) = 1s ) : No typesetting found for |- ( ( z e. No /\ 0s E. y e. No ( xO x.s y ) = 1s ) ) -> ( z x.s ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) ) = 1s ) with typecode |-
22		oveq2	Could not format ( y = ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) -> ( z x.s y ) = ( z x.s ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) ) ) : No typesetting found for |- ( y = ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) -> ( z x.s y ) = ( z x.s ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) ) ) with typecode |-
23	22	eqeq1d	Could not format ( y = ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) -> ( ( z x.s y ) = 1s <-> ( z x.s ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) ) = 1s ) ) : No typesetting found for |- ( y = ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) -> ( ( z x.s y ) = 1s <-> ( z x.s ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) ) = 1s ) ) with typecode |-
24	23	rspcev	Could not format ( ( ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) e. No /\ ( z x.s ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) ) = 1s ) -> E. y e. No ( z x.s y ) = 1s ) : No typesetting found for |- ( ( ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) e. No /\ ( z x.s ( U. ( ( 1st o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) |s U. ( ( 2nd o. rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` z ) E. w e. m b = ( ( 1s +s ( ( zR -s z ) x.s w ) ) /su zR ) } u. { b | E. zL e. { u e. ( _Left ` z ) | 0s . ) , <. { 0s } , (/) >. ) ) " _om ) ) ) = 1s ) -> E. y e. No ( z x.s y ) = 1s ) with typecode |-
25	19 21 24	syl2anc	Could not format ( ( z e. No /\ 0s E. y e. No ( xO x.s y ) = 1s ) ) -> E. y e. No ( z x.s y ) = 1s ) : No typesetting found for |- ( ( z e. No /\ 0s E. y e. No ( xO x.s y ) = 1s ) ) -> E. y e. No ( z x.s y ) = 1s ) with typecode |-
26	25	3exp	Could not format ( z e. No -> ( 0s ( A. xO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) -> E. y e. No ( z x.s y ) = 1s ) ) ) : No typesetting found for |- ( z e. No -> ( 0s ( A. xO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) -> E. y e. No ( z x.s y ) = 1s ) ) ) with typecode |-
27	26	com23	Could not format ( z e. No -> ( A. xO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) -> ( 0s E. y e. No ( z x.s y ) = 1s ) ) ) : No typesetting found for |- ( z e. No -> ( A. xO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) -> ( 0s E. y e. No ( z x.s y ) = 1s ) ) ) with typecode |-
28	5 10 27	noinds	$$⊢A\in \mathrm{No}\to \left(0_s{<}_{s}A\to \exists y\in \mathrm{No}A{\cdot }_{s}y=1_s\right)$$
29	28	imp	$$⊢\left(A\in \mathrm{No}\wedge 0_s{<}_{s}A\right)\to \exists y\in \mathrm{No}A{\cdot }_{s}y=1_s$$