omeueq

Description: The division algorithm for ordinal multiplication ( omeu ) produces a unique quotient and remainder. (Contributed by BTernaryTau, 5-Oct-2026)

	Ref	Expression
Hypotheses	omeueq.1	$⊢ φ \to A \in On$
	omeueq.2	$⊢ φ \to A \neq \emptyset$
	omeueq.3	$⊢ φ \to B \in On$
	omeueq.4	$⊢ φ \to C \in A$
	omeueq.5	$⊢ φ \to D \in On$
	omeueq.6	$⊢ φ \to E \in A$
	omeueq.7	$⊢ φ \to (A \cdot_{𝑜} B) +_{𝑜} C = (A \cdot_{𝑜} D) +_{𝑜} E$
Assertion	omeueq	$⊢ φ \to (B = D \land C = E)$

Proof

Step	Hyp	Ref	Expression
1		omeueq.1	$⊢ φ \to A \in On$
2		omeueq.2	$⊢ φ \to A \neq \emptyset$
3		omeueq.3	$⊢ φ \to B \in On$
4		omeueq.4	$⊢ φ \to C \in A$
5		omeueq.5	$⊢ φ \to D \in On$
6		omeueq.6	$⊢ φ \to E \in A$
7		omeueq.7	$⊢ φ \to (A \cdot_{𝑜} B) +_{𝑜} C = (A \cdot_{𝑜} D) +_{𝑜} E$
8		omcl	$⊢ (A \in On \land B \in On) \to A \cdot_{𝑜} B \in On$
9	1 3 8	syl2anc	$⊢ φ \to A \cdot_{𝑜} B \in On$
10		onelon	$⊢ (A \in On \land C \in A) \to C \in On$
11	1 4 10	syl2anc	$⊢ φ \to C \in On$
12		oacl	$⊢ (A \cdot_{𝑜} B \in On \land C \in On) \to (A \cdot_{𝑜} B) +_{𝑜} C \in On$
13	9 11 12	syl2anc	$⊢ φ \to (A \cdot_{𝑜} B) +_{𝑜} C \in On$
14		omeu	$⊢ (A \in On \land (A \cdot_{𝑜} B) +_{𝑜} C \in On \land A \neq \emptyset) \to \exists! z \exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C)$
15	1 13 2 14	syl3anc	$⊢ φ \to \exists! z \exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C)$
16		eumo	$⊢ \exists! z \exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C) \to \exists^{*} z \exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C)$
17	15 16	syl	$⊢ φ \to \exists^{*} z \exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C)$
18		opeq1	$⊢ x = B \to ⟨x, y⟩ = ⟨B, y⟩$
19	18	eqeq2d	$⊢ x = B \to (⟨B, C⟩ = ⟨x, y⟩ \leftrightarrow ⟨B, C⟩ = ⟨B, y⟩)$
20		oveq2	$⊢ x = B \to A \cdot_{𝑜} x = A \cdot_{𝑜} B$
21	20	oveq1d	$⊢ x = B \to (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} y$
22	21	eqeq1d	$⊢ x = B \to ((A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C \leftrightarrow (A \cdot_{𝑜} B) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C)$
23	19 22	anbi12d	$⊢ x = B \to ((⟨B, C⟩ = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C) \leftrightarrow (⟨B, C⟩ = ⟨B, y⟩ \land (A \cdot_{𝑜} B) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C))$
24		opeq2	$⊢ y = C \to ⟨B, y⟩ = ⟨B, C⟩$
25	24	eqeq2d	$⊢ y = C \to (⟨B, C⟩ = ⟨B, y⟩ \leftrightarrow ⟨B, C⟩ = ⟨B, C⟩)$
26		oveq2	$⊢ y = C \to (A \cdot_{𝑜} B) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C$
27	26	eqeq1d	$⊢ y = C \to ((A \cdot_{𝑜} B) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C \leftrightarrow (A \cdot_{𝑜} B) +_{𝑜} C = (A \cdot_{𝑜} B) +_{𝑜} C)$
28	25 27	anbi12d	$⊢ y = C \to ((⟨B, C⟩ = ⟨B, y⟩ \land (A \cdot_{𝑜} B) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C) \leftrightarrow (⟨B, C⟩ = ⟨B, C⟩ \land (A \cdot_{𝑜} B) +_{𝑜} C = (A \cdot_{𝑜} B) +_{𝑜} C))$
29		eqid	$⊢ ⟨B, C⟩ = ⟨B, C⟩$
30		eqid	$⊢ (A \cdot_{𝑜} B) +_{𝑜} C = (A \cdot_{𝑜} B) +_{𝑜} C$
31	29 30	pm3.2i	$⊢ (⟨B, C⟩ = ⟨B, C⟩ \land (A \cdot_{𝑜} B) +_{𝑜} C = (A \cdot_{𝑜} B) +_{𝑜} C)$
32	31	a1i	$⊢ φ \to (⟨B, C⟩ = ⟨B, C⟩ \land (A \cdot_{𝑜} B) +_{𝑜} C = (A \cdot_{𝑜} B) +_{𝑜} C)$
33	23 28 3 4 32	2rspcedvdw	$⊢ φ \to \exists x \in On \exists y \in A (⟨B, C⟩ = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C)$
34		opeq1	$⊢ x = D \to ⟨x, y⟩ = ⟨D, y⟩$
35	34	eqeq2d	$⊢ x = D \to (⟨D, E⟩ = ⟨x, y⟩ \leftrightarrow ⟨D, E⟩ = ⟨D, y⟩)$
36		oveq2	$⊢ x = D \to A \cdot_{𝑜} x = A \cdot_{𝑜} D$
37	36	oveq1d	$⊢ x = D \to (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} D) +_{𝑜} y$
38	37	eqeq1d	$⊢ x = D \to ((A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C \leftrightarrow (A \cdot_{𝑜} D) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C)$
39	35 38	anbi12d	$⊢ x = D \to ((⟨D, E⟩ = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C) \leftrightarrow (⟨D, E⟩ = ⟨D, y⟩ \land (A \cdot_{𝑜} D) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C))$
40		opeq2	$⊢ y = E \to ⟨D, y⟩ = ⟨D, E⟩$
41	40	eqeq2d	$⊢ y = E \to (⟨D, E⟩ = ⟨D, y⟩ \leftrightarrow ⟨D, E⟩ = ⟨D, E⟩)$
42		oveq2	$⊢ y = E \to (A \cdot_{𝑜} D) +_{𝑜} y = (A \cdot_{𝑜} D) +_{𝑜} E$
43	42	eqeq1d	$⊢ y = E \to ((A \cdot_{𝑜} D) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C \leftrightarrow (A \cdot_{𝑜} D) +_{𝑜} E = (A \cdot_{𝑜} B) +_{𝑜} C)$
44	41 43	anbi12d	$⊢ y = E \to ((⟨D, E⟩ = ⟨D, y⟩ \land (A \cdot_{𝑜} D) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C) \leftrightarrow (⟨D, E⟩ = ⟨D, E⟩ \land (A \cdot_{𝑜} D) +_{𝑜} E = (A \cdot_{𝑜} B) +_{𝑜} C))$
45	7	eqcomd	$⊢ φ \to (A \cdot_{𝑜} D) +_{𝑜} E = (A \cdot_{𝑜} B) +_{𝑜} C$
46		eqid	$⊢ ⟨D, E⟩ = ⟨D, E⟩$
47	45 46	jctil	$⊢ φ \to (⟨D, E⟩ = ⟨D, E⟩ \land (A \cdot_{𝑜} D) +_{𝑜} E = (A \cdot_{𝑜} B) +_{𝑜} C)$
48	39 44 5 6 47	2rspcedvdw	$⊢ φ \to \exists x \in On \exists y \in A (⟨D, E⟩ = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C)$
49		opex	$⊢ ⟨B, C⟩ \in V$
50		opex	$⊢ ⟨D, E⟩ \in V$
51	49 50	pm3.2i	$⊢ (⟨B, C⟩ \in V \land ⟨D, E⟩ \in V)$
52		eqeq1	$⊢ z = ⟨B, C⟩ \to (z = ⟨x, y⟩ \leftrightarrow ⟨B, C⟩ = ⟨x, y⟩)$
53	52	anbi1d	$⊢ z = ⟨B, C⟩ \to ((z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C) \leftrightarrow (⟨B, C⟩ = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C))$
54	53	2rexbidv	$⊢ z = ⟨B, C⟩ \to (\exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C) \leftrightarrow \exists x \in On \exists y \in A (⟨B, C⟩ = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C))$
55		eqeq1	$⊢ z = ⟨D, E⟩ \to (z = ⟨x, y⟩ \leftrightarrow ⟨D, E⟩ = ⟨x, y⟩)$
56	55	anbi1d	$⊢ z = ⟨D, E⟩ \to ((z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C) \leftrightarrow (⟨D, E⟩ = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C))$
57	56	2rexbidv	$⊢ z = ⟨D, E⟩ \to (\exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C) \leftrightarrow \exists x \in On \exists y \in A (⟨D, E⟩ = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C))$
58	54 57	moi	$⊢ ((⟨B, C⟩ \in V \land ⟨D, E⟩ \in V) \land \exists^{*} z \exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C) \land (\exists x \in On \exists y \in A (⟨B, C⟩ = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C) \land \exists x \in On \exists y \in A (⟨D, E⟩ = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C))) \to ⟨B, C⟩ = ⟨D, E⟩$
59	51 58	mp3an1	$⊢ (\exists^{*} z \exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C) \land (\exists x \in On \exists y \in A (⟨B, C⟩ = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C) \land \exists x \in On \exists y \in A (⟨D, E⟩ = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} B) +_{𝑜} C))) \to ⟨B, C⟩ = ⟨D, E⟩$
60	17 33 48 59	syl12anc	$⊢ φ \to ⟨B, C⟩ = ⟨D, E⟩$
61		opthg	$⊢ (B \in On \land C \in A) \to (⟨B, C⟩ = ⟨D, E⟩ \leftrightarrow (B = D \land C = E))$
62	3 4 61	syl2anc	$⊢ φ \to (⟨B, C⟩ = ⟨D, E⟩ \leftrightarrow (B = D \land C = E))$
63	60 62	mpbid	$⊢ φ \to (B = D \land C = E)$

Metamath Proof Explorer

Theorem omeueq

Proof