oecl

Description: Closure law for ordinal exponentiation. Remark 2.8 of Schloeder p. 5. (Contributed by NM, 1-Jan-2005) (Proof shortened by Andrew Salmon, 22-Oct-2011)

		Ref	Expression
	Assertion	oecl	$⊢ (A \in On \land B \in On) \to A ↑_{𝑜} B \in On$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ B = \emptyset \to \emptyset ↑_{𝑜} B = \emptyset ↑_{𝑜} \emptyset$
2		oe0m0	$⊢ \emptyset ↑_{𝑜} \emptyset = 1_{𝑜}$
3		1on	$⊢ 1_{𝑜} \in On$
4	2 3	eqeltri	$⊢ \emptyset ↑_{𝑜} \emptyset \in On$
5	1 4	eqeltrdi	$⊢ B = \emptyset \to \emptyset ↑_{𝑜} B \in On$
6	5	adantl	$⊢ (B \in On \land B = \emptyset) \to \emptyset ↑_{𝑜} B \in On$
7		oe0m1	$⊢ B \in On \to (\emptyset \in B \leftrightarrow \emptyset ↑_{𝑜} B = \emptyset)$
8	7	biimpa	$⊢ (B \in On \land \emptyset \in B) \to \emptyset ↑_{𝑜} B = \emptyset$
9		0elon	$⊢ \emptyset \in On$
10	8 9	eqeltrdi	$⊢ (B \in On \land \emptyset \in B) \to \emptyset ↑_{𝑜} B \in On$
11	10	adantll	$⊢ ((B \in On \land B \in On) \land \emptyset \in B) \to \emptyset ↑_{𝑜} B \in On$
12	6 11	oe0lem	$⊢ (B \in On \land B \in On) \to \emptyset ↑_{𝑜} B \in On$
13	12	anidms	$⊢ B \in On \to \emptyset ↑_{𝑜} B \in On$
14		oveq1	$⊢ A = \emptyset \to A ↑_{𝑜} B = \emptyset ↑_{𝑜} B$
15	14	eleq1d	$⊢ A = \emptyset \to (A ↑_{𝑜} B \in On \leftrightarrow \emptyset ↑_{𝑜} B \in On)$
16	13 15	imbitrrid	$⊢ A = \emptyset \to (B \in On \to A ↑_{𝑜} B \in On)$
17	16	impcom	$⊢ (B \in On \land A = \emptyset) \to A ↑_{𝑜} B \in On$
18		oveq2	$⊢ x = \emptyset \to A ↑_{𝑜} x = A ↑_{𝑜} \emptyset$
19	18	eleq1d	$⊢ x = \emptyset \to (A ↑_{𝑜} x \in On \leftrightarrow A ↑_{𝑜} \emptyset \in On)$
20		oveq2	$⊢ x = y \to A ↑_{𝑜} x = A ↑_{𝑜} y$
21	20	eleq1d	$⊢ x = y \to (A ↑_{𝑜} x \in On \leftrightarrow A ↑_{𝑜} y \in On)$
22		oveq2	$⊢ x = suc y \to A ↑_{𝑜} x = A ↑_{𝑜} suc y$
23	22	eleq1d	$⊢ x = suc y \to (A ↑_{𝑜} x \in On \leftrightarrow A ↑_{𝑜} suc y \in On)$
24		oveq2	$⊢ x = B \to A ↑_{𝑜} x = A ↑_{𝑜} B$
25	24	eleq1d	$⊢ x = B \to (A ↑_{𝑜} x \in On \leftrightarrow A ↑_{𝑜} B \in On)$
26		oe0	$⊢ A \in On \to A ↑_{𝑜} \emptyset = 1_{𝑜}$
27	26 3	eqeltrdi	$⊢ A \in On \to A ↑_{𝑜} \emptyset \in On$
28	27	adantr	$⊢ (A \in On \land \emptyset \in A) \to A ↑_{𝑜} \emptyset \in On$
29		omcl	$⊢ (A ↑_{𝑜} y \in On \land A \in On) \to (A ↑_{𝑜} y) \cdot_{𝑜} A \in On$
30	29	expcom	$⊢ A \in On \to (A ↑_{𝑜} y \in On \to (A ↑_{𝑜} y) \cdot_{𝑜} A \in On)$
31	30	adantr	$⊢ (A \in On \land y \in On) \to (A ↑_{𝑜} y \in On \to (A ↑_{𝑜} y) \cdot_{𝑜} A \in On)$
32		oesuc	$⊢ (A \in On \land y \in On) \to A ↑_{𝑜} suc y = (A ↑_{𝑜} y) \cdot_{𝑜} A$
33	32	eleq1d	$⊢ (A \in On \land y \in On) \to (A ↑_{𝑜} suc y \in On \leftrightarrow (A ↑_{𝑜} y) \cdot_{𝑜} A \in On)$
34	31 33	sylibrd	$⊢ (A \in On \land y \in On) \to (A ↑_{𝑜} y \in On \to A ↑_{𝑜} suc y \in On)$
35	34	expcom	$⊢ y \in On \to (A \in On \to (A ↑_{𝑜} y \in On \to A ↑_{𝑜} suc y \in On))$
36	35	adantrd	$⊢ y \in On \to ((A \in On \land \emptyset \in A) \to (A ↑_{𝑜} y \in On \to A ↑_{𝑜} suc y \in On))$
37		vex	$⊢ x \in V$
38		iunon	$⊢ (x \in V \land \forall y \in x A ↑_{𝑜} y \in On) \to ⋃_{y \in x} (A ↑_{𝑜} y) \in On$
39	37 38	mpan	$⊢ \forall y \in x A ↑_{𝑜} y \in On \to ⋃_{y \in x} (A ↑_{𝑜} y) \in On$
40		oelim	$⊢ ((A \in On \land (x \in V \land Lim x)) \land \emptyset \in A) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
41	37 40	mpanlr1	$⊢ ((A \in On \land Lim x) \land \emptyset \in A) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
42	41	anasss	$⊢ (A \in On \land (Lim x \land \emptyset \in A)) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
43	42	an12s	$⊢ (Lim x \land (A \in On \land \emptyset \in A)) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
44	43	eleq1d	$⊢ (Lim x \land (A \in On \land \emptyset \in A)) \to (A ↑_{𝑜} x \in On \leftrightarrow ⋃_{y \in x} (A ↑_{𝑜} y) \in On)$
45	39 44	imbitrrid	$⊢ (Lim x \land (A \in On \land \emptyset \in A)) \to (\forall y \in x A ↑_{𝑜} y \in On \to A ↑_{𝑜} x \in On)$
46	45	ex	$⊢ Lim x \to ((A \in On \land \emptyset \in A) \to (\forall y \in x A ↑_{𝑜} y \in On \to A ↑_{𝑜} x \in On))$
47	19 21 23 25 28 36 46	tfinds3	$⊢ B \in On \to ((A \in On \land \emptyset \in A) \to A ↑_{𝑜} B \in On)$
48	47	expd	$⊢ B \in On \to (A \in On \to (\emptyset \in A \to A ↑_{𝑜} B \in On))$
49	48	com12	$⊢ A \in On \to (B \in On \to (\emptyset \in A \to A ↑_{𝑜} B \in On))$
50	49	imp31	$⊢ ((A \in On \land B \in On) \land \emptyset \in A) \to A ↑_{𝑜} B \in On$
51	17 50	oe0lem	$⊢ (A \in On \land B \in On) \to A ↑_{𝑜} B \in On$

Metamath Proof Explorer

Theorem oecl

Proof