Theorem nmulrid

Description: Identity law for natural multiplication. (Contributed by Scott Fenton, 21-Jul-2026)

	Ref	Expression
Assertion	nmulrid	Could not format assertion : No typesetting found for |- ( A e. On -> ( A .no 1o ) = A ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oveq1	Could not format ( a = b -> ( a .no 1o ) = ( b .no 1o ) ) : No typesetting found for |- ( a = b -> ( a .no 1o ) = ( b .no 1o ) ) with typecode |-
2		id	$$⊢a=b\to a=b$$
3	1 2	eqeq12d	Could not format ( a = b -> ( ( a .no 1o ) = a <-> ( b .no 1o ) = b ) ) : No typesetting found for |- ( a = b -> ( ( a .no 1o ) = a <-> ( b .no 1o ) = b ) ) with typecode |-
4		oveq1	Could not format ( a = A -> ( a .no 1o ) = ( A .no 1o ) ) : No typesetting found for |- ( a = A -> ( a .no 1o ) = ( A .no 1o ) ) with typecode |-
5		id	$$⊢a=A\to a=A$$
6	4 5	eqeq12d	Could not format ( a = A -> ( ( a .no 1o ) = a <-> ( A .no 1o ) = A ) ) : No typesetting found for |- ( a = A -> ( ( a .no 1o ) = a <-> ( A .no 1o ) = A ) ) with typecode |-
7		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
8		nmulval	Could not format ( ( a e. On /\ 1o e. On ) -> ( a .no 1o ) = |^| { x e. On | A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) } ) : No typesetting found for |- ( ( a e. On /\ 1o e. On ) -> ( a .no 1o ) = |^| { x e. On | A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) } ) with typecode |-
9	7 8	mpan2	Could not format ( a e. On -> ( a .no 1o ) = |^| { x e. On | A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) } ) : No typesetting found for |- ( a e. On -> ( a .no 1o ) = |^| { x e. On | A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) } ) with typecode |-
10	9	adantr	Could not format ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) -> ( a .no 1o ) = |^| { x e. On | A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) } ) : No typesetting found for |- ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) -> ( a .no 1o ) = |^| { x e. On | A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) } ) with typecode |-
11		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
12	11	raleqi	Could not format ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> A. y e. { (/) } ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) ) : No typesetting found for |- ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> A. y e. { (/) } ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) ) with typecode |-
13		0ex	$$⊢\varnothing \in \mathrm{V}$$
14		oveq2	Could not format ( y = (/) -> ( a .no y ) = ( a .no (/) ) ) : No typesetting found for |- ( y = (/) -> ( a .no y ) = ( a .no (/) ) ) with typecode |-
15	14	oveq2d	Could not format ( y = (/) -> ( ( b .no 1o ) +no ( a .no y ) ) = ( ( b .no 1o ) +no ( a .no (/) ) ) ) : No typesetting found for |- ( y = (/) -> ( ( b .no 1o ) +no ( a .no y ) ) = ( ( b .no 1o ) +no ( a .no (/) ) ) ) with typecode |-
16		oveq2	Could not format ( y = (/) -> ( b .no y ) = ( b .no (/) ) ) : No typesetting found for |- ( y = (/) -> ( b .no y ) = ( b .no (/) ) ) with typecode |-
17	16	oveq2d	Could not format ( y = (/) -> ( x +no ( b .no y ) ) = ( x +no ( b .no (/) ) ) ) : No typesetting found for |- ( y = (/) -> ( x +no ( b .no y ) ) = ( x +no ( b .no (/) ) ) ) with typecode |-
18	15 17	eleq12d	Could not format ( y = (/) -> ( ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> ( ( b .no 1o ) +no ( a .no (/) ) ) e. ( x +no ( b .no (/) ) ) ) ) : No typesetting found for |- ( y = (/) -> ( ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> ( ( b .no 1o ) +no ( a .no (/) ) ) e. ( x +no ( b .no (/) ) ) ) ) with typecode |-
19	13 18	ralsn	Could not format ( A. y e. { (/) } ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> ( ( b .no 1o ) +no ( a .no (/) ) ) e. ( x +no ( b .no (/) ) ) ) : No typesetting found for |- ( A. y e. { (/) } ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> ( ( b .no 1o ) +no ( a .no (/) ) ) e. ( x +no ( b .no (/) ) ) ) with typecode |-
20	12 19	bitri	Could not format ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> ( ( b .no 1o ) +no ( a .no (/) ) ) e. ( x +no ( b .no (/) ) ) ) : No typesetting found for |- ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> ( ( b .no 1o ) +no ( a .no (/) ) ) e. ( x +no ( b .no (/) ) ) ) with typecode |-
21		simprr	Could not format ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( b .no 1o ) = b ) : No typesetting found for |- ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( b .no 1o ) = b ) with typecode |-
22		nmulr0	Could not format ( a e. On -> ( a .no (/) ) = (/) ) : No typesetting found for |- ( a e. On -> ( a .no (/) ) = (/) ) with typecode |-
23	22	ad2antrr	Could not format ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( a .no (/) ) = (/) ) : No typesetting found for |- ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( a .no (/) ) = (/) ) with typecode |-
24	21 23	oveq12d	Could not format ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( ( b .no 1o ) +no ( a .no (/) ) ) = ( b +no (/) ) ) : No typesetting found for |- ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( ( b .no 1o ) +no ( a .no (/) ) ) = ( b +no (/) ) ) with typecode |-
25		onss	$$⊢a\in \mathrm{On}\to a\subseteq \mathrm{On}$$
26	25	adantr	$$⊢\left(a\in \mathrm{On}\wedge x\in \mathrm{On}\right)\to a\subseteq \mathrm{On}$$
27	26	sselda	$$⊢\left(\left(a\in \mathrm{On}\wedge x\in \mathrm{On}\right)\wedge b\in a\right)\to b\in \mathrm{On}$$
28	27	adantrr	Could not format ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> b e. On ) : No typesetting found for |- ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> b e. On ) with typecode |-
29		naddrid	$$⊢b\in \mathrm{On}\to b+\varnothing =b$$
30	28 29	syl	Could not format ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( b +no (/) ) = b ) : No typesetting found for |- ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( b +no (/) ) = b ) with typecode |-
31	24 30	eqtrd	Could not format ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( ( b .no 1o ) +no ( a .no (/) ) ) = b ) : No typesetting found for |- ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( ( b .no 1o ) +no ( a .no (/) ) ) = b ) with typecode |-
32		nmulr0	Could not format ( b e. On -> ( b .no (/) ) = (/) ) : No typesetting found for |- ( b e. On -> ( b .no (/) ) = (/) ) with typecode |-
33	28 32	syl	Could not format ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( b .no (/) ) = (/) ) : No typesetting found for |- ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( b .no (/) ) = (/) ) with typecode |-
34	33	oveq2d	Could not format ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( x +no ( b .no (/) ) ) = ( x +no (/) ) ) : No typesetting found for |- ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( x +no ( b .no (/) ) ) = ( x +no (/) ) ) with typecode |-
35		naddrid	$$⊢x\in \mathrm{On}\to x+\varnothing =x$$
36	35	ad2antlr	Could not format ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( x +no (/) ) = x ) : No typesetting found for |- ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( x +no (/) ) = x ) with typecode |-
37	34 36	eqtrd	Could not format ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( x +no ( b .no (/) ) ) = x ) : No typesetting found for |- ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( x +no ( b .no (/) ) ) = x ) with typecode |-
38	31 37	eleq12d	Could not format ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( ( ( b .no 1o ) +no ( a .no (/) ) ) e. ( x +no ( b .no (/) ) ) <-> b e. x ) ) : No typesetting found for |- ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( ( ( b .no 1o ) +no ( a .no (/) ) ) e. ( x +no ( b .no (/) ) ) <-> b e. x ) ) with typecode |-
39	20 38	bitrid	Could not format ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> b e. x ) ) : No typesetting found for |- ( ( ( a e. On /\ x e. On ) /\ ( b e. a /\ ( b .no 1o ) = b ) ) -> ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> b e. x ) ) with typecode |-
40	39	expr	Could not format ( ( ( a e. On /\ x e. On ) /\ b e. a ) -> ( ( b .no 1o ) = b -> ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> b e. x ) ) ) : No typesetting found for |- ( ( ( a e. On /\ x e. On ) /\ b e. a ) -> ( ( b .no 1o ) = b -> ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> b e. x ) ) ) with typecode |-
41	40	ralimdva	Could not format ( ( a e. On /\ x e. On ) -> ( A. b e. a ( b .no 1o ) = b -> A. b e. a ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> b e. x ) ) ) : No typesetting found for |- ( ( a e. On /\ x e. On ) -> ( A. b e. a ( b .no 1o ) = b -> A. b e. a ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> b e. x ) ) ) with typecode |-
42	41	imp	Could not format ( ( ( a e. On /\ x e. On ) /\ A. b e. a ( b .no 1o ) = b ) -> A. b e. a ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> b e. x ) ) : No typesetting found for |- ( ( ( a e. On /\ x e. On ) /\ A. b e. a ( b .no 1o ) = b ) -> A. b e. a ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> b e. x ) ) with typecode |-
43		ralbi	Could not format ( A. b e. a ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> b e. x ) -> ( A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> A. b e. a b e. x ) ) : No typesetting found for |- ( A. b e. a ( A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> b e. x ) -> ( A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> A. b e. a b e. x ) ) with typecode |-
44	42 43	syl	Could not format ( ( ( a e. On /\ x e. On ) /\ A. b e. a ( b .no 1o ) = b ) -> ( A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> A. b e. a b e. x ) ) : No typesetting found for |- ( ( ( a e. On /\ x e. On ) /\ A. b e. a ( b .no 1o ) = b ) -> ( A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> A. b e. a b e. x ) ) with typecode |-
45	44	an32s	Could not format ( ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) /\ x e. On ) -> ( A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> A. b e. a b e. x ) ) : No typesetting found for |- ( ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) /\ x e. On ) -> ( A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> A. b e. a b e. x ) ) with typecode |-
46		dfss3	$$⊢a\subseteq x\leftrightarrow \forall b\in ab\in x$$
47	45 46	bitr4di	Could not format ( ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) /\ x e. On ) -> ( A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> a C_ x ) ) : No typesetting found for |- ( ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) /\ x e. On ) -> ( A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) <-> a C_ x ) ) with typecode |-
48	47	rabbidva	Could not format ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) -> { x e. On | A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) } = { x e. On | a C_ x } ) : No typesetting found for |- ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) -> { x e. On | A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) } = { x e. On | a C_ x } ) with typecode |-
49	48	inteqd	Could not format ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) -> |^| { x e. On | A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) } = |^| { x e. On | a C_ x } ) : No typesetting found for |- ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) -> |^| { x e. On | A. b e. a A. y e. 1o ( ( b .no 1o ) +no ( a .no y ) ) e. ( x +no ( b .no y ) ) } = |^| { x e. On | a C_ x } ) with typecode |-
50		intmin	$$⊢a\in \mathrm{On}\to \bigcap \left\{x\in \mathrm{On}|a\subseteq x\right\}=a$$
51	50	adantr	Could not format ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) -> |^| { x e. On | a C_ x } = a ) : No typesetting found for |- ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) -> |^| { x e. On | a C_ x } = a ) with typecode |-
52	10 49 51	3eqtrd	Could not format ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) -> ( a .no 1o ) = a ) : No typesetting found for |- ( ( a e. On /\ A. b e. a ( b .no 1o ) = b ) -> ( a .no 1o ) = a ) with typecode |-
53	52	ex	Could not format ( a e. On -> ( A. b e. a ( b .no 1o ) = b -> ( a .no 1o ) = a ) ) : No typesetting found for |- ( a e. On -> ( A. b e. a ( b .no 1o ) = b -> ( a .no 1o ) = a ) ) with typecode |-
54	3 6 53	tfis3	Could not format ( A e. On -> ( A .no 1o ) = A ) : No typesetting found for |- ( A e. On -> ( A .no 1o ) = A ) with typecode |-