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	3	elexd	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in (On ∖ 1_{𝑜})) \to ⋃ ⋂ \{a \in On \| B \in (A ↑_{𝑜} a)\} \in V$
5		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$
6		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$
7		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))$
8		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)))$
9		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)))$
10	1 7 8 9	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)))))$
11	4 5 6 10	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))$
12		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))$
13	12	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_{𝑜})))$
14	13	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)$
15	14	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))$
16		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))$
17		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)))$
18	15 16 17	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)))$
19	18	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)))$
20		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)))$
21		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))$
22	19 20 21	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))$
23	22	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))$
24		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))$
25	23 24	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)$
26	25	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)$
27	11 26	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