Theorem nmulrid

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

	Ref	Expression
Assertion	nmulrid	⊢ ( 𝐴 ∈ On → ( 𝐴 ·no 1o ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑎 = 𝑏 → ( 𝑎 ·no 1o ) = ( 𝑏 ·no 1o ) )
2		id	⊢ ( 𝑎 = 𝑏 → 𝑎 = 𝑏 )
3	1 2	eqeq12d	⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 ·no 1o ) = 𝑎 ↔ ( 𝑏 ·no 1o ) = 𝑏 ) )
4		oveq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 ·no 1o ) = ( 𝐴 ·no 1o ) )
5		id	⊢ ( 𝑎 = 𝐴 → 𝑎 = 𝐴 )
6	4 5	eqeq12d	⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ·no 1o ) = 𝑎 ↔ ( 𝐴 ·no 1o ) = 𝐴 ) )
7		1on	⊢ 1o ∈ On
8		nmulval	⊢ ( ( 𝑎 ∈ On ∧ 1o ∈ On ) → ( 𝑎 ·no 1o ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ 1o ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) } )
9	7 8	mpan2	⊢ ( 𝑎 ∈ On → ( 𝑎 ·no 1o ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ 1o ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) } )
10	9	adantr	⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 ·no 1o ) = 𝑏 ) → ( 𝑎 ·no 1o ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ 1o ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) } )
11		df1o2	⊢ 1o = { ∅ }
12	11	raleqi	⊢ ( ∀ 𝑦 ∈ 1o ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) ↔ ∀ 𝑦 ∈ { ∅ } ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) )
13		0ex	⊢ ∅ ∈ V
14		oveq2	⊢ ( 𝑦 = ∅ → ( 𝑎 ·no 𝑦 ) = ( 𝑎 ·no ∅ ) )
15	14	oveq2d	⊢ ( 𝑦 = ∅ → ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) = ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no ∅ ) ) )
16		oveq2	⊢ ( 𝑦 = ∅ → ( 𝑏 ·no 𝑦 ) = ( 𝑏 ·no ∅ ) )
17	16	oveq2d	⊢ ( 𝑦 = ∅ → ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) = ( 𝑥 +no ( 𝑏 ·no ∅ ) ) )
18	15 17	eleq12d	⊢ ( 𝑦 = ∅ → ( ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) ↔ ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no ∅ ) ) ∈ ( 𝑥 +no ( 𝑏 ·no ∅ ) ) ) )
19	13 18	ralsn	⊢ ( ∀ 𝑦 ∈ { ∅ } ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) ↔ ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no ∅ ) ) ∈ ( 𝑥 +no ( 𝑏 ·no ∅ ) ) )
20	12 19	bitri	⊢ ( ∀ 𝑦 ∈ 1o ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) ↔ ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no ∅ ) ) ∈ ( 𝑥 +no ( 𝑏 ·no ∅ ) ) )
21		simprr	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑏 ∈ 𝑎 ∧ ( 𝑏 ·no 1o ) = 𝑏 ) ) → ( 𝑏 ·no 1o ) = 𝑏 )
22		nmulr0	⊢ ( 𝑎 ∈ On → ( 𝑎 ·no ∅ ) = ∅ )
23	22	ad2antrr	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑏 ∈ 𝑎 ∧ ( 𝑏 ·no 1o ) = 𝑏 ) ) → ( 𝑎 ·no ∅ ) = ∅ )
24	21 23	oveq12d	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑏 ∈ 𝑎 ∧ ( 𝑏 ·no 1o ) = 𝑏 ) ) → ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no ∅ ) ) = ( 𝑏 +no ∅ ) )
25		onss	⊢ ( 𝑎 ∈ On → 𝑎 ⊆ On )
26	25	adantr	⊢ ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) → 𝑎 ⊆ On )
27	26	sselda	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ 𝑏 ∈ 𝑎 ) → 𝑏 ∈ On )
28	27	adantrr	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑏 ∈ 𝑎 ∧ ( 𝑏 ·no 1o ) = 𝑏 ) ) → 𝑏 ∈ On )
29		naddrid	⊢ ( 𝑏 ∈ On → ( 𝑏 +no ∅ ) = 𝑏 )
30	28 29	syl	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑏 ∈ 𝑎 ∧ ( 𝑏 ·no 1o ) = 𝑏 ) ) → ( 𝑏 +no ∅ ) = 𝑏 )
31	24 30	eqtrd	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑏 ∈ 𝑎 ∧ ( 𝑏 ·no 1o ) = 𝑏 ) ) → ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no ∅ ) ) = 𝑏 )
32		nmulr0	⊢ ( 𝑏 ∈ On → ( 𝑏 ·no ∅ ) = ∅ )
33	28 32	syl	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑏 ∈ 𝑎 ∧ ( 𝑏 ·no 1o ) = 𝑏 ) ) → ( 𝑏 ·no ∅ ) = ∅ )
34	33	oveq2d	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑏 ∈ 𝑎 ∧ ( 𝑏 ·no 1o ) = 𝑏 ) ) → ( 𝑥 +no ( 𝑏 ·no ∅ ) ) = ( 𝑥 +no ∅ ) )
35		naddrid	⊢ ( 𝑥 ∈ On → ( 𝑥 +no ∅ ) = 𝑥 )
36	35	ad2antlr	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑏 ∈ 𝑎 ∧ ( 𝑏 ·no 1o ) = 𝑏 ) ) → ( 𝑥 +no ∅ ) = 𝑥 )
37	34 36	eqtrd	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑏 ∈ 𝑎 ∧ ( 𝑏 ·no 1o ) = 𝑏 ) ) → ( 𝑥 +no ( 𝑏 ·no ∅ ) ) = 𝑥 )
38	31 37	eleq12d	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑏 ∈ 𝑎 ∧ ( 𝑏 ·no 1o ) = 𝑏 ) ) → ( ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no ∅ ) ) ∈ ( 𝑥 +no ( 𝑏 ·no ∅ ) ) ↔ 𝑏 ∈ 𝑥 ) )
39	20 38	bitrid	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑏 ∈ 𝑎 ∧ ( 𝑏 ·no 1o ) = 𝑏 ) ) → ( ∀ 𝑦 ∈ 1o ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) ↔ 𝑏 ∈ 𝑥 ) )
40	39	expr	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ 𝑏 ∈ 𝑎 ) → ( ( 𝑏 ·no 1o ) = 𝑏 → ( ∀ 𝑦 ∈ 1o ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) ↔ 𝑏 ∈ 𝑥 ) ) )
41	40	ralimdva	⊢ ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) → ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 ·no 1o ) = 𝑏 → ∀ 𝑏 ∈ 𝑎 ( ∀ 𝑦 ∈ 1o ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) ↔ 𝑏 ∈ 𝑥 ) ) )
42	41	imp	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 ·no 1o ) = 𝑏 ) → ∀ 𝑏 ∈ 𝑎 ( ∀ 𝑦 ∈ 1o ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) ↔ 𝑏 ∈ 𝑥 ) )
43		ralbi	⊢ ( ∀ 𝑏 ∈ 𝑎 ( ∀ 𝑦 ∈ 1o ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) ↔ 𝑏 ∈ 𝑥 ) → ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ 1o ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) ↔ ∀ 𝑏 ∈ 𝑎 𝑏 ∈ 𝑥 ) )
44	42 43	syl	⊢ ( ( ( 𝑎 ∈ On ∧ 𝑥 ∈ On ) ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 ·no 1o ) = 𝑏 ) → ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ 1o ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) ↔ ∀ 𝑏 ∈ 𝑎 𝑏 ∈ 𝑥 ) )
45	44	an32s	⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 ·no 1o ) = 𝑏 ) ∧ 𝑥 ∈ On ) → ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ 1o ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) ↔ ∀ 𝑏 ∈ 𝑎 𝑏 ∈ 𝑥 ) )
46		dfss3	⊢ ( 𝑎 ⊆ 𝑥 ↔ ∀ 𝑏 ∈ 𝑎 𝑏 ∈ 𝑥 )
47	45 46	bitr4di	⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 ·no 1o ) = 𝑏 ) ∧ 𝑥 ∈ On ) → ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ 1o ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) ↔ 𝑎 ⊆ 𝑥 ) )
48	47	rabbidva	⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 ·no 1o ) = 𝑏 ) → { 𝑥 ∈ On ∣ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ 1o ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) } = { 𝑥 ∈ On ∣ 𝑎 ⊆ 𝑥 } )
49	48	inteqd	⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 ·no 1o ) = 𝑏 ) → ∩ { 𝑥 ∈ On ∣ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ 1o ( ( 𝑏 ·no 1o ) +no ( 𝑎 ·no 𝑦 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑦 ) ) } = ∩ { 𝑥 ∈ On ∣ 𝑎 ⊆ 𝑥 } )
50		intmin	⊢ ( 𝑎 ∈ On → ∩ { 𝑥 ∈ On ∣ 𝑎 ⊆ 𝑥 } = 𝑎 )
51	50	adantr	⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 ·no 1o ) = 𝑏 ) → ∩ { 𝑥 ∈ On ∣ 𝑎 ⊆ 𝑥 } = 𝑎 )
52	10 49 51	3eqtrd	⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 ·no 1o ) = 𝑏 ) → ( 𝑎 ·no 1o ) = 𝑎 )
53	52	ex	⊢ ( 𝑎 ∈ On → ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 ·no 1o ) = 𝑏 → ( 𝑎 ·no 1o ) = 𝑎 ) )
54	3 6 53	tfis3	⊢ ( 𝐴 ∈ On → ( 𝐴 ·no 1o ) = 𝐴 )