Metamath Proof Explorer

Theorem nohalf

Description: An explicit expression for one half. This theorem avoids the axiom of infinity. (Contributed by Scott Fenton, 23-Jul-2025)

Ref Expression
Assertion nohalf 
|- ( 1s /su 2s ) = ( { 0s } |s { 1s } )

Proof

Step Hyp Ref Expression
1 snex 
 |-  { 0s } e. _V
2 1 a1i 
 |-  ( T. -> { 0s } e. _V )
3 snex 
 |-  { 1s } e. _V
4 3 a1i 
 |-  ( T. -> { 1s } e. _V )
5 0sno 
 |-  0s e. No
6 5 a1i 
 |-  ( T. -> 0s e. No )
7 6 snssd 
 |-  ( T. -> { 0s } C_ No )
8 1sno 
 |-  1s e. No
9 snssi 
 |-  ( 1s e. No -> { 1s } C_ No )
10 8 9 mp1i 
 |-  ( T. -> { 1s } C_ No )
11 velsn 
 |-  ( x e. { 0s } <-> x = 0s )
12 velsn 
 |-  ( y e. { 1s } <-> y = 1s )
13 0slt1s 
 |-  0s
14 breq12 
 |-  ( ( x = 0s /\ y = 1s ) -> ( x  0s
15 13 14 mpbiri 
 |-  ( ( x = 0s /\ y = 1s ) -> x
16 11 12 15 syl2anb 
 |-  ( ( x e. { 0s } /\ y e. { 1s } ) -> x
17 16 3adant1 
 |-  ( ( T. /\ x e. { 0s } /\ y e. { 1s } ) -> x
18 2 4 7 10 17 ssltd 
 |-  ( T. -> { 0s } <
19 18 scutcld 
 |-  ( T. -> ( { 0s } |s { 1s } ) e. No )
20 19 mptru 
 |-  ( { 0s } |s { 1s } ) e. No
21 no2times 
 |-  ( ( { 0s } |s { 1s } ) e. No -> ( 2s x.s ( { 0s } |s { 1s } ) ) = ( ( { 0s } |s { 1s } ) +s ( { 0s } |s { 1s } ) ) )
22 20 21 ax-mp 
 |-  ( 2s x.s ( { 0s } |s { 1s } ) ) = ( ( { 0s } |s { 1s } ) +s ( { 0s } |s { 1s } ) )
23 eqidd 
 |-  ( T. -> ( { 0s } |s { 1s } ) = ( { 0s } |s { 1s } ) )
24 18 18 23 23 addsunif 
 |-  ( T. -> ( ( { 0s } |s { 1s } ) +s ( { 0s } |s { 1s } ) ) = ( ( { x | E. y e. { 0s } x = ( y +s ( { 0s } |s { 1s } ) ) } u. { x | E. y e. { 0s } x = ( ( { 0s } |s { 1s } ) +s y ) } ) |s ( { x | E. y e. { 1s } x = ( y +s ( { 0s } |s { 1s } ) ) } u. { x | E. y e. { 1s } x = ( ( { 0s } |s { 1s } ) +s y ) } ) ) )
25 24 mptru 
 |-  ( ( { 0s } |s { 1s } ) +s ( { 0s } |s { 1s } ) ) = ( ( { x | E. y e. { 0s } x = ( y +s ( { 0s } |s { 1s } ) ) } u. { x | E. y e. { 0s } x = ( ( { 0s } |s { 1s } ) +s y ) } ) |s ( { x | E. y e. { 1s } x = ( y +s ( { 0s } |s { 1s } ) ) } u. { x | E. y e. { 1s } x = ( ( { 0s } |s { 1s } ) +s y ) } ) )
26 5 elexi 
 |-  0s e. _V
27 oveq1 
 |-  ( y = 0s -> ( y +s ( { 0s } |s { 1s } ) ) = ( 0s +s ( { 0s } |s { 1s } ) ) )
28 addslid 
 |-  ( ( { 0s } |s { 1s } ) e. No -> ( 0s +s ( { 0s } |s { 1s } ) ) = ( { 0s } |s { 1s } ) )
29 20 28 ax-mp 
 |-  ( 0s +s ( { 0s } |s { 1s } ) ) = ( { 0s } |s { 1s } )
30 27 29 eqtrdi 
 |-  ( y = 0s -> ( y +s ( { 0s } |s { 1s } ) ) = ( { 0s } |s { 1s } ) )
31 30 eqeq2d 
 |-  ( y = 0s -> ( x = ( y +s ( { 0s } |s { 1s } ) ) <-> x = ( { 0s } |s { 1s } ) ) )
32 26 31 rexsn 
 |-  ( E. y e. { 0s } x = ( y +s ( { 0s } |s { 1s } ) ) <-> x = ( { 0s } |s { 1s } ) )
33 32 abbii 
 |-  { x | E. y e. { 0s } x = ( y +s ( { 0s } |s { 1s } ) ) } = { x | x = ( { 0s } |s { 1s } ) }
34 df-sn 
 |-  { ( { 0s } |s { 1s } ) } = { x | x = ( { 0s } |s { 1s } ) }
35 33 34 eqtr4i 
 |-  { x | E. y e. { 0s } x = ( y +s ( { 0s } |s { 1s } ) ) } = { ( { 0s } |s { 1s } ) }
36 oveq2 
 |-  ( y = 0s -> ( ( { 0s } |s { 1s } ) +s y ) = ( ( { 0s } |s { 1s } ) +s 0s ) )
37 addsrid 
 |-  ( ( { 0s } |s { 1s } ) e. No -> ( ( { 0s } |s { 1s } ) +s 0s ) = ( { 0s } |s { 1s } ) )
38 20 37 ax-mp 
 |-  ( ( { 0s } |s { 1s } ) +s 0s ) = ( { 0s } |s { 1s } )
39 36 38 eqtrdi 
 |-  ( y = 0s -> ( ( { 0s } |s { 1s } ) +s y ) = ( { 0s } |s { 1s } ) )
40 39 eqeq2d 
 |-  ( y = 0s -> ( x = ( ( { 0s } |s { 1s } ) +s y ) <-> x = ( { 0s } |s { 1s } ) ) )
41 26 40 rexsn 
 |-  ( E. y e. { 0s } x = ( ( { 0s } |s { 1s } ) +s y ) <-> x = ( { 0s } |s { 1s } ) )
42 41 abbii 
 |-  { x | E. y e. { 0s } x = ( ( { 0s } |s { 1s } ) +s y ) } = { x | x = ( { 0s } |s { 1s } ) }
43 42 34 eqtr4i 
 |-  { x | E. y e. { 0s } x = ( ( { 0s } |s { 1s } ) +s y ) } = { ( { 0s } |s { 1s } ) }
44 35 43 uneq12i 
 |-  ( { x | E. y e. { 0s } x = ( y +s ( { 0s } |s { 1s } ) ) } u. { x | E. y e. { 0s } x = ( ( { 0s } |s { 1s } ) +s y ) } ) = ( { ( { 0s } |s { 1s } ) } u. { ( { 0s } |s { 1s } ) } )
45 unidm 
 |-  ( { ( { 0s } |s { 1s } ) } u. { ( { 0s } |s { 1s } ) } ) = { ( { 0s } |s { 1s } ) }
46 44 45 eqtri 
 |-  ( { x | E. y e. { 0s } x = ( y +s ( { 0s } |s { 1s } ) ) } u. { x | E. y e. { 0s } x = ( ( { 0s } |s { 1s } ) +s y ) } ) = { ( { 0s } |s { 1s } ) }
47 8 elexi 
 |-  1s e. _V
48 oveq1 
 |-  ( y = 1s -> ( y +s ( { 0s } |s { 1s } ) ) = ( 1s +s ( { 0s } |s { 1s } ) ) )
49 addscom 
 |-  ( ( 1s e. No /\ ( { 0s } |s { 1s } ) e. No ) -> ( 1s +s ( { 0s } |s { 1s } ) ) = ( ( { 0s } |s { 1s } ) +s 1s ) )
50 8 20 49 mp2an 
 |-  ( 1s +s ( { 0s } |s { 1s } ) ) = ( ( { 0s } |s { 1s } ) +s 1s )
51 48 50 eqtrdi 
 |-  ( y = 1s -> ( y +s ( { 0s } |s { 1s } ) ) = ( ( { 0s } |s { 1s } ) +s 1s ) )
52 51 eqeq2d 
 |-  ( y = 1s -> ( x = ( y +s ( { 0s } |s { 1s } ) ) <-> x = ( ( { 0s } |s { 1s } ) +s 1s ) ) )
53 47 52 rexsn 
 |-  ( E. y e. { 1s } x = ( y +s ( { 0s } |s { 1s } ) ) <-> x = ( ( { 0s } |s { 1s } ) +s 1s ) )
54 53 abbii 
 |-  { x | E. y e. { 1s } x = ( y +s ( { 0s } |s { 1s } ) ) } = { x | x = ( ( { 0s } |s { 1s } ) +s 1s ) }
55 df-sn 
 |-  { ( ( { 0s } |s { 1s } ) +s 1s ) } = { x | x = ( ( { 0s } |s { 1s } ) +s 1s ) }
56 54 55 eqtr4i 
 |-  { x | E. y e. { 1s } x = ( y +s ( { 0s } |s { 1s } ) ) } = { ( ( { 0s } |s { 1s } ) +s 1s ) }
57 oveq2 
 |-  ( y = 1s -> ( ( { 0s } |s { 1s } ) +s y ) = ( ( { 0s } |s { 1s } ) +s 1s ) )
58 57 eqeq2d 
 |-  ( y = 1s -> ( x = ( ( { 0s } |s { 1s } ) +s y ) <-> x = ( ( { 0s } |s { 1s } ) +s 1s ) ) )
59 47 58 rexsn 
 |-  ( E. y e. { 1s } x = ( ( { 0s } |s { 1s } ) +s y ) <-> x = ( ( { 0s } |s { 1s } ) +s 1s ) )
60 59 abbii 
 |-  { x | E. y e. { 1s } x = ( ( { 0s } |s { 1s } ) +s y ) } = { x | x = ( ( { 0s } |s { 1s } ) +s 1s ) }
61 60 55 eqtr4i 
 |-  { x | E. y e. { 1s } x = ( ( { 0s } |s { 1s } ) +s y ) } = { ( ( { 0s } |s { 1s } ) +s 1s ) }
62 56 61 uneq12i 
 |-  ( { x | E. y e. { 1s } x = ( y +s ( { 0s } |s { 1s } ) ) } u. { x | E. y e. { 1s } x = ( ( { 0s } |s { 1s } ) +s y ) } ) = ( { ( ( { 0s } |s { 1s } ) +s 1s ) } u. { ( ( { 0s } |s { 1s } ) +s 1s ) } )
63 unidm 
 |-  ( { ( ( { 0s } |s { 1s } ) +s 1s ) } u. { ( ( { 0s } |s { 1s } ) +s 1s ) } ) = { ( ( { 0s } |s { 1s } ) +s 1s ) }
64 62 63 eqtri 
 |-  ( { x | E. y e. { 1s } x = ( y +s ( { 0s } |s { 1s } ) ) } u. { x | E. y e. { 1s } x = ( ( { 0s } |s { 1s } ) +s y ) } ) = { ( ( { 0s } |s { 1s } ) +s 1s ) }
65 46 64 oveq12i 
 |-  ( ( { x | E. y e. { 0s } x = ( y +s ( { 0s } |s { 1s } ) ) } u. { x | E. y e. { 0s } x = ( ( { 0s } |s { 1s } ) +s y ) } ) |s ( { x | E. y e. { 1s } x = ( y +s ( { 0s } |s { 1s } ) ) } u. { x | E. y e. { 1s } x = ( ( { 0s } |s { 1s } ) +s y ) } ) ) = ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } )
66 ral0 
 |-  A. x e. (/) ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } )
67 slerflex 
 |-  ( 1s e. No -> 1s <_s 1s )
68 8 67 ax-mp 
 |-  1s <_s 1s
69 breq1 
 |-  ( y = 1s -> ( y <_s 1s <-> 1s <_s 1s ) )
70 47 69 rexsn 
 |-  ( E. y e. { 1s } y <_s 1s <-> 1s <_s 1s )
71 68 70 mpbir 
 |-  E. y e. { 1s } y <_s 1s
72 71 olci 
 |-  ( E. x e. { 0s } ( { 0s } |s { 1s } ) <_s x \/ E. y e. { 1s } y <_s 1s )
73 18 mptru 
 |-  { 0s } <
74 snelpwi 
 |-  ( 0s e. No -> { 0s } e. ~P No )
75 5 74 ax-mp 
 |-  { 0s } e. ~P No
76 nulssgt 
 |-  ( { 0s } e. ~P No -> { 0s } <
77 75 76 ax-mp 
 |-  { 0s } <
78 eqid 
 |-  ( { 0s } |s { 1s } ) = ( { 0s } |s { 1s } )
79 df-1s 
 |-  1s = ( { 0s } |s (/) )
80 sltrec 
 |-  ( ( ( { 0s } < ( ( { 0s } |s { 1s } )  ( E. x e. { 0s } ( { 0s } |s { 1s } ) <_s x \/ E. y e. { 1s } y <_s 1s ) ) )
81 73 77 78 79 80 mp4an 
 |-  ( ( { 0s } |s { 1s } )  ( E. x e. { 0s } ( { 0s } |s { 1s } ) <_s x \/ E. y e. { 1s } y <_s 1s ) )
82 72 81 mpbir 
 |-  ( { 0s } |s { 1s } )
83 ovex 
 |-  ( { 0s } |s { 1s } ) e. _V
84 breq1 
 |-  ( y = ( { 0s } |s { 1s } ) -> ( y  ( { 0s } |s { 1s } )
85 83 84 ralsn 
 |-  ( A. y e. { ( { 0s } |s { 1s } ) } y  ( { 0s } |s { 1s } )
86 82 85 mpbir 
 |-  A. y e. { ( { 0s } |s { 1s } ) } y
87 snex 
 |-  { ( { 0s } |s { 1s } ) } e. _V
88 87 a1i 
 |-  ( T. -> { ( { 0s } |s { 1s } ) } e. _V )
89 snex 
 |-  { ( ( { 0s } |s { 1s } ) +s 1s ) } e. _V
90 89 a1i 
 |-  ( T. -> { ( ( { 0s } |s { 1s } ) +s 1s ) } e. _V )
91 19 snssd 
 |-  ( T. -> { ( { 0s } |s { 1s } ) } C_ No )
92 8 a1i 
 |-  ( T. -> 1s e. No )
93 19 92 addscld 
 |-  ( T. -> ( ( { 0s } |s { 1s } ) +s 1s ) e. No )
94 93 snssd 
 |-  ( T. -> { ( ( { 0s } |s { 1s } ) +s 1s ) } C_ No )
95 velsn 
 |-  ( x e. { ( { 0s } |s { 1s } ) } <-> x = ( { 0s } |s { 1s } ) )
96 velsn 
 |-  ( y e. { ( ( { 0s } |s { 1s } ) +s 1s ) } <-> y = ( ( { 0s } |s { 1s } ) +s 1s ) )
97 sltadd2 
 |-  ( ( 0s e. No /\ 1s e. No /\ ( { 0s } |s { 1s } ) e. No ) -> ( 0s  ( ( { 0s } |s { 1s } ) +s 0s )
98 5 8 20 97 mp3an 
 |-  ( 0s  ( ( { 0s } |s { 1s } ) +s 0s )
99 13 98 mpbi 
 |-  ( ( { 0s } |s { 1s } ) +s 0s )
100 38 99 eqbrtrri 
 |-  ( { 0s } |s { 1s } )
101 breq12 
 |-  ( ( x = ( { 0s } |s { 1s } ) /\ y = ( ( { 0s } |s { 1s } ) +s 1s ) ) -> ( x  ( { 0s } |s { 1s } )
102 100 101 mpbiri 
 |-  ( ( x = ( { 0s } |s { 1s } ) /\ y = ( ( { 0s } |s { 1s } ) +s 1s ) ) -> x
103 95 96 102 syl2anb 
 |-  ( ( x e. { ( { 0s } |s { 1s } ) } /\ y e. { ( ( { 0s } |s { 1s } ) +s 1s ) } ) -> x
104 103 3adant1 
 |-  ( ( T. /\ x e. { ( { 0s } |s { 1s } ) } /\ y e. { ( ( { 0s } |s { 1s } ) +s 1s ) } ) -> x
105 88 90 91 94 104 ssltd 
 |-  ( T. -> { ( { 0s } |s { 1s } ) } <
106 105 mptru 
 |-  { ( { 0s } |s { 1s } ) } <
107 eqid 
 |-  ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) = ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } )
108 slerec 
 |-  ( ( ( { ( { 0s } |s { 1s } ) } < ( ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) <_s 1s <-> ( A. x e. (/) ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } )
109 106 77 107 79 108 mp4an 
 |-  ( ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) <_s 1s <-> ( A. x e. (/) ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } )
110 66 86 109 mpbir2an 
 |-  ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) <_s 1s
111 addslid 
 |-  ( 1s e. No -> ( 0s +s 1s ) = 1s )
112 8 111 ax-mp 
 |-  ( 0s +s 1s ) = 1s
113 slerflex 
 |-  ( 0s e. No -> 0s <_s 0s )
114 5 113 ax-mp 
 |-  0s <_s 0s
115 breq2 
 |-  ( x = 0s -> ( 0s <_s x <-> 0s <_s 0s ) )
116 26 115 rexsn 
 |-  ( E. x e. { 0s } 0s <_s x <-> 0s <_s 0s )
117 114 116 mpbir 
 |-  E. x e. { 0s } 0s <_s x
118 117 orci 
 |-  ( E. x e. { 0s } 0s <_s x \/ E. y e. (/) y <_s ( { 0s } |s { 1s } ) )
119 0elpw 
 |-  (/) e. ~P No
120 nulssgt 
 |-  ( (/) e. ~P No -> (/) <
121 119 120 ax-mp 
 |-  (/) <
122 df-0s 
 |-  0s = ( (/) |s (/) )
123 sltrec 
 |-  ( ( ( (/) < ( 0s  ( E. x e. { 0s } 0s <_s x \/ E. y e. (/) y <_s ( { 0s } |s { 1s } ) ) ) )
124 121 73 122 78 123 mp4an 
 |-  ( 0s  ( E. x e. { 0s } 0s <_s x \/ E. y e. (/) y <_s ( { 0s } |s { 1s } ) ) )
125 118 124 mpbir 
 |-  0s
126 sltadd1 
 |-  ( ( 0s e. No /\ ( { 0s } |s { 1s } ) e. No /\ 1s e. No ) -> ( 0s  ( 0s +s 1s )
127 5 20 8 126 mp3an 
 |-  ( 0s  ( 0s +s 1s )
128 125 127 mpbi 
 |-  ( 0s +s 1s )
129 112 128 eqbrtrri 
 |-  1s
130 ovex 
 |-  ( ( { 0s } |s { 1s } ) +s 1s ) e. _V
131 breq2 
 |-  ( y = ( ( { 0s } |s { 1s } ) +s 1s ) -> ( 1s  1s
132 130 131 ralsn 
 |-  ( A. y e. { ( ( { 0s } |s { 1s } ) +s 1s ) } 1s  1s
133 129 132 mpbir 
 |-  A. y e. { ( ( { 0s } |s { 1s } ) +s 1s ) } 1s
134 breq2 
 |-  ( x = 1s -> ( 0s  0s
135 47 134 ralsn 
 |-  ( A. x e. { 1s } 0s  0s
136 13 135 mpbir 
 |-  A. x e. { 1s } 0s
137 ral0 
 |-  A. y e. (/) y
138 slerec 
 |-  ( ( ( (/) < ( 0s <_s ( { 0s } |s { 1s } ) <-> ( A. x e. { 1s } 0s
139 121 73 122 78 138 mp4an 
 |-  ( 0s <_s ( { 0s } |s { 1s } ) <-> ( A. x e. { 1s } 0s
140 136 137 139 mpbir2an 
 |-  0s <_s ( { 0s } |s { 1s } )
141 breq2 
 |-  ( x = ( { 0s } |s { 1s } ) -> ( 0s <_s x <-> 0s <_s ( { 0s } |s { 1s } ) ) )
142 83 141 rexsn 
 |-  ( E. x e. { ( { 0s } |s { 1s } ) } 0s <_s x <-> 0s <_s ( { 0s } |s { 1s } ) )
143 140 142 mpbir 
 |-  E. x e. { ( { 0s } |s { 1s } ) } 0s <_s x
144 143 orci 
 |-  ( E. x e. { ( { 0s } |s { 1s } ) } 0s <_s x \/ E. y e. (/) y <_s ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) )
145 sltrec 
 |-  ( ( ( (/) < ( 0s  ( E. x e. { ( { 0s } |s { 1s } ) } 0s <_s x \/ E. y e. (/) y <_s ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) ) ) )
146 121 106 122 107 145 mp4an 
 |-  ( 0s  ( E. x e. { ( { 0s } |s { 1s } ) } 0s <_s x \/ E. y e. (/) y <_s ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) ) )
147 144 146 mpbir 
 |-  0s
148 breq1 
 |-  ( x = 0s -> ( x  0s
149 26 148 ralsn 
 |-  ( A. x e. { 0s } x  0s
150 147 149 mpbir 
 |-  A. x e. { 0s } x
151 slerec 
 |-  ( ( ( { 0s } < ( 1s <_s ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) <-> ( A. y e. { ( ( { 0s } |s { 1s } ) +s 1s ) } 1s
152 77 106 79 107 151 mp4an 
 |-  ( 1s <_s ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) <-> ( A. y e. { ( ( { 0s } |s { 1s } ) +s 1s ) } 1s
153 133 150 152 mpbir2an 
 |-  1s <_s ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } )
154 105 scutcld 
 |-  ( T. -> ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) e. No )
155 154 mptru 
 |-  ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) e. No
156 sletri3 
 |-  ( ( ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) e. No /\ 1s e. No ) -> ( ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) = 1s <-> ( ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) <_s 1s /\ 1s <_s ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) ) ) )
157 155 8 156 mp2an 
 |-  ( ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) = 1s <-> ( ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) <_s 1s /\ 1s <_s ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) ) )
158 110 153 157 mpbir2an 
 |-  ( { ( { 0s } |s { 1s } ) } |s { ( ( { 0s } |s { 1s } ) +s 1s ) } ) = 1s
159 65 158 eqtri 
 |-  ( ( { x | E. y e. { 0s } x = ( y +s ( { 0s } |s { 1s } ) ) } u. { x | E. y e. { 0s } x = ( ( { 0s } |s { 1s } ) +s y ) } ) |s ( { x | E. y e. { 1s } x = ( y +s ( { 0s } |s { 1s } ) ) } u. { x | E. y e. { 1s } x = ( ( { 0s } |s { 1s } ) +s y ) } ) ) = 1s
160 25 159 eqtri 
 |-  ( ( { 0s } |s { 1s } ) +s ( { 0s } |s { 1s } ) ) = 1s
161 22 160 eqtri 
 |-  ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s
162 2sno 
 |-  2s e. No
163 2ne0s 
 |-  2s =/= 0s
164 162 163 pm3.2i 
 |-  ( 2s e. No /\ 2s =/= 0s )
165 8 20 164 3pm3.2i 
 |-  ( 1s e. No /\ ( { 0s } |s { 1s } ) e. No /\ ( 2s e. No /\ 2s =/= 0s ) )
166 oveq2 
 |-  ( x = ( { 0s } |s { 1s } ) -> ( 2s x.s x ) = ( 2s x.s ( { 0s } |s { 1s } ) ) )
167 166 eqeq1d 
 |-  ( x = ( { 0s } |s { 1s } ) -> ( ( 2s x.s x ) = 1s <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) )
168 167 rspcev 
 |-  ( ( ( { 0s } |s { 1s } ) e. No /\ ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) -> E. x e. No ( 2s x.s x ) = 1s )
169 20 161 168 mp2an 
 |-  E. x e. No ( 2s x.s x ) = 1s
170 divsmulw 
 |-  ( ( ( 1s e. No /\ ( { 0s } |s { 1s } ) e. No /\ ( 2s e. No /\ 2s =/= 0s ) ) /\ E. x e. No ( 2s x.s x ) = 1s ) -> ( ( 1s /su 2s ) = ( { 0s } |s { 1s } ) <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) )
171 165 169 170 mp2an 
 |-  ( ( 1s /su 2s ) = ( { 0s } |s { 1s } ) <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s )
172 161 171 mpbir 
 |-  ( 1s /su 2s ) = ( { 0s } |s { 1s } )