Metamath Proof Explorer

Theorem omeu

Description: The division algorithm for ordinal multiplication. (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion omeu ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) → ∃! 𝑧 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 omeulem1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 )
2 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
3 2 isseti ⊢ ∃ 𝑧 𝑧 = ⟨ 𝑥 , 𝑦 ⟩
4 19.41v ⊢ ( ∃ 𝑧 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ↔ ( ∃ 𝑧 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) )
5 3 4 mpbiran ⊢ ( ∃ 𝑧 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ↔ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 )
6 5 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐴 ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 )
7 rexcom4 ⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ↔ ∃ 𝑧 ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) )
8 6 7 bitr3i ⊢ ( ∃ 𝑦 ∈ 𝐴 ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ↔ ∃ 𝑧 ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) )
9 8 rexbii ⊢ ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ↔ ∃ 𝑥 ∈ On ∃ 𝑧 ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) )
10 rexcom4 ⊢ ( ∃ 𝑥 ∈ On ∃ 𝑧 ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ↔ ∃ 𝑧 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) )
11 9 10 bitri ⊢ ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ↔ ∃ 𝑧 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) )
12 1 11 sylib ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) → ∃ 𝑧 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) )
13 simp2rl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) ∧ ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) ) → 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
14 simp3rl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) ∧ ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) ) → 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ )
15 simp2rr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) ∧ ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) ) → ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 )
16 simp3rr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) ∧ ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) ) → ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 )
17 15 16 eqtr4d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) ∧ ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) ) → ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) )
18 simp11 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) ∧ ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) ) → 𝐴 ∈ On )
19 simp13 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) ∧ ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) ) → 𝐴 ≠ ∅ )
20 simp2ll ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) ∧ ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) ) → 𝑥 ∈ On )
21 simp2lr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) ∧ ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) ) → 𝑦 ∈ 𝐴 )
22 simp3ll ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) ∧ ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) ) → 𝑟 ∈ On )
23 simp3lr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) ∧ ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) ) → 𝑠 ∈ 𝐴 )
24 omopth2 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ) → ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) ↔ ( 𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ) ) )
25 18 19 20 21 22 23 24 syl222anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) ∧ ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) ) → ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) ↔ ( 𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ) ) )
26 17 25 mpbid ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) ∧ ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) ) → ( 𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ) )
27 opeq12 ⊢ ( ( 𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑟 , 𝑠 ⟩ )
28 26 27 syl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) ∧ ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑟 , 𝑠 ⟩ )
29 14 28 eqtr4d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) ∧ ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) ) → 𝑡 = ⟨ 𝑥 , 𝑦 ⟩ )
30 13 29 eqtr4d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) ∧ ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) ) → 𝑧 = 𝑡 )
31 30 3expia ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) ) → ( ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) → 𝑧 = 𝑡 ) )
32 31 exp4b ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) → ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) → ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) → 𝑧 = 𝑡 ) ) ) )
33 32 expd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) → ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) → ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) → 𝑧 = 𝑡 ) ) ) ) )
34 33 rexlimdvv ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) → ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) → 𝑧 = 𝑡 ) ) ) )
35 34 imp ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) → ( ( 𝑟 ∈ On ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) → 𝑧 = 𝑡 ) ) )
36 35 rexlimdvv ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ) → ( ∃ 𝑟 ∈ On ∃ 𝑠 ∈ 𝐴 ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) → 𝑧 = 𝑡 ) )
37 36 expimpd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) → ( ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ∧ ∃ 𝑟 ∈ On ∃ 𝑠 ∈ 𝐴 ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) → 𝑧 = 𝑡 ) )
38 37 alrimivv ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) → ∀ 𝑧 ∀ 𝑡 ( ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ∧ ∃ 𝑟 ∈ On ∃ 𝑠 ∈ 𝐴 ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) → 𝑧 = 𝑡 ) )
39 opeq1 ⊢ ( 𝑥 = 𝑟 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑟 , 𝑦 ⟩ )
40 39 eqeq2d ⊢ ( 𝑥 = 𝑟 → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑧 = ⟨ 𝑟 , 𝑦 ⟩ ) )
41 oveq2 ⊢ ( 𝑥 = 𝑟 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o 𝑟 ) )
42 41 oveq1d ⊢ ( 𝑥 = 𝑟 → ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝑟 ) +o 𝑦 ) )
43 42 eqeq1d ⊢ ( 𝑥 = 𝑟 → ( ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ↔ ( ( 𝐴 ·o 𝑟 ) +o 𝑦 ) = 𝐵 ) )
44 40 43 anbi12d ⊢ ( 𝑥 = 𝑟 → ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ↔ ( 𝑧 = ⟨ 𝑟 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑦 ) = 𝐵 ) ) )
45 opeq2 ⊢ ( 𝑦 = 𝑠 → ⟨ 𝑟 , 𝑦 ⟩ = ⟨ 𝑟 , 𝑠 ⟩ )
46 45 eqeq2d ⊢ ( 𝑦 = 𝑠 → ( 𝑧 = ⟨ 𝑟 , 𝑦 ⟩ ↔ 𝑧 = ⟨ 𝑟 , 𝑠 ⟩ ) )
47 oveq2 ⊢ ( 𝑦 = 𝑠 → ( ( 𝐴 ·o 𝑟 ) +o 𝑦 ) = ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) )
48 47 eqeq1d ⊢ ( 𝑦 = 𝑠 → ( ( ( 𝐴 ·o 𝑟 ) +o 𝑦 ) = 𝐵 ↔ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) )
49 46 48 anbi12d ⊢ ( 𝑦 = 𝑠 → ( ( 𝑧 = ⟨ 𝑟 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑦 ) = 𝐵 ) ↔ ( 𝑧 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) )
50 44 49 cbvrex2vw ⊢ ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ↔ ∃ 𝑟 ∈ On ∃ 𝑠 ∈ 𝐴 ( 𝑧 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) )
51 eqeq1 ⊢ ( 𝑧 = 𝑡 → ( 𝑧 = ⟨ 𝑟 , 𝑠 ⟩ ↔ 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ) )
52 51 anbi1d ⊢ ( 𝑧 = 𝑡 → ( ( 𝑧 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ↔ ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) )
53 52 2rexbidv ⊢ ( 𝑧 = 𝑡 → ( ∃ 𝑟 ∈ On ∃ 𝑠 ∈ 𝐴 ( 𝑧 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ↔ ∃ 𝑟 ∈ On ∃ 𝑠 ∈ 𝐴 ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) )
54 50 53 bitrid ⊢ ( 𝑧 = 𝑡 → ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ↔ ∃ 𝑟 ∈ On ∃ 𝑠 ∈ 𝐴 ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) )
55 54 eu4 ⊢ ( ∃! 𝑧 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ↔ ( ∃ 𝑧 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ∧ ∀ 𝑧 ∀ 𝑡 ( ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) ∧ ∃ 𝑟 ∈ On ∃ 𝑠 ∈ 𝐴 ( 𝑡 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ( ( 𝐴 ·o 𝑟 ) +o 𝑠 ) = 𝐵 ) ) → 𝑧 = 𝑡 ) ) )
56 12 38 55 sylanbrc ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) → ∃! 𝑧 ∃ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) = 𝐵 ) )