omeu

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

		Ref	Expression
	Assertion	omeu	$⊢ (A \in On \land B \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 = B)$

Proof

Step	Hyp	Ref	Expression
1		omeulem1	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to \exists x \in On \exists y \in A (A \cdot_{𝑜} x) +_{𝑜} y = B$
2		opex	$⊢ ⟨x, y⟩ \in V$
3	2	isseti	$⊢ \exists z z = ⟨x, y⟩$
4		19.41v	$⊢ \exists z (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B) \leftrightarrow (\exists z z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)$
5	3 4	mpbiran	$⊢ \exists z (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B) \leftrightarrow (A \cdot_{𝑜} x) +_{𝑜} y = B$
6	5	rexbii	$⊢ \exists y \in A \exists z (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B) \leftrightarrow \exists y \in A (A \cdot_{𝑜} x) +_{𝑜} y = B$
7		rexcom4	$⊢ \exists y \in A \exists z (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B) \leftrightarrow \exists z \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)$
8	6 7	bitr3i	$⊢ \exists y \in A (A \cdot_{𝑜} x) +_{𝑜} y = B \leftrightarrow \exists z \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)$
9	8	rexbii	$⊢ \exists x \in On \exists y \in A (A \cdot_{𝑜} x) +_{𝑜} y = B \leftrightarrow \exists x \in On \exists z \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)$
10		rexcom4	$⊢ \exists x \in On \exists z \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B) \leftrightarrow \exists z \exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)$
11	9 10	bitri	$⊢ \exists x \in On \exists y \in A (A \cdot_{𝑜} x) +_{𝑜} y = B \leftrightarrow \exists z \exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)$
12	1 11	sylib	$⊢ (A \in On \land B \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 = B)$
13		simp2rl	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land ((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \land ((r \in On \land s \in A) \land (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))) \to z = ⟨x, y⟩$
14		simp3rl	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land ((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \land ((r \in On \land s \in A) \land (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))) \to t = ⟨r, s⟩$
15		simp2rr	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land ((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \land ((r \in On \land s \in A) \land (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))) \to (A \cdot_{𝑜} x) +_{𝑜} y = B$
16		simp3rr	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land ((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \land ((r \in On \land s \in A) \land (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))) \to (A \cdot_{𝑜} r) +_{𝑜} s = B$
17	15 16	eqtr4d	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land ((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \land ((r \in On \land s \in A) \land (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))) \to (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} r) +_{𝑜} s$
18		simp11	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land ((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \land ((r \in On \land s \in A) \land (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))) \to A \in On$
19		simp13	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land ((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \land ((r \in On \land s \in A) \land (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))) \to A \neq \emptyset$
20		simp2ll	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land ((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \land ((r \in On \land s \in A) \land (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))) \to x \in On$
21		simp2lr	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land ((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \land ((r \in On \land s \in A) \land (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))) \to y \in A$
22		simp3ll	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land ((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \land ((r \in On \land s \in A) \land (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))) \to r \in On$
23		simp3lr	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land ((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \land ((r \in On \land s \in A) \land (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))) \to s \in A$
24		omopth2	$⊢ ((A \in On \land A \neq \emptyset) \land (x \in On \land y \in A) \land (r \in On \land s \in A)) \to ((A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} r) +_{𝑜} s \leftrightarrow (x = r \land y = s))$
25	18 19 20 21 22 23 24	syl222anc	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land ((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \land ((r \in On \land s \in A) \land (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))) \to ((A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} r) +_{𝑜} s \leftrightarrow (x = r \land y = s))$
26	17 25	mpbid	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land ((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \land ((r \in On \land s \in A) \land (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))) \to (x = r \land y = s)$
27		opeq12	$⊢ (x = r \land y = s) \to ⟨x, y⟩ = ⟨r, s⟩$
28	26 27	syl	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land ((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \land ((r \in On \land s \in A) \land (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))) \to ⟨x, y⟩ = ⟨r, s⟩$
29	14 28	eqtr4d	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land ((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \land ((r \in On \land s \in A) \land (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))) \to t = ⟨x, y⟩$
30	13 29	eqtr4d	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land ((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \land ((r \in On \land s \in A) \land (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))) \to z = t$
31	30	3expia	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land ((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B))) \to (((r \in On \land s \in A) \land (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B)) \to z = t)$
32	31	exp4b	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to (((x \in On \land y \in A) \land (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \to ((r \in On \land s \in A) \to ((t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B) \to z = t)))$
33	32	expd	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to ((x \in On \land y \in A) \to ((z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B) \to ((r \in On \land s \in A) \to ((t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B) \to z = t))))$
34	33	rexlimdvv	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to (\exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B) \to ((r \in On \land s \in A) \to ((t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B) \to z = t)))$
35	34	imp	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land \exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \to ((r \in On \land s \in A) \to ((t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B) \to z = t))$
36	35	rexlimdvv	$⊢ ((A \in On \land B \in On \land A \neq \emptyset) \land \exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B)) \to (\exists r \in On \exists s \in A (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B) \to z = t)$
37	36	expimpd	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to ((\exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B) \land \exists r \in On \exists s \in A (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B)) \to z = t)$
38	37	alrimivv	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to \forall z \forall t ((\exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B) \land \exists r \in On \exists s \in A (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B)) \to z = t)$
39		opeq1	$⊢ x = r \to ⟨x, y⟩ = ⟨r, y⟩$
40	39	eqeq2d	$⊢ x = r \to (z = ⟨x, y⟩ \leftrightarrow z = ⟨r, y⟩)$
41		oveq2	$⊢ x = r \to A \cdot_{𝑜} x = A \cdot_{𝑜} r$
42	41	oveq1d	$⊢ x = r \to (A \cdot_{𝑜} x) +_{𝑜} y = (A \cdot_{𝑜} r) +_{𝑜} y$
43	42	eqeq1d	$⊢ x = r \to ((A \cdot_{𝑜} x) +_{𝑜} y = B \leftrightarrow (A \cdot_{𝑜} r) +_{𝑜} y = B)$
44	40 43	anbi12d	$⊢ x = r \to ((z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B) \leftrightarrow (z = ⟨r, y⟩ \land (A \cdot_{𝑜} r) +_{𝑜} y = B))$
45		opeq2	$⊢ y = s \to ⟨r, y⟩ = ⟨r, s⟩$
46	45	eqeq2d	$⊢ y = s \to (z = ⟨r, y⟩ \leftrightarrow z = ⟨r, s⟩)$
47		oveq2	$⊢ y = s \to (A \cdot_{𝑜} r) +_{𝑜} y = (A \cdot_{𝑜} r) +_{𝑜} s$
48	47	eqeq1d	$⊢ y = s \to ((A \cdot_{𝑜} r) +_{𝑜} y = B \leftrightarrow (A \cdot_{𝑜} r) +_{𝑜} s = B)$
49	46 48	anbi12d	$⊢ y = s \to ((z = ⟨r, y⟩ \land (A \cdot_{𝑜} r) +_{𝑜} y = B) \leftrightarrow (z = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))$
50	44 49	cbvrex2vw	$⊢ \exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B) \leftrightarrow \exists r \in On \exists s \in A (z = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B)$
51		eqeq1	$⊢ z = t \to (z = ⟨r, s⟩ \leftrightarrow t = ⟨r, s⟩)$
52	51	anbi1d	$⊢ z = t \to ((z = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B) \leftrightarrow (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))$
53	52	2rexbidv	$⊢ z = t \to (\exists r \in On \exists s \in A (z = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B) \leftrightarrow \exists r \in On \exists s \in A (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))$
54	50 53	syl5bb	$⊢ z = t \to (\exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B) \leftrightarrow \exists r \in On \exists s \in A (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B))$
55	54	eu4	$⊢ \exists! z \exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B) \leftrightarrow (\exists z \exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B) \land \forall z \forall t ((\exists x \in On \exists y \in A (z = ⟨x, y⟩ \land (A \cdot_{𝑜} x) +_{𝑜} y = B) \land \exists r \in On \exists s \in A (t = ⟨r, s⟩ \land (A \cdot_{𝑜} r) +_{𝑜} s = B)) \to z = t))$
56	12 38 55	sylanbrc	$⊢ (A \in On \land B \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 = B)$

Metamath Proof Explorer

Theorem omeu

Proof