Theorem nohalf 28422

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

Assertion

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

Proof of Theorem nohalf

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		snex 5442	. . . . . . . 8 ⊢ { 0s } ∈ V
2	1	a1i 11	. . . . . . 7 ⊢ (⊤ → { 0s } ∈ V)
3		snex 5442	. . . . . . . 8 ⊢ { 1s } ∈ V
4	3	a1i 11	. . . . . . 7 ⊢ (⊤ → { 1s } ∈ V)
5		0sno 27886	. . . . . . . . 9 ⊢ 0s ∈ No
6	5	a1i 11	. . . . . . . 8 ⊢ (⊤ → 0s ∈ No )
7	6	snssd 4814	. . . . . . 7 ⊢ (⊤ → { 0s } ⊆ No )
8		1sno 27887	. . . . . . . 8 ⊢ 1s ∈ No
9		snssi 4813	. . . . . . . 8 ⊢ ( 1s ∈ No → { 1s } ⊆ No )
10	8, 9	mp1i 13	. . . . . . 7 ⊢ (⊤ → { 1s } ⊆ No )
11		velsn 4647	. . . . . . . . 9 ⊢ (𝑥 ∈ { 0s } ↔ 𝑥 = 0s )
12		velsn 4647	. . . . . . . . 9 ⊢ (𝑦 ∈ { 1s } ↔ 𝑦 = 1s )
13		0slt1s 27889	. . . . . . . . . 10 ⊢ 0s <s 1s
14		breq12 5153	. . . . . . . . . 10 ⊢ ((𝑥 = 0s ∧ 𝑦 = 1s ) → (𝑥 <s 𝑦 ↔ 0s <s 1s ))
15	13, 14	mpbiri 258	. . . . . . . . 9 ⊢ ((𝑥 = 0s ∧ 𝑦 = 1s ) → 𝑥 <s 𝑦)
16	11, 12, 15	syl2anb 598	. . . . . . . 8 ⊢ ((𝑥 ∈ { 0s } ∧ 𝑦 ∈ { 1s }) → 𝑥 <s 𝑦)
17	16	3adant1 1129	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ { 0s } ∧ 𝑦 ∈ { 1s }) → 𝑥 <s 𝑦)
18	2, 4, 7, 10, 17	ssltd 27851	. . . . . 6 ⊢ (⊤ → { 0s } <<s { 1s })
19	18	scutcld 27863	. . . . 5 ⊢ (⊤ → ({ 0s } |s { 1s }) ∈ No )
20	19	mptru 1544	. . . 4 ⊢ ({ 0s } |s { 1s }) ∈ No
21		no2times 28416	. . . 4 ⊢ (({ 0s } |s { 1s }) ∈ No → (2s ·s ({ 0s } |s { 1s })) = (({ 0s } |s { 1s }) +s ({ 0s } |s { 1s })))
22	20, 21	ax-mp 5	. . 3 ⊢ (2s ·s ({ 0s } |s { 1s })) = (({ 0s } |s { 1s }) +s ({ 0s } |s { 1s }))
23		eqidd 2736	. . . . . 6 ⊢ (⊤ → ({ 0s } |s { 1s }) = ({ 0s } |s { 1s }))
24	18, 18, 23, 23	addsunif 28050	. . . . 5 ⊢ (⊤ → (({ 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 1544	. . . 4 ⊢ (({ 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 3501	. . . . . . . . . . 11 ⊢ 0s ∈ V
27		oveq1 7438	. . . . . . . . . . . . 13 ⊢ (𝑦 = 0s → (𝑦 +s ({ 0s } |s { 1s })) = ( 0s +s ({ 0s } |s { 1s })))
28		addslid 28016	. . . . . . . . . . . . . 14 ⊢ (({ 0s } |s { 1s }) ∈ No → ( 0s +s ({ 0s } |s { 1s })) = ({ 0s } |s { 1s }))
29	20, 28	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ( 0s +s ({ 0s } |s { 1s })) = ({ 0s } |s { 1s })
30	27, 29	eqtrdi 2791	. . . . . . . . . . . 12 ⊢ (𝑦 = 0s → (𝑦 +s ({ 0s } |s { 1s })) = ({ 0s } |s { 1s }))
31	30	eqeq2d 2746	. . . . . . . . . . 11 ⊢ (𝑦 = 0s → (𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ({ 0s } |s { 1s })))
32	26, 31	rexsn 4687	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ({ 0s } |s { 1s }))
33	32	abbii 2807	. . . . . . . . 9 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
34		df-sn 4632	. . . . . . . . 9 ⊢ {({ 0s } |s { 1s })} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
35	33, 34	eqtr4i 2766	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {({ 0s } |s { 1s })}
36		oveq2 7439	. . . . . . . . . . . . 13 ⊢ (𝑦 = 0s → (({ 0s } |s { 1s }) +s 𝑦) = (({ 0s } |s { 1s }) +s 0s ))
37		addsrid 28012	. . . . . . . . . . . . . 14 ⊢ (({ 0s } |s { 1s }) ∈ No → (({ 0s } |s { 1s }) +s 0s ) = ({ 0s } |s { 1s }))
38	20, 37	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (({ 0s } |s { 1s }) +s 0s ) = ({ 0s } |s { 1s })
39	36, 38	eqtrdi 2791	. . . . . . . . . . . 12 ⊢ (𝑦 = 0s → (({ 0s } |s { 1s }) +s 𝑦) = ({ 0s } |s { 1s }))
40	39	eqeq2d 2746	. . . . . . . . . . 11 ⊢ (𝑦 = 0s → (𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = ({ 0s } |s { 1s })))
41	26, 40	rexsn 4687	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = ({ 0s } |s { 1s }))
42	41	abbii 2807	. . . . . . . . 9 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
43	42, 34	eqtr4i 2766	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {({ 0s } |s { 1s })}
44	35, 43	uneq12i 4176	. . . . . . 7 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = ({({ 0s } |s { 1s })} ∪ {({ 0s } |s { 1s })})
45		unidm 4167	. . . . . . 7 ⊢ ({({ 0s } |s { 1s })} ∪ {({ 0s } |s { 1s })}) = {({ 0s } |s { 1s })}
46	44, 45	eqtri 2763	. . . . . 6 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = {({ 0s } |s { 1s })}
47	8	elexi 3501	. . . . . . . . . . 11 ⊢ 1s ∈ V
48		oveq1 7438	. . . . . . . . . . . . 13 ⊢ (𝑦 = 1s → (𝑦 +s ({ 0s } |s { 1s })) = ( 1s +s ({ 0s } |s { 1s })))
49		addscom 28014	. . . . . . . . . . . . . 14 ⊢ (( 1s ∈ No ∧ ({ 0s } |s { 1s }) ∈ No ) → ( 1s +s ({ 0s } |s { 1s })) = (({ 0s } |s { 1s }) +s 1s ))
50	8, 20, 49	mp2an 692	. . . . . . . . . . . . 13 ⊢ ( 1s +s ({ 0s } |s { 1s })) = (({ 0s } |s { 1s }) +s 1s )
51	48, 50	eqtrdi 2791	. . . . . . . . . . . 12 ⊢ (𝑦 = 1s → (𝑦 +s ({ 0s } |s { 1s })) = (({ 0s } |s { 1s }) +s 1s ))
52	51	eqeq2d 2746	. . . . . . . . . . 11 ⊢ (𝑦 = 1s → (𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s )))
53	47, 52	rexsn 4687	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s ))
54	53	abbii 2807	. . . . . . . . 9 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {𝑥 ∣ 𝑥 = (({ 0s } |s { 1s }) +s 1s )}
55		df-sn 4632	. . . . . . . . 9 ⊢ {(({ 0s } |s { 1s }) +s 1s )} = {𝑥 ∣ 𝑥 = (({ 0s } |s { 1s }) +s 1s )}
56	54, 55	eqtr4i 2766	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {(({ 0s } |s { 1s }) +s 1s )}
57		oveq2 7439	. . . . . . . . . . . 12 ⊢ (𝑦 = 1s → (({ 0s } |s { 1s }) +s 𝑦) = (({ 0s } |s { 1s }) +s 1s ))
58	57	eqeq2d 2746	. . . . . . . . . . 11 ⊢ (𝑦 = 1s → (𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s )))
59	47, 58	rexsn 4687	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s ))
60	59	abbii 2807	. . . . . . . . 9 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {𝑥 ∣ 𝑥 = (({ 0s } |s { 1s }) +s 1s )}
61	60, 55	eqtr4i 2766	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {(({ 0s } |s { 1s }) +s 1s )}
62	56, 61	uneq12i 4176	. . . . . . 7 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = ({(({ 0s } |s { 1s }) +s 1s )} ∪ {(({ 0s } |s { 1s }) +s 1s )})
63		unidm 4167	. . . . . . 7 ⊢ ({(({ 0s } |s { 1s }) +s 1s )} ∪ {(({ 0s } |s { 1s }) +s 1s )}) = {(({ 0s } |s { 1s }) +s 1s )}
64	62, 63	eqtri 2763	. . . . . 6 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = {(({ 0s } |s { 1s }) +s 1s )}
65	46, 64	oveq12i 7443	. . . . 5 ⊢ (({𝑥 ∣ ∃𝑦 ∈ { 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 4519	. . . . . . 7 ⊢ ∀𝑥 ∈ ∅ ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) <s 𝑥
67		slerflex 27823	. . . . . . . . . . . 12 ⊢ ( 1s ∈ No → 1s ≤s 1s )
68	8, 67	ax-mp 5	. . . . . . . . . . 11 ⊢ 1s ≤s 1s
69		breq1 5151	. . . . . . . . . . . 12 ⊢ (𝑦 = 1s → (𝑦 ≤s 1s ↔ 1s ≤s 1s ))
70	47, 69	rexsn 4687	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ { 1s }𝑦 ≤s 1s ↔ 1s ≤s 1s )
71	68, 70	mpbir 231	. . . . . . . . . 10 ⊢ ∃𝑦 ∈ { 1s }𝑦 ≤s 1s
72	71	olci 866	. . . . . . . . 9 ⊢ (∃𝑥 ∈ { 0s } ({ 0s } |s { 1s }) ≤s 𝑥 ∨ ∃𝑦 ∈ { 1s }𝑦 ≤s 1s )
73	18	mptru 1544	. . . . . . . . . 10 ⊢ { 0s } <<s { 1s }
74		snelpwi 5454	. . . . . . . . . . . 12 ⊢ ( 0s ∈ No → { 0s } ∈ 𝒫 No )
75	5, 74	ax-mp 5	. . . . . . . . . . 11 ⊢ { 0s } ∈ 𝒫 No
76		nulssgt 27858	. . . . . . . . . . 11 ⊢ ({ 0s } ∈ 𝒫 No → { 0s } <<s ∅)
77	75, 76	ax-mp 5	. . . . . . . . . 10 ⊢ { 0s } <<s ∅
78		eqid 2735	. . . . . . . . . 10 ⊢ ({ 0s } |s { 1s }) = ({ 0s } |s { 1s })
79		df-1s 27885	. . . . . . . . . 10 ⊢ 1s = ({ 0s } |s ∅)
80		sltrec 27880	. . . . . . . . . 10 ⊢ ((({ 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 693	. . . . . . . . 9 ⊢ (({ 0s } |s { 1s }) <s 1s ↔ (∃𝑥 ∈ { 0s } ({ 0s } |s { 1s }) ≤s 𝑥 ∨ ∃𝑦 ∈ { 1s }𝑦 ≤s 1s ))
82	72, 81	mpbir 231	. . . . . . . 8 ⊢ ({ 0s } |s { 1s }) <s 1s
83		ovex 7464	. . . . . . . . 9 ⊢ ({ 0s } |s { 1s }) ∈ V
84		breq1 5151	. . . . . . . . 9 ⊢ (𝑦 = ({ 0s } |s { 1s }) → (𝑦 <s 1s ↔ ({ 0s } |s { 1s }) <s 1s ))
85	83, 84	ralsn 4686	. . . . . . . 8 ⊢ (∀𝑦 ∈ {({ 0s } |s { 1s })}𝑦 <s 1s ↔ ({ 0s } |s { 1s }) <s 1s )
86	82, 85	mpbir 231	. . . . . . 7 ⊢ ∀𝑦 ∈ {({ 0s } |s { 1s })}𝑦 <s 1s
87		snex 5442	. . . . . . . . . . 11 ⊢ {({ 0s } |s { 1s })} ∈ V
88	87	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → {({ 0s } |s { 1s })} ∈ V)
89		snex 5442	. . . . . . . . . . 11 ⊢ {(({ 0s } |s { 1s }) +s 1s )} ∈ V
90	89	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → {(({ 0s } |s { 1s }) +s 1s )} ∈ V)
91	19	snssd 4814	. . . . . . . . . 10 ⊢ (⊤ → {({ 0s } |s { 1s })} ⊆ No )
92	8	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → 1s ∈ No )
93	19, 92	addscld 28028	. . . . . . . . . . 11 ⊢ (⊤ → (({ 0s } |s { 1s }) +s 1s ) ∈ No )
94	93	snssd 4814	. . . . . . . . . 10 ⊢ (⊤ → {(({ 0s } |s { 1s }) +s 1s )} ⊆ No )
95		velsn 4647	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {({ 0s } |s { 1s })} ↔ 𝑥 = ({ 0s } |s { 1s }))
96		velsn 4647	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {(({ 0s } |s { 1s }) +s 1s )} ↔ 𝑦 = (({ 0s } |s { 1s }) +s 1s ))
97		sltadd2 28039	. . . . . . . . . . . . . . . 16 ⊢ (( 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 1460	. . . . . . . . . . . . . . 15 ⊢ ( 0s <s 1s ↔ (({ 0s } |s { 1s }) +s 0s ) <s (({ 0s } |s { 1s }) +s 1s ))
99	13, 98	mpbi 230	. . . . . . . . . . . . . 14 ⊢ (({ 0s } |s { 1s }) +s 0s ) <s (({ 0s } |s { 1s }) +s 1s )
100	38, 99	eqbrtrri 5171	. . . . . . . . . . . . 13 ⊢ ({ 0s } |s { 1s }) <s (({ 0s } |s { 1s }) +s 1s )
101		breq12 5153	. . . . . . . . . . . . 13 ⊢ ((𝑥 = ({ 0s } |s { 1s }) ∧ 𝑦 = (({ 0s } |s { 1s }) +s 1s )) → (𝑥 <s 𝑦 ↔ ({ 0s } |s { 1s }) <s (({ 0s } |s { 1s }) +s 1s )))
102	100, 101	mpbiri 258	. . . . . . . . . . . 12 ⊢ ((𝑥 = ({ 0s } |s { 1s }) ∧ 𝑦 = (({ 0s } |s { 1s }) +s 1s )) → 𝑥 <s 𝑦)
103	95, 96, 102	syl2anb 598	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ {({ 0s } |s { 1s })} ∧ 𝑦 ∈ {(({ 0s } |s { 1s }) +s 1s )}) → 𝑥 <s 𝑦)
104	103	3adant1 1129	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ {({ 0s } |s { 1s })} ∧ 𝑦 ∈ {(({ 0s } |s { 1s }) +s 1s )}) → 𝑥 <s 𝑦)
105	88, 90, 91, 94, 104	ssltd 27851	. . . . . . . . 9 ⊢ (⊤ → {({ 0s } |s { 1s })} <<s {(({ 0s } |s { 1s }) +s 1s )})
106	105	mptru 1544	. . . . . . . 8 ⊢ {({ 0s } |s { 1s })} <<s {(({ 0s } |s { 1s }) +s 1s )}
107		eqid 2735	. . . . . . . 8 ⊢ ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) = ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )})
108		slerec 27879	. . . . . . . 8 ⊢ ((({({ 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 693	. . . . . . 7 ⊢ (({({ 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 711	. . . . . 6 ⊢ ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ≤s 1s
111		addslid 28016	. . . . . . . . . 10 ⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
112	8, 111	ax-mp 5	. . . . . . . . 9 ⊢ ( 0s +s 1s ) = 1s
113		slerflex 27823	. . . . . . . . . . . . . 14 ⊢ ( 0s ∈ No → 0s ≤s 0s )
114	5, 113	ax-mp 5	. . . . . . . . . . . . 13 ⊢ 0s ≤s 0s
115		breq2 5152	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 0s → ( 0s ≤s 𝑥 ↔ 0s ≤s 0s ))
116	26, 115	rexsn 4687	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ { 0s } 0s ≤s 𝑥 ↔ 0s ≤s 0s )
117	114, 116	mpbir 231	. . . . . . . . . . . 12 ⊢ ∃𝑥 ∈ { 0s } 0s ≤s 𝑥
118	117	orci 865	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ { 0s } 0s ≤s 𝑥 ∨ ∃𝑦 ∈ ∅ 𝑦 ≤s ({ 0s } |s { 1s }))
119		0elpw 5362	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 𝒫 No
120		nulssgt 27858	. . . . . . . . . . . . 13 ⊢ (∅ ∈ 𝒫 No → ∅ <<s ∅)
121	119, 120	ax-mp 5	. . . . . . . . . . . 12 ⊢ ∅ <<s ∅
122		df-0s 27884	. . . . . . . . . . . 12 ⊢ 0s = (∅ |s ∅)
123		sltrec 27880	. . . . . . . . . . . 12 ⊢ (((∅ <<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 693	. . . . . . . . . . 11 ⊢ ( 0s <s ({ 0s } |s { 1s }) ↔ (∃𝑥 ∈ { 0s } 0s ≤s 𝑥 ∨ ∃𝑦 ∈ ∅ 𝑦 ≤s ({ 0s } |s { 1s })))
125	118, 124	mpbir 231	. . . . . . . . . 10 ⊢ 0s <s ({ 0s } |s { 1s })
126		sltadd1 28040	. . . . . . . . . . 11 ⊢ (( 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 1460	. . . . . . . . . 10 ⊢ ( 0s <s ({ 0s } |s { 1s }) ↔ ( 0s +s 1s ) <s (({ 0s } |s { 1s }) +s 1s ))
128	125, 127	mpbi 230	. . . . . . . . 9 ⊢ ( 0s +s 1s ) <s (({ 0s } |s { 1s }) +s 1s )
129	112, 128	eqbrtrri 5171	. . . . . . . 8 ⊢ 1s <s (({ 0s } |s { 1s }) +s 1s )
130		ovex 7464	. . . . . . . . 9 ⊢ (({ 0s } |s { 1s }) +s 1s ) ∈ V
131		breq2 5152	. . . . . . . . 9 ⊢ (𝑦 = (({ 0s } |s { 1s }) +s 1s ) → ( 1s <s 𝑦 ↔ 1s <s (({ 0s } |s { 1s }) +s 1s )))
132	130, 131	ralsn 4686	. . . . . . . 8 ⊢ (∀𝑦 ∈ {(({ 0s } |s { 1s }) +s 1s )} 1s <s 𝑦 ↔ 1s <s (({ 0s } |s { 1s }) +s 1s ))
133	129, 132	mpbir 231	. . . . . . 7 ⊢ ∀𝑦 ∈ {(({ 0s } |s { 1s }) +s 1s )} 1s <s 𝑦
134		breq2 5152	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1s → ( 0s <s 𝑥 ↔ 0s <s 1s ))
135	47, 134	ralsn 4686	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ { 1s } 0s <s 𝑥 ↔ 0s <s 1s )
136	13, 135	mpbir 231	. . . . . . . . . . . 12 ⊢ ∀𝑥 ∈ { 1s } 0s <s 𝑥
137		ral0 4519	. . . . . . . . . . . 12 ⊢ ∀𝑦 ∈ ∅ 𝑦 <s ({ 0s } |s { 1s })
138		slerec 27879	. . . . . . . . . . . . 13 ⊢ (((∅ <<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 693	. . . . . . . . . . . 12 ⊢ ( 0s ≤s ({ 0s } |s { 1s }) ↔ (∀𝑥 ∈ { 1s } 0s <s 𝑥 ∧ ∀𝑦 ∈ ∅ 𝑦 <s ({ 0s } |s { 1s })))
140	136, 137, 139	mpbir2an 711	. . . . . . . . . . 11 ⊢ 0s ≤s ({ 0s } |s { 1s })
141		breq2 5152	. . . . . . . . . . . 12 ⊢ (𝑥 = ({ 0s } |s { 1s }) → ( 0s ≤s 𝑥 ↔ 0s ≤s ({ 0s } |s { 1s })))
142	83, 141	rexsn 4687	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ {({ 0s } |s { 1s })} 0s ≤s 𝑥 ↔ 0s ≤s ({ 0s } |s { 1s }))
143	140, 142	mpbir 231	. . . . . . . . . 10 ⊢ ∃𝑥 ∈ {({ 0s } |s { 1s })} 0s ≤s 𝑥
144	143	orci 865	. . . . . . . . 9 ⊢ (∃𝑥 ∈ {({ 0s } |s { 1s })} 0s ≤s 𝑥 ∨ ∃𝑦 ∈ ∅ 𝑦 ≤s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}))
145		sltrec 27880	. . . . . . . . . 10 ⊢ (((∅ <<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 693	. . . . . . . . 9 ⊢ ( 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 231	. . . . . . . 8 ⊢ 0s <s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )})
148		breq1 5151	. . . . . . . . 9 ⊢ (𝑥 = 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 4686	. . . . . . . 8 ⊢ (∀𝑥 ∈ { 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 231	. . . . . . 7 ⊢ ∀𝑥 ∈ { 0s }𝑥 <s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )})
151		slerec 27879	. . . . . . . 8 ⊢ ((({ 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 693	. . . . . . 7 ⊢ ( 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 711	. . . . . 6 ⊢ 1s ≤s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )})
154	105	scutcld 27863	. . . . . . . 8 ⊢ (⊤ → ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ∈ No )
155	154	mptru 1544	. . . . . . 7 ⊢ ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ∈ No
156		sletri3 27815	. . . . . . 7 ⊢ ((({({ 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 692	. . . . . 6 ⊢ (({({ 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 711	. . . . 5 ⊢ ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) = 1s
159	65, 158	eqtri 2763	. . . 4 ⊢ (({𝑥 ∣ ∃𝑦 ∈ { 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 2763	. . 3 ⊢ (({ 0s } |s { 1s }) +s ({ 0s } |s { 1s })) = 1s
161	22, 160	eqtri 2763	. 2 ⊢ (2s ·s ({ 0s } |s { 1s })) = 1s
162		2sno 28418	. . . . 5 ⊢ 2s ∈ No
163		2ne0s 28419	. . . . 5 ⊢ 2s ≠ 0s
164	162, 163	pm3.2i 470	. . . 4 ⊢ (2s ∈ No ∧ 2s ≠ 0s )
165	8, 20, 164	3pm3.2i 1338	. . 3 ⊢ ( 1s ∈ No ∧ ({ 0s } |s { 1s }) ∈ No ∧ (2s ∈ No ∧ 2s ≠ 0s ))
166		oveq2 7439	. . . . . 6 ⊢ (𝑥 = ({ 0s } |s { 1s }) → (2s ·s 𝑥) = (2s ·s ({ 0s } |s { 1s })))
167	166	eqeq1d 2737	. . . . 5 ⊢ (𝑥 = ({ 0s } |s { 1s }) → ((2s ·s 𝑥) = 1s ↔ (2s ·s ({ 0s } |s { 1s })) = 1s ))
168	167	rspcev 3622	. . . 4 ⊢ ((({ 0s } |s { 1s }) ∈ No ∧ (2s ·s ({ 0s } |s { 1s })) = 1s ) → ∃𝑥 ∈ No (2s ·s 𝑥) = 1s )
169	20, 161, 168	mp2an 692	. . 3 ⊢ ∃𝑥 ∈ No (2s ·s 𝑥) = 1s
170		divsmulw 28233	. . 3 ⊢ ((( 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 692	. 2 ⊢ (( 1s /su 2s) = ({ 0s } |s { 1s }) ↔ (2s ·s ({ 0s } |s { 1s })) = 1s )
172	161, 171	mpbir 231	1 ⊢ ( 1s /su 2s) = ({ 0s } |s { 1s })

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1537  ⊤wtru 1538   ∈ wcel 2106  {cab 2712   ≠ wne 2938  ∀wral 3059  ∃wrex 3068  Vcvv 3478   ∪ cun 3961   ⊆ wss 3963  ∅c0 4339  𝒫 cpw 4605  {csn 4631   class class class wbr 5148  (class class class)co 7431   No csur 27699   <s cslt 27700   ≤s csle 27804   <<s csslt 27840   |s cscut 27842   0_s c0s 27882   1_s c1s 27883   +_s cadds 28007   ·_s cmuls 28147   /_su cdivs 28228  2_sc2s 28409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-ot 4640  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-nadd 8703  df-no 27702  df-slt 27703  df-bday 27704  df-sle 27805  df-sslt 27841  df-scut 27843  df-0s 27884  df-1s 27885  df-made 27901  df-old 27902  df-left 27904  df-right 27905  df-norec 27986  df-norec2 27997  df-adds 28008  df-negs 28068  df-subs 28069  df-muls 28148  df-divs 28229  df-n0s 28335  df-nns 28336  df-2s 28410

This theorem is referenced by:  cutpw2  28432