Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐴 ∈ On )
omeueq.2 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
omeueq.3 ⊢ ( 𝜑 → 𝐵 ∈ On )
omeueq.4 ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
omeueq.5 ⊢ ( 𝜑 → 𝐷 ∈ On )
omeueq.6 ⊢ ( 𝜑 → 𝐸 ∈ 𝐴 )
omeueq.7 ⊢ ( 𝜑 → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) )
Assertion omeueq ( 𝜑 → ( 𝐵 = 𝐷 ∧ 𝐶 = 𝐸 ) )

Proof

Step Hyp Ref Expression
1 omeueq.1 ⊢ ( 𝜑 → 𝐴 ∈ On )
2 omeueq.2 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3 omeueq.3 ⊢ ( 𝜑 → 𝐵 ∈ On )
4 omeueq.4 ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
5 omeueq.5 ⊢ ( 𝜑 → 𝐷 ∈ On )
6 omeueq.6 ⊢ ( 𝜑 → 𝐸 ∈ 𝐴 )
7 omeueq.7 ⊢ ( 𝜑 → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) )
8 omcl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) ∈ On )
9 1 3 8 syl2anc ⊢ ( 𝜑 → ( 𝐴 ·o 𝐵 ) ∈ On )
10 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ On )
11 1 4 10 syl2anc ⊢ ( 𝜑 → 𝐶 ∈ On )
12 oacl ⊢ ( ( ( 𝐴 ·o 𝐵 ) ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ On )
13 9 11 12 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ On )
14 omeu ⊢ ( ( 𝐴 ∈ On ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ∈ On ∧ 𝐴 ≠ ∅ ) → ∃! 𝑧 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) )
15 1 13 2 14 syl3anc ⊢ ( 𝜑 → ∃! 𝑧 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) )
16 eumo ⊢ ( ∃! 𝑧 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) → ∃* 𝑧 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) )
17 15 16 syl ⊢ ( 𝜑 → ∃* 𝑧 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) )
18 opeq1 ⊢ ( 𝑥 = 𝐵 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝑦 ⟩ )
19 18 eqeq2d ⊢ ( 𝑥 = 𝐵 → ( ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝐵 , 𝑦 ⟩ ) )
20 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o 𝐵 ) )
21 20 oveq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝑦 ) )
22 21 eqeq1d ⊢ ( 𝑥 = 𝐵 → ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ↔ ( ( 𝐴 ·o 𝐵 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) )
23 19 22 anbi12d ⊢ ( 𝑥 = 𝐵 → ( ( ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ↔ ( ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝐵 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ) )
24 opeq2 ⊢ ( 𝑦 = 𝐶 → ⟨ 𝐵 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ )
25 24 eqeq2d ⊢ ( 𝑦 = 𝐶 → ( ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝐵 , 𝑦 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) )
26 oveq2 ⊢ ( 𝑦 = 𝐶 → ( ( 𝐴 ·o 𝐵 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) )
27 26 eqeq1d ⊢ ( 𝑦 = 𝐶 → ( ( ( 𝐴 ·o 𝐵 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ↔ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) )
28 25 27 anbi12d ⊢ ( 𝑦 = 𝐶 → ( ( ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝐵 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ↔ ( ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ) )
29 eqid ⊢ ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝐵 , 𝐶 ⟩
30 eqid ⊢ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 )
31 29 30 pm3.2i ⊢ ( ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) )
32 31 a1i ⊢ ( 𝜑 → ( ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ∧ ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) )
33 23 28 3 4 32 2rspcedvdw ⊢ ( 𝜑 → ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) )
34 opeq1 ⊢ ( 𝑥 = 𝐷 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐷 , 𝑦 ⟩ )
35 34 eqeq2d ⊢ ( 𝑥 = 𝐷 → ( ⟨ 𝐷 , 𝐸 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝐷 , 𝐸 ⟩ = ⟨ 𝐷 , 𝑦 ⟩ ) )
36 oveq2 ⊢ ( 𝑥 = 𝐷 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o 𝐷 ) )
37 36 oveq1d ⊢ ( 𝑥 = 𝐷 → ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝑦 ) )
38 37 eqeq1d ⊢ ( 𝑥 = 𝐷 → ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ↔ ( ( 𝐴 ·o 𝐷 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) )
39 35 38 anbi12d ⊢ ( 𝑥 = 𝐷 → ( ( ⟨ 𝐷 , 𝐸 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ↔ ( ⟨ 𝐷 , 𝐸 ⟩ = ⟨ 𝐷 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝐷 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ) )
40 opeq2 ⊢ ( 𝑦 = 𝐸 → ⟨ 𝐷 , 𝑦 ⟩ = ⟨ 𝐷 , 𝐸 ⟩ )
41 40 eqeq2d ⊢ ( 𝑦 = 𝐸 → ( ⟨ 𝐷 , 𝐸 ⟩ = ⟨ 𝐷 , 𝑦 ⟩ ↔ ⟨ 𝐷 , 𝐸 ⟩ = ⟨ 𝐷 , 𝐸 ⟩ ) )
42 oveq2 ⊢ ( 𝑦 = 𝐸 → ( ( 𝐴 ·o 𝐷 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) )
43 42 eqeq1d ⊢ ( 𝑦 = 𝐸 → ( ( ( 𝐴 ·o 𝐷 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ↔ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) )
44 41 43 anbi12d ⊢ ( 𝑦 = 𝐸 → ( ( ⟨ 𝐷 , 𝐸 ⟩ = ⟨ 𝐷 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝐷 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ↔ ( ⟨ 𝐷 , 𝐸 ⟩ = ⟨ 𝐷 , 𝐸 ⟩ ∧ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ) )
45 7 eqcomd ⊢ ( 𝜑 → ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) )
46 eqid ⊢ ⟨ 𝐷 , 𝐸 ⟩ = ⟨ 𝐷 , 𝐸 ⟩
47 45 46 jctil ⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ = ⟨ 𝐷 , 𝐸 ⟩ ∧ ( ( 𝐴 ·o 𝐷 ) +o 𝐸 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) )
48 39 44 5 6 47 2rspcedvdw ⊢ ( 𝜑 → ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( ⟨ 𝐷 , 𝐸 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) )
49 opex ⊢ ⟨ 𝐵 , 𝐶 ⟩ ∈ V
50 opex ⊢ ⟨ 𝐷 , 𝐸 ⟩ ∈ V
51 49 50 pm3.2i ⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ V ∧ ⟨ 𝐷 , 𝐸 ⟩ ∈ V )
52 eqeq1 ⊢ ( 𝑧 = ⟨ 𝐵 , 𝐶 ⟩ → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
53 52 anbi1d ⊢ ( 𝑧 = ⟨ 𝐵 , 𝐶 ⟩ → ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ↔ ( ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ) )
54 53 2rexbidv ⊢ ( 𝑧 = ⟨ 𝐵 , 𝐶 ⟩ → ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ↔ ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ) )
55 eqeq1 ⊢ ( 𝑧 = ⟨ 𝐷 , 𝐸 ⟩ → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝐷 , 𝐸 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
56 55 anbi1d ⊢ ( 𝑧 = ⟨ 𝐷 , 𝐸 ⟩ → ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ↔ ( ⟨ 𝐷 , 𝐸 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ) )
57 56 2rexbidv ⊢ ( 𝑧 = ⟨ 𝐷 , 𝐸 ⟩ → ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ↔ ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( ⟨ 𝐷 , 𝐸 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ) )
58 54 57 moi ⊢ ( ( ( ⟨ 𝐵 , 𝐶 ⟩ ∈ V ∧ ⟨ 𝐷 , 𝐸 ⟩ ∈ V ) ∧ ∃* 𝑧 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ∧ ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ∧ ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( ⟨ 𝐷 , 𝐸 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ) ) → ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝐷 , 𝐸 ⟩ )
59 51 58 mp3an1 ⊢ ( ( ∃* 𝑧 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ∧ ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ∧ ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( ⟨ 𝐷 , 𝐸 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐶 ) ) ) ) → ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝐷 , 𝐸 ⟩ )
60 17 33 48 59 syl12anc ⊢ ( 𝜑 → ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝐷 , 𝐸 ⟩ )
61 opthg ⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ 𝐴 ) → ( ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝐷 , 𝐸 ⟩ ↔ ( 𝐵 = 𝐷 ∧ 𝐶 = 𝐸 ) ) )
62 3 4 61 syl2anc ⊢ ( 𝜑 → ( ⟨ 𝐵 , 𝐶 ⟩ = ⟨ 𝐷 , 𝐸 ⟩ ↔ ( 𝐵 = 𝐷 ∧ 𝐶 = 𝐸 ) ) )
63 60 62 mpbid ⊢ ( 𝜑 → ( 𝐵 = 𝐷 ∧ 𝐶 = 𝐸 ) )