Metamath Proof Explorer

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 Could not format assertion : No typesetting found for |- ( ( A e. No /\ 0s E. y e. No ( A x.s y ) = 1s ) with typecode |-

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 Could not format ( z = A -> ( 0s 0s ( 0s 0s
7 oveq1 Could not format ( z = A -> ( z x.s y ) = ( A x.s y ) ) : No typesetting found for |- ( z = A -> ( z x.s y ) = ( A x.s y ) ) with typecode |-
8 7 eqeq1d Could not format ( z = A -> ( ( z x.s y ) = 1s <-> ( A x.s y ) = 1s ) ) : No typesetting found for |- ( z = A -> ( ( z x.s y ) = 1s <-> ( A x.s y ) = 1s ) ) with typecode |-
9 8 rexbidv Could not format ( z = A -> ( E. y e. No ( z x.s y ) = 1s <-> E. y e. No ( A x.s y ) = 1s ) ) : No typesetting found for |- ( z = A -> ( E. y e. No ( z x.s y ) = 1s <-> E. y e. No ( A x.s y ) = 1s ) ) with typecode |-
10 6 9 imbi12d Could not format ( z = A -> ( ( 0s E. y e. No ( z x.s y ) = 1s ) <-> ( 0s E. y e. No ( A x.s y ) = 1s ) ) ) : No typesetting found for |- ( z = A -> ( ( 0s E. y e. No ( z x.s y ) = 1s ) <-> ( 0s E. y e. No ( A x.s y ) = 1s ) ) ) with typecode |-
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 Could not format ( A e. No -> ( 0s E. y e. No ( A x.s y ) = 1s ) ) : No typesetting found for |- ( A e. No -> ( 0s E. y e. No ( A x.s y ) = 1s ) ) with typecode |-
29 28 imp Could not format ( ( A e. No /\ 0s E. y e. No ( A x.s y ) = 1s ) : No typesetting found for |- ( ( A e. No /\ 0s E. y e. No ( A x.s y ) = 1s ) with typecode |-