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