MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  omeu Structured version   Visualization version   GIF version

Theorem omeu 7625
Description: The division algorithm for ordinal multiplication. (Contributed by Mario Carneiro, 28-Feb-2013.)
Assertion
Ref Expression
omeu ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃!𝑧𝑥 ∈ On ∃𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝑥,𝐵,𝑦,𝑧

Proof of Theorem omeu
Dummy variables 𝑟 𝑠 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 omeulem1 7622 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
2 opex 4903 . . . . . . . . 9 𝑥, 𝑦⟩ ∈ V
32isseti 3199 . . . . . . . 8 𝑧 𝑧 = ⟨𝑥, 𝑦
4 19.41v 1911 . . . . . . . 8 (∃𝑧(𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) ↔ (∃𝑧 𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
53, 4mpbiran 952 . . . . . . 7 (∃𝑧(𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) ↔ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
65rexbii 3036 . . . . . 6 (∃𝑦𝐴𝑧(𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) ↔ ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
7 rexcom4 3215 . . . . . 6 (∃𝑦𝐴𝑧(𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) ↔ ∃𝑧𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
86, 7bitr3i 266 . . . . 5 (∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵 ↔ ∃𝑧𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
98rexbii 3036 . . . 4 (∃𝑥 ∈ On ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵 ↔ ∃𝑥 ∈ On ∃𝑧𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
10 rexcom4 3215 . . . 4 (∃𝑥 ∈ On ∃𝑧𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) ↔ ∃𝑧𝑥 ∈ On ∃𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
119, 10bitri 264 . . 3 (∃𝑥 ∈ On ∃𝑦𝐴 ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵 ↔ ∃𝑧𝑥 ∈ On ∃𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
121, 11sylib 208 . 2 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃𝑧𝑥 ∈ On ∃𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
13 simp2rl 1128 . . . . . . . . . . 11 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) ∧ ((𝑟 ∈ On ∧ 𝑠𝐴) ∧ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))) → 𝑧 = ⟨𝑥, 𝑦⟩)
14 simp3rl 1132 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) ∧ ((𝑟 ∈ On ∧ 𝑠𝐴) ∧ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))) → 𝑡 = ⟨𝑟, 𝑠⟩)
15 simp2rr 1129 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) ∧ ((𝑟 ∈ On ∧ 𝑠𝐴) ∧ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)
16 simp3rr 1133 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) ∧ ((𝑟 ∈ On ∧ 𝑠𝐴) ∧ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))) → ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵)
1715, 16eqtr4d 2658 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) ∧ ((𝑟 ∈ On ∧ 𝑠𝐴) ∧ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))) → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = ((𝐴 ·𝑜 𝑟) +𝑜 𝑠))
18 simp11 1089 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) ∧ ((𝑟 ∈ On ∧ 𝑠𝐴) ∧ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))) → 𝐴 ∈ On)
19 simp13 1091 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) ∧ ((𝑟 ∈ On ∧ 𝑠𝐴) ∧ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))) → 𝐴 ≠ ∅)
20 simp2ll 1126 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) ∧ ((𝑟 ∈ On ∧ 𝑠𝐴) ∧ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))) → 𝑥 ∈ On)
21 simp2lr 1127 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) ∧ ((𝑟 ∈ On ∧ 𝑠𝐴) ∧ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))) → 𝑦𝐴)
22 simp3ll 1130 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) ∧ ((𝑟 ∈ On ∧ 𝑠𝐴) ∧ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))) → 𝑟 ∈ On)
23 simp3lr 1131 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) ∧ ((𝑟 ∈ On ∧ 𝑠𝐴) ∧ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))) → 𝑠𝐴)
24 omopth2 7624 . . . . . . . . . . . . . . 15 (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑟 ∈ On ∧ 𝑠𝐴)) → (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) ↔ (𝑥 = 𝑟𝑦 = 𝑠)))
2518, 19, 20, 21, 22, 23, 24syl222anc 1339 . . . . . . . . . . . . . 14 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) ∧ ((𝑟 ∈ On ∧ 𝑠𝐴) ∧ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))) → (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) ↔ (𝑥 = 𝑟𝑦 = 𝑠)))
2617, 25mpbid 222 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) ∧ ((𝑟 ∈ On ∧ 𝑠𝐴) ∧ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))) → (𝑥 = 𝑟𝑦 = 𝑠))
27 opeq12 4379 . . . . . . . . . . . . 13 ((𝑥 = 𝑟𝑦 = 𝑠) → ⟨𝑥, 𝑦⟩ = ⟨𝑟, 𝑠⟩)
2826, 27syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) ∧ ((𝑟 ∈ On ∧ 𝑠𝐴) ∧ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))) → ⟨𝑥, 𝑦⟩ = ⟨𝑟, 𝑠⟩)
2914, 28eqtr4d 2658 . . . . . . . . . . 11 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) ∧ ((𝑟 ∈ On ∧ 𝑠𝐴) ∧ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))) → 𝑡 = ⟨𝑥, 𝑦⟩)
3013, 29eqtr4d 2658 . . . . . . . . . 10 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) ∧ ((𝑟 ∈ On ∧ 𝑠𝐴) ∧ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))) → 𝑧 = 𝑡)
31303expia 1264 . . . . . . . . 9 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))) → (((𝑟 ∈ On ∧ 𝑠𝐴) ∧ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵)) → 𝑧 = 𝑡))
3231exp4b 631 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → (((𝑥 ∈ On ∧ 𝑦𝐴) ∧ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → ((𝑟 ∈ On ∧ 𝑠𝐴) → ((𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵) → 𝑧 = 𝑡))))
3332expd 452 . . . . . . 7 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ((𝑥 ∈ On ∧ 𝑦𝐴) → ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) → ((𝑟 ∈ On ∧ 𝑠𝐴) → ((𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵) → 𝑧 = 𝑡)))))
3433rexlimdvv 3032 . . . . . 6 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → (∃𝑥 ∈ On ∃𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) → ((𝑟 ∈ On ∧ 𝑠𝐴) → ((𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵) → 𝑧 = 𝑡))))
3534imp 445 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∃𝑥 ∈ On ∃𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → ((𝑟 ∈ On ∧ 𝑠𝐴) → ((𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵) → 𝑧 = 𝑡)))
3635rexlimdvv 3032 . . . 4 (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) ∧ ∃𝑥 ∈ On ∃𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵)) → (∃𝑟 ∈ On ∃𝑠𝐴 (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵) → 𝑧 = 𝑡))
3736expimpd 628 . . 3 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ((∃𝑥 ∈ On ∃𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) ∧ ∃𝑟 ∈ On ∃𝑠𝐴 (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵)) → 𝑧 = 𝑡))
3837alrimivv 1853 . 2 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∀𝑧𝑡((∃𝑥 ∈ On ∃𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) ∧ ∃𝑟 ∈ On ∃𝑠𝐴 (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵)) → 𝑧 = 𝑡))
39 opeq1 4377 . . . . . . 7 (𝑥 = 𝑟 → ⟨𝑥, 𝑦⟩ = ⟨𝑟, 𝑦⟩)
4039eqeq2d 2631 . . . . . 6 (𝑥 = 𝑟 → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ 𝑧 = ⟨𝑟, 𝑦⟩))
41 oveq2 6623 . . . . . . . 8 (𝑥 = 𝑟 → (𝐴 ·𝑜 𝑥) = (𝐴 ·𝑜 𝑟))
4241oveq1d 6630 . . . . . . 7 (𝑥 = 𝑟 → ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = ((𝐴 ·𝑜 𝑟) +𝑜 𝑦))
4342eqeq1d 2623 . . . . . 6 (𝑥 = 𝑟 → (((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵 ↔ ((𝐴 ·𝑜 𝑟) +𝑜 𝑦) = 𝐵))
4440, 43anbi12d 746 . . . . 5 (𝑥 = 𝑟 → ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) ↔ (𝑧 = ⟨𝑟, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑦) = 𝐵)))
45 opeq2 4378 . . . . . . 7 (𝑦 = 𝑠 → ⟨𝑟, 𝑦⟩ = ⟨𝑟, 𝑠⟩)
4645eqeq2d 2631 . . . . . 6 (𝑦 = 𝑠 → (𝑧 = ⟨𝑟, 𝑦⟩ ↔ 𝑧 = ⟨𝑟, 𝑠⟩))
47 oveq2 6623 . . . . . . 7 (𝑦 = 𝑠 → ((𝐴 ·𝑜 𝑟) +𝑜 𝑦) = ((𝐴 ·𝑜 𝑟) +𝑜 𝑠))
4847eqeq1d 2623 . . . . . 6 (𝑦 = 𝑠 → (((𝐴 ·𝑜 𝑟) +𝑜 𝑦) = 𝐵 ↔ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))
4946, 48anbi12d 746 . . . . 5 (𝑦 = 𝑠 → ((𝑧 = ⟨𝑟, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑦) = 𝐵) ↔ (𝑧 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵)))
5044, 49cbvrex2v 3172 . . . 4 (∃𝑥 ∈ On ∃𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) ↔ ∃𝑟 ∈ On ∃𝑠𝐴 (𝑧 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵))
51 eqeq1 2625 . . . . . 6 (𝑧 = 𝑡 → (𝑧 = ⟨𝑟, 𝑠⟩ ↔ 𝑡 = ⟨𝑟, 𝑠⟩))
5251anbi1d 740 . . . . 5 (𝑧 = 𝑡 → ((𝑧 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵) ↔ (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵)))
53522rexbidv 3052 . . . 4 (𝑧 = 𝑡 → (∃𝑟 ∈ On ∃𝑠𝐴 (𝑧 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵) ↔ ∃𝑟 ∈ On ∃𝑠𝐴 (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵)))
5450, 53syl5bb 272 . . 3 (𝑧 = 𝑡 → (∃𝑥 ∈ On ∃𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) ↔ ∃𝑟 ∈ On ∃𝑠𝐴 (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵)))
5554eu4 2517 . 2 (∃!𝑧𝑥 ∈ On ∃𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) ↔ (∃𝑧𝑥 ∈ On ∃𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) ∧ ∀𝑧𝑡((∃𝑥 ∈ On ∃𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵) ∧ ∃𝑟 ∈ On ∃𝑠𝐴 (𝑡 = ⟨𝑟, 𝑠⟩ ∧ ((𝐴 ·𝑜 𝑟) +𝑜 𝑠) = 𝐵)) → 𝑧 = 𝑡)))
5612, 38, 55sylanbrc 697 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∃!𝑧𝑥 ∈ On ∃𝑦𝐴 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036  wal 1478   = wceq 1480  wex 1701  wcel 1987  ∃!weu 2469  wne 2790  wrex 2909  c0 3897  cop 4161  Oncon0 5692  (class class class)co 6615   +𝑜 coa 7517   ·𝑜 comu 7518
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-oadd 7524  df-omul 7525
This theorem is referenced by:  oeeui  7642  omxpenlem  8021
  Copyright terms: Public domain W3C validator