oeeu

Description: The division algorithm for ordinal exponentiation. (Contributed by Mario Carneiro, 25-May-2015)

		Ref	Expression
	Assertion	oeeu	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to \exists! w \exists x \in On \exists y \in (A ∖ 1_{𝑜}) \exists z \in (A ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\} = ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}$
2	1	oeeulem	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to (⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\} \in On \land A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\} \subseteq B \land B \in (A ↑_{𝑜} suc ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}))$
3	2	simp1d	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\} \in On$
4		fvexd	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to 1^{st} ((ι d \| \exists b \in On \exists c \in (A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) (d = ⟨b, c⟩ \land ((A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) \cdot_{𝑜} b) +_{𝑜} c = B))) \in V$
5		fvexd	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to 2^{nd} ((ι d \| \exists b \in On \exists c \in (A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) (d = ⟨b, c⟩ \land ((A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) \cdot_{𝑜} b) +_{𝑜} c = B))) \in V$
6		eqid	$⊢ (ι d \| \exists b \in On \exists c \in (A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) (d = ⟨b, c⟩ \land ((A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) \cdot_{𝑜} b) +_{𝑜} c = B)) = (ι d \| \exists b \in On \exists c \in (A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) (d = ⟨b, c⟩ \land ((A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) \cdot_{𝑜} b) +_{𝑜} c = B))$
7		eqid	$⊢ 1^{st} ((ι d \| \exists b \in On \exists c \in (A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) (d = ⟨b, c⟩ \land ((A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) \cdot_{𝑜} b) +_{𝑜} c = B))) = 1^{st} ((ι d \| \exists b \in On \exists c \in (A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) (d = ⟨b, c⟩ \land ((A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) \cdot_{𝑜} b) +_{𝑜} c = B)))$
8		eqid	$⊢ 2^{nd} ((ι d \| \exists b \in On \exists c \in (A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) (d = ⟨b, c⟩ \land ((A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) \cdot_{𝑜} b) +_{𝑜} c = B))) = 2^{nd} ((ι d \| \exists b \in On \exists c \in (A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) (d = ⟨b, c⟩ \land ((A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) \cdot_{𝑜} b) +_{𝑜} c = B)))$
9	1 6 7 8	oeeui	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to (((x \in On \land y \in (A ∖ 1_{𝑜}) \land z \in (A ↑_{𝑜} x)) \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B) \leftrightarrow (x = ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\} \land y = 1^{st} ((ι d \| \exists b \in On \exists c \in (A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) (d = ⟨b, c⟩ \land ((A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) \cdot_{𝑜} b) +_{𝑜} c = B))) \land z = 2^{nd} ((ι d \| \exists b \in On \exists c \in (A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) (d = ⟨b, c⟩ \land ((A ↑_{𝑜} ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\}) \cdot_{𝑜} b) +_{𝑜} c = B)))))$
10	3 4 5 9	euotd	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to \exists! w \exists x \exists y \exists z (w = ⟨x, y, z⟩ \land ((x \in On \land y \in (A ∖ 1_{𝑜}) \land z \in (A ↑_{𝑜} x)) \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B))$
11		df-3an	$⊢ (x \in On \land y \in (A ∖ 1_{𝑜}) \land z \in (A ↑_{𝑜} x)) \leftrightarrow ((x \in On \land y \in (A ∖ 1_{𝑜})) \land z \in (A ↑_{𝑜} x))$
12	11	biancomi	$⊢ (x \in On \land y \in (A ∖ 1_{𝑜}) \land z \in (A ↑_{𝑜} x)) \leftrightarrow (z \in (A ↑_{𝑜} x) \land (x \in On \land y \in (A ∖ 1_{𝑜})))$
13	12	anbi1i	$⊢ ((x \in On \land y \in (A ∖ 1_{𝑜}) \land z \in (A ↑_{𝑜} x)) \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B) \leftrightarrow ((z \in (A ↑_{𝑜} x) \land (x \in On \land y \in (A ∖ 1_{𝑜}))) \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)$
14	13	anbi2i	$⊢ (w = ⟨x, y, z⟩ \land ((x \in On \land y \in (A ∖ 1_{𝑜}) \land z \in (A ↑_{𝑜} x)) \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)) \leftrightarrow (w = ⟨x, y, z⟩ \land ((z \in (A ↑_{𝑜} x) \land (x \in On \land y \in (A ∖ 1_{𝑜}))) \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B))$
15		an12	$⊢ (w = ⟨x, y, z⟩ \land ((z \in (A ↑_{𝑜} x) \land (x \in On \land y \in (A ∖ 1_{𝑜}))) \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)) \leftrightarrow ((z \in (A ↑_{𝑜} x) \land (x \in On \land y \in (A ∖ 1_{𝑜}))) \land (w = ⟨x, y, z⟩ \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B))$
16		anass	$⊢ ((z \in (A ↑_{𝑜} x) \land (x \in On \land y \in (A ∖ 1_{𝑜}))) \land (w = ⟨x, y, z⟩ \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)) \leftrightarrow (z \in (A ↑_{𝑜} x) \land ((x \in On \land y \in (A ∖ 1_{𝑜})) \land (w = ⟨x, y, z⟩ \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)))$
17	14 15 16	3bitri	$⊢ (w = ⟨x, y, z⟩ \land ((x \in On \land y \in (A ∖ 1_{𝑜}) \land z \in (A ↑_{𝑜} x)) \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)) \leftrightarrow (z \in (A ↑_{𝑜} x) \land ((x \in On \land y \in (A ∖ 1_{𝑜})) \land (w = ⟨x, y, z⟩ \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)))$
18	17	exbii	$⊢ \exists z (w = ⟨x, y, z⟩ \land ((x \in On \land y \in (A ∖ 1_{𝑜}) \land z \in (A ↑_{𝑜} x)) \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)) \leftrightarrow \exists z (z \in (A ↑_{𝑜} x) \land ((x \in On \land y \in (A ∖ 1_{𝑜})) \land (w = ⟨x, y, z⟩ \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)))$
19		df-rex	$⊢ \exists z \in (A ↑_{𝑜} x) ((x \in On \land y \in (A ∖ 1_{𝑜})) \land (w = ⟨x, y, z⟩ \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)) \leftrightarrow \exists z (z \in (A ↑_{𝑜} x) \land ((x \in On \land y \in (A ∖ 1_{𝑜})) \land (w = ⟨x, y, z⟩ \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)))$
20		r19.42v	$⊢ \exists z \in (A ↑_{𝑜} x) ((x \in On \land y \in (A ∖ 1_{𝑜})) \land (w = ⟨x, y, z⟩ \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)) \leftrightarrow ((x \in On \land y \in (A ∖ 1_{𝑜})) \land \exists z \in (A ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B))$
21	18 19 20	3bitr2i	$⊢ \exists z (w = ⟨x, y, z⟩ \land ((x \in On \land y \in (A ∖ 1_{𝑜}) \land z \in (A ↑_{𝑜} x)) \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)) \leftrightarrow ((x \in On \land y \in (A ∖ 1_{𝑜})) \land \exists z \in (A ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B))$
22	21	2exbii	$⊢ \exists x \exists y \exists z (w = ⟨x, y, z⟩ \land ((x \in On \land y \in (A ∖ 1_{𝑜}) \land z \in (A ↑_{𝑜} x)) \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)) \leftrightarrow \exists x \exists y ((x \in On \land y \in (A ∖ 1_{𝑜})) \land \exists z \in (A ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B))$
23		r2ex	$⊢ \exists x \in On \exists y \in (A ∖ 1_{𝑜}) \exists z \in (A ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B) \leftrightarrow \exists x \exists y ((x \in On \land y \in (A ∖ 1_{𝑜})) \land \exists z \in (A ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B))$
24	22 23	bitr4i	$⊢ \exists x \exists y \exists z (w = ⟨x, y, z⟩ \land ((x \in On \land y \in (A ∖ 1_{𝑜}) \land z \in (A ↑_{𝑜} x)) \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)) \leftrightarrow \exists x \in On \exists y \in (A ∖ 1_{𝑜}) \exists z \in (A ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)$
25	24	eubii	$⊢ \exists! w \exists x \exists y \exists z (w = ⟨x, y, z⟩ \land ((x \in On \land y \in (A ∖ 1_{𝑜}) \land z \in (A ↑_{𝑜} x)) \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)) \leftrightarrow \exists! w \exists x \in On \exists y \in (A ∖ 1_{𝑜}) \exists z \in (A ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)$
26	10 25	sylib	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to \exists! w \exists x \in On \exists y \in (A ∖ 1_{𝑜}) \exists z \in (A ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((A ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = B)$

Metamath Proof Explorer

Theorem oeeu

Proof