Metamath Proof Explorer

Theorem twocut

Description: Two times the cut of zero and one is one. (Contributed by Scott Fenton, 5-Sep-2025)

Ref Expression
Assertion twocut 
|- ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s

Proof

Step Hyp Ref Expression
1 0sno 
 |-  0s e. No
2 1 a1i 
 |-  ( T. -> 0s e. No )
3 1sno 
 |-  1s e. No
4 3 a1i 
 |-  ( T. -> 1s e. No )
5 0slt1s 
 |-  0s
6 5 a1i 
 |-  ( T. -> 0s
7 2 4 6 ssltsn 
 |-  ( T. -> { 0s } <
8 7 scutcld 
 |-  ( T. -> ( { 0s } |s { 1s } ) e. No )
9 8 mptru 
 |-  ( { 0s } |s { 1s } ) e. No
10 no2times 
 |-  ( ( { 0s } |s { 1s } ) e. No -> ( 2s x.s ( { 0s } |s { 1s } ) ) = ( ( { 0s } |s { 1s } ) +s ( { 0s } |s { 1s } ) ) )
11 9 10 ax-mp 
 |-  ( 2s x.s ( { 0s } |s { 1s } ) ) = ( ( { 0s } |s { 1s } ) +s ( { 0s } |s { 1s } ) )
12 eqidd 
 |-  ( T. -> ( { 0s } |s { 1s } ) = ( { 0s } |s { 1s } ) )
13 7 7 12 12 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 ) } ) ) )
14 13 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 ) } ) )
15 1 elexi 
 |-  0s e. _V
16 oveq1 
 |-  ( y = 0s -> ( y +s ( { 0s } |s { 1s } ) ) = ( 0s +s ( { 0s } |s { 1s } ) ) )
17 16 eqeq2d 
 |-  ( y = 0s -> ( x = ( y +s ( { 0s } |s { 1s } ) ) <-> x = ( 0s +s ( { 0s } |s { 1s } ) ) ) )
18 15 17 rexsn 
 |-  ( E. y e. { 0s } x = ( y +s ( { 0s } |s { 1s } ) ) <-> x = ( 0s +s ( { 0s } |s { 1s } ) ) )
19 addslid 
 |-  ( ( { 0s } |s { 1s } ) e. No -> ( 0s +s ( { 0s } |s { 1s } ) ) = ( { 0s } |s { 1s } ) )
20 9 19 ax-mp 
 |-  ( 0s +s ( { 0s } |s { 1s } ) ) = ( { 0s } |s { 1s } )
21 20 eqeq2i 
 |-  ( x = ( 0s +s ( { 0s } |s { 1s } ) ) <-> x = ( { 0s } |s { 1s } ) )
22 18 21 bitri 
 |-  ( E. y e. { 0s } x = ( y +s ( { 0s } |s { 1s } ) ) <-> x = ( { 0s } |s { 1s } ) )
23 22 abbii 
 |-  { x | E. y e. { 0s } x = ( y +s ( { 0s } |s { 1s } ) ) } = { x | x = ( { 0s } |s { 1s } ) }
24 df-sn 
 |-  { ( { 0s } |s { 1s } ) } = { x | x = ( { 0s } |s { 1s } ) }
25 23 24 eqtr4i 
 |-  { x | E. y e. { 0s } x = ( y +s ( { 0s } |s { 1s } ) ) } = { ( { 0s } |s { 1s } ) }
26 oveq2 
 |-  ( y = 0s -> ( ( { 0s } |s { 1s } ) +s y ) = ( ( { 0s } |s { 1s } ) +s 0s ) )
27 26 eqeq2d 
 |-  ( y = 0s -> ( x = ( ( { 0s } |s { 1s } ) +s y ) <-> x = ( ( { 0s } |s { 1s } ) +s 0s ) ) )
28 15 27 rexsn 
 |-  ( E. y e. { 0s } x = ( ( { 0s } |s { 1s } ) +s y ) <-> x = ( ( { 0s } |s { 1s } ) +s 0s ) )
29 addsrid 
 |-  ( ( { 0s } |s { 1s } ) e. No -> ( ( { 0s } |s { 1s } ) +s 0s ) = ( { 0s } |s { 1s } ) )
30 9 29 ax-mp 
 |-  ( ( { 0s } |s { 1s } ) +s 0s ) = ( { 0s } |s { 1s } )
31 30 eqeq2i 
 |-  ( x = ( ( { 0s } |s { 1s } ) +s 0s ) <-> x = ( { 0s } |s { 1s } ) )
32 28 31 bitri 
 |-  ( E. y e. { 0s } x = ( ( { 0s } |s { 1s } ) +s y ) <-> x = ( { 0s } |s { 1s } ) )
33 32 abbii 
 |-  { x | E. y e. { 0s } x = ( ( { 0s } |s { 1s } ) +s y ) } = { x | x = ( { 0s } |s { 1s } ) }
34 33 24 eqtr4i 
 |-  { x | E. y e. { 0s } x = ( ( { 0s } |s { 1s } ) +s y ) } = { ( { 0s } |s { 1s } ) }
35 25 34 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 } ) } )
36 unidm 
 |-  ( { ( { 0s } |s { 1s } ) } u. { ( { 0s } |s { 1s } ) } ) = { ( { 0s } |s { 1s } ) }
37 35 36 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 } ) }
38 3 elexi 
 |-  1s e. _V
39 oveq1 
 |-  ( y = 1s -> ( y +s ( { 0s } |s { 1s } ) ) = ( 1s +s ( { 0s } |s { 1s } ) ) )
40 39 eqeq2d 
 |-  ( y = 1s -> ( x = ( y +s ( { 0s } |s { 1s } ) ) <-> x = ( 1s +s ( { 0s } |s { 1s } ) ) ) )
41 38 40 rexsn 
 |-  ( E. y e. { 1s } x = ( y +s ( { 0s } |s { 1s } ) ) <-> x = ( 1s +s ( { 0s } |s { 1s } ) ) )
42 41 abbii 
 |-  { x | E. y e. { 1s } x = ( y +s ( { 0s } |s { 1s } ) ) } = { x | x = ( 1s +s ( { 0s } |s { 1s } ) ) }
43 df-sn 
 |-  { ( 1s +s ( { 0s } |s { 1s } ) ) } = { x | x = ( 1s +s ( { 0s } |s { 1s } ) ) }
44 42 43 eqtr4i 
 |-  { x | E. y e. { 1s } x = ( y +s ( { 0s } |s { 1s } ) ) } = { ( 1s +s ( { 0s } |s { 1s } ) ) }
45 oveq2 
 |-  ( y = 1s -> ( ( { 0s } |s { 1s } ) +s y ) = ( ( { 0s } |s { 1s } ) +s 1s ) )
46 45 eqeq2d 
 |-  ( y = 1s -> ( x = ( ( { 0s } |s { 1s } ) +s y ) <-> x = ( ( { 0s } |s { 1s } ) +s 1s ) ) )
47 38 46 rexsn 
 |-  ( E. y e. { 1s } x = ( ( { 0s } |s { 1s } ) +s y ) <-> x = ( ( { 0s } |s { 1s } ) +s 1s ) )
48 addscom 
 |-  ( ( ( { 0s } |s { 1s } ) e. No /\ 1s e. No ) -> ( ( { 0s } |s { 1s } ) +s 1s ) = ( 1s +s ( { 0s } |s { 1s } ) ) )
49 9 3 48 mp2an 
 |-  ( ( { 0s } |s { 1s } ) +s 1s ) = ( 1s +s ( { 0s } |s { 1s } ) )
50 49 eqeq2i 
 |-  ( x = ( ( { 0s } |s { 1s } ) +s 1s ) <-> x = ( 1s +s ( { 0s } |s { 1s } ) ) )
51 47 50 bitri 
 |-  ( E. y e. { 1s } x = ( ( { 0s } |s { 1s } ) +s y ) <-> x = ( 1s +s ( { 0s } |s { 1s } ) ) )
52 51 abbii 
 |-  { x | E. y e. { 1s } x = ( ( { 0s } |s { 1s } ) +s y ) } = { x | x = ( 1s +s ( { 0s } |s { 1s } ) ) }
53 52 43 eqtr4i 
 |-  { x | E. y e. { 1s } x = ( ( { 0s } |s { 1s } ) +s y ) } = { ( 1s +s ( { 0s } |s { 1s } ) ) }
54 44 53 uneq12i 
 |-  ( { x | E. y e. { 1s } x = ( y +s ( { 0s } |s { 1s } ) ) } u. { x | E. y e. { 1s } x = ( ( { 0s } |s { 1s } ) +s y ) } ) = ( { ( 1s +s ( { 0s } |s { 1s } ) ) } u. { ( 1s +s ( { 0s } |s { 1s } ) ) } )
55 unidm 
 |-  ( { ( 1s +s ( { 0s } |s { 1s } ) ) } u. { ( 1s +s ( { 0s } |s { 1s } ) ) } ) = { ( 1s +s ( { 0s } |s { 1s } ) ) }
56 54 55 eqtri 
 |-  ( { x | E. y e. { 1s } x = ( y +s ( { 0s } |s { 1s } ) ) } u. { x | E. y e. { 1s } x = ( ( { 0s } |s { 1s } ) +s y ) } ) = { ( 1s +s ( { 0s } |s { 1s } ) ) }
57 37 56 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 { ( 1s +s ( { 0s } |s { 1s } ) ) } )
58 ral0 
 |-  A. x e. (/) ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } )
59 scutcut 
 |-  ( { 0s } < ( ( { 0s } |s { 1s } ) e. No /\ { 0s } <
60 7 59 syl 
 |-  ( T. -> ( ( { 0s } |s { 1s } ) e. No /\ { 0s } <
61 60 simp3d 
 |-  ( T. -> { ( { 0s } |s { 1s } ) } <
62 ovex 
 |-  ( { 0s } |s { 1s } ) e. _V
63 62 snid 
 |-  ( { 0s } |s { 1s } ) e. { ( { 0s } |s { 1s } ) }
64 63 a1i 
 |-  ( T. -> ( { 0s } |s { 1s } ) e. { ( { 0s } |s { 1s } ) } )
65 38 snid 
 |-  1s e. { 1s }
66 65 a1i 
 |-  ( T. -> 1s e. { 1s } )
67 61 64 66 ssltsepcd 
 |-  ( T. -> ( { 0s } |s { 1s } )
68 67 mptru 
 |-  ( { 0s } |s { 1s } )
69 breq1 
 |-  ( y = ( { 0s } |s { 1s } ) -> ( y  ( { 0s } |s { 1s } )
70 62 69 ralsn 
 |-  ( A. y e. { ( { 0s } |s { 1s } ) } y  ( { 0s } |s { 1s } )
71 68 70 mpbir 
 |-  A. y e. { ( { 0s } |s { 1s } ) } y
72 4 8 addscld 
 |-  ( T. -> ( 1s +s ( { 0s } |s { 1s } ) ) e. No )
73 8 sltp1d 
 |-  ( T. -> ( { 0s } |s { 1s } )
74 73 49 breqtrdi 
 |-  ( T. -> ( { 0s } |s { 1s } )
75 8 72 74 ssltsn 
 |-  ( T. -> { ( { 0s } |s { 1s } ) } <
76 75 mptru 
 |-  { ( { 0s } |s { 1s } ) } <
77 snelpwi 
 |-  ( 0s e. No -> { 0s } e. ~P No )
78 1 77 ax-mp 
 |-  { 0s } e. ~P No
79 nulssgt 
 |-  ( { 0s } e. ~P No -> { 0s } <
80 78 79 ax-mp 
 |-  { 0s } <
81 eqid 
 |-  ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) = ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } )
82 df-1s 
 |-  1s = ( { 0s } |s (/) )
83 slerec 
 |-  ( ( ( { ( { 0s } |s { 1s } ) } < ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) <_s 1s <-> ( A. x e. (/) ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } )
84 76 80 81 82 83 mp4an 
 |-  ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) <_s 1s <-> ( A. x e. (/) ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } )
85 58 71 84 mpbir2an 
 |-  ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) <_s 1s
86 60 simp2d 
 |-  ( T. -> { 0s } <
87 15 snid 
 |-  0s e. { 0s }
88 87 a1i 
 |-  ( T. -> 0s e. { 0s } )
89 86 88 64 ssltsepcd 
 |-  ( T. -> 0s
90 89 mptru 
 |-  0s
91 sltadd1 
 |-  ( ( 0s e. No /\ ( { 0s } |s { 1s } ) e. No /\ 1s e. No ) -> ( 0s  ( 0s +s 1s )
92 1 9 3 91 mp3an 
 |-  ( 0s  ( 0s +s 1s )
93 90 92 mpbi 
 |-  ( 0s +s 1s )
94 addslid 
 |-  ( 1s e. No -> ( 0s +s 1s ) = 1s )
95 3 94 ax-mp 
 |-  ( 0s +s 1s ) = 1s
96 93 95 49 3brtr3i 
 |-  1s
97 ovex 
 |-  ( 1s +s ( { 0s } |s { 1s } ) ) e. _V
98 breq2 
 |-  ( x = ( 1s +s ( { 0s } |s { 1s } ) ) -> ( 1s  1s
99 97 98 ralsn 
 |-  ( A. x e. { ( 1s +s ( { 0s } |s { 1s } ) ) } 1s  1s
100 96 99 mpbir 
 |-  A. x e. { ( 1s +s ( { 0s } |s { 1s } ) ) } 1s
101 75 scutcld 
 |-  ( T. -> ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) e. No )
102 scutcut 
 |-  ( { ( { 0s } |s { 1s } ) } < ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) e. No /\ { ( { 0s } |s { 1s } ) } <
103 75 102 syl 
 |-  ( T. -> ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) e. No /\ { ( { 0s } |s { 1s } ) } <
104 103 simp2d 
 |-  ( T. -> { ( { 0s } |s { 1s } ) } <
105 ovex 
 |-  ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) e. _V
106 105 snid 
 |-  ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) e. { ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) }
107 106 a1i 
 |-  ( T. -> ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) e. { ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) } )
108 104 64 107 ssltsepcd 
 |-  ( T. -> ( { 0s } |s { 1s } )
109 2 8 101 89 108 slttrd 
 |-  ( T. -> 0s
110 109 mptru 
 |-  0s
111 breq1 
 |-  ( y = 0s -> ( y  0s
112 15 111 ralsn 
 |-  ( A. y e. { 0s } y  0s
113 110 112 mpbir 
 |-  A. y e. { 0s } y
114 slerec 
 |-  ( ( ( { 0s } < ( 1s <_s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) <-> ( A. x e. { ( 1s +s ( { 0s } |s { 1s } ) ) } 1s
115 80 76 82 81 114 mp4an 
 |-  ( 1s <_s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) <-> ( A. x e. { ( 1s +s ( { 0s } |s { 1s } ) ) } 1s
116 100 113 115 mpbir2an 
 |-  1s <_s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } )
117 101 mptru 
 |-  ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) e. No
118 sletri3 
 |-  ( ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) e. No /\ 1s e. No ) -> ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) = 1s <-> ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) <_s 1s /\ 1s <_s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ) ) )
119 117 3 118 mp2an 
 |-  ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) = 1s <-> ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) <_s 1s /\ 1s <_s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ) )
120 85 116 119 mpbir2an 
 |-  ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) = 1s
121 57 120 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
122 14 121 eqtri 
 |-  ( ( { 0s } |s { 1s } ) +s ( { 0s } |s { 1s } ) ) = 1s
123 11 122 eqtri 
 |-  ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s