oe1m

Description: Ordinal exponentiation with a base of 1. Proposition 8.31(3) of TakeutiZaring p. 67. Lemma 2.17 of Schloeder p. 6. (Contributed by NM, 2-Jan-2005)

		Ref	Expression
	Assertion	oe1m	$⊢ A \in On \to 1_{𝑜} ↑_{𝑜} A = 1_{𝑜}$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = \emptyset \to 1_{𝑜} ↑_{𝑜} x = 1_{𝑜} ↑_{𝑜} \emptyset$
2	1	eqeq1d	$⊢ x = \emptyset \to (1_{𝑜} ↑_{𝑜} x = 1_{𝑜} \leftrightarrow 1_{𝑜} ↑_{𝑜} \emptyset = 1_{𝑜})$
3		oveq2	$⊢ x = y \to 1_{𝑜} ↑_{𝑜} x = 1_{𝑜} ↑_{𝑜} y$
4	3	eqeq1d	$⊢ x = y \to (1_{𝑜} ↑_{𝑜} x = 1_{𝑜} \leftrightarrow 1_{𝑜} ↑_{𝑜} y = 1_{𝑜})$
5		oveq2	$⊢ x = suc y \to 1_{𝑜} ↑_{𝑜} x = 1_{𝑜} ↑_{𝑜} suc y$
6	5	eqeq1d	$⊢ x = suc y \to (1_{𝑜} ↑_{𝑜} x = 1_{𝑜} \leftrightarrow 1_{𝑜} ↑_{𝑜} suc y = 1_{𝑜})$
7		oveq2	$⊢ x = A \to 1_{𝑜} ↑_{𝑜} x = 1_{𝑜} ↑_{𝑜} A$
8	7	eqeq1d	$⊢ x = A \to (1_{𝑜} ↑_{𝑜} x = 1_{𝑜} \leftrightarrow 1_{𝑜} ↑_{𝑜} A = 1_{𝑜})$
9		1on	$⊢ 1_{𝑜} \in On$
10		oe0	$⊢ 1_{𝑜} \in On \to 1_{𝑜} ↑_{𝑜} \emptyset = 1_{𝑜}$
11	9 10	ax-mp	$⊢ 1_{𝑜} ↑_{𝑜} \emptyset = 1_{𝑜}$
12		oesuc	$⊢ (1_{𝑜} \in On \land y \in On) \to 1_{𝑜} ↑_{𝑜} suc y = (1_{𝑜} ↑_{𝑜} y) \cdot_{𝑜} 1_{𝑜}$
13	9 12	mpan	$⊢ y \in On \to 1_{𝑜} ↑_{𝑜} suc y = (1_{𝑜} ↑_{𝑜} y) \cdot_{𝑜} 1_{𝑜}$
14		oveq1	$⊢ 1_{𝑜} ↑_{𝑜} y = 1_{𝑜} \to (1_{𝑜} ↑_{𝑜} y) \cdot_{𝑜} 1_{𝑜} = 1_{𝑜} \cdot_{𝑜} 1_{𝑜}$
15		om1	$⊢ 1_{𝑜} \in On \to 1_{𝑜} \cdot_{𝑜} 1_{𝑜} = 1_{𝑜}$
16	9 15	ax-mp	$⊢ 1_{𝑜} \cdot_{𝑜} 1_{𝑜} = 1_{𝑜}$
17	14 16	eqtrdi	$⊢ 1_{𝑜} ↑_{𝑜} y = 1_{𝑜} \to (1_{𝑜} ↑_{𝑜} y) \cdot_{𝑜} 1_{𝑜} = 1_{𝑜}$
18	13 17	sylan9eq	$⊢ (y \in On \land 1_{𝑜} ↑_{𝑜} y = 1_{𝑜}) \to 1_{𝑜} ↑_{𝑜} suc y = 1_{𝑜}$
19	18	ex	$⊢ y \in On \to (1_{𝑜} ↑_{𝑜} y = 1_{𝑜} \to 1_{𝑜} ↑_{𝑜} suc y = 1_{𝑜})$
20		iuneq2	$⊢ \forall y \in x 1_{𝑜} ↑_{𝑜} y = 1_{𝑜} \to ⋃_{y \in x} (1_{𝑜} ↑_{𝑜} y) = ⋃_{y \in x} 1_{𝑜}$
21		vex	$⊢ x \in V$
22		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
23		oelim	$⊢ ((1_{𝑜} \in On \land (x \in V \land Lim x)) \land \emptyset \in 1_{𝑜}) \to 1_{𝑜} ↑_{𝑜} x = ⋃_{y \in x} (1_{𝑜} ↑_{𝑜} y)$
24	22 23	mpan2	$⊢ (1_{𝑜} \in On \land (x \in V \land Lim x)) \to 1_{𝑜} ↑_{𝑜} x = ⋃_{y \in x} (1_{𝑜} ↑_{𝑜} y)$
25	9 24	mpan	$⊢ (x \in V \land Lim x) \to 1_{𝑜} ↑_{𝑜} x = ⋃_{y \in x} (1_{𝑜} ↑_{𝑜} y)$
26	21 25	mpan	$⊢ Lim x \to 1_{𝑜} ↑_{𝑜} x = ⋃_{y \in x} (1_{𝑜} ↑_{𝑜} y)$
27	26	eqeq1d	$⊢ Lim x \to (1_{𝑜} ↑_{𝑜} x = 1_{𝑜} \leftrightarrow ⋃_{y \in x} (1_{𝑜} ↑_{𝑜} y) = 1_{𝑜})$
28		0ellim	$⊢ Lim x \to \emptyset \in x$
29		ne0i	$⊢ \emptyset \in x \to x \neq \emptyset$
30		iunconst	$⊢ x \neq \emptyset \to ⋃_{y \in x} 1_{𝑜} = 1_{𝑜}$
31	28 29 30	3syl	$⊢ Lim x \to ⋃_{y \in x} 1_{𝑜} = 1_{𝑜}$
32	31	eqeq2d	$⊢ Lim x \to (⋃_{y \in x} (1_{𝑜} ↑_{𝑜} y) = ⋃_{y \in x} 1_{𝑜} \leftrightarrow ⋃_{y \in x} (1_{𝑜} ↑_{𝑜} y) = 1_{𝑜})$
33	27 32	bitr4d	$⊢ Lim x \to (1_{𝑜} ↑_{𝑜} x = 1_{𝑜} \leftrightarrow ⋃_{y \in x} (1_{𝑜} ↑_{𝑜} y) = ⋃_{y \in x} 1_{𝑜})$
34	20 33	imbitrrid	$⊢ Lim x \to (\forall y \in x 1_{𝑜} ↑_{𝑜} y = 1_{𝑜} \to 1_{𝑜} ↑_{𝑜} x = 1_{𝑜})$
35	2 4 6 8 11 19 34	tfinds	$⊢ A \in On \to 1_{𝑜} ↑_{𝑜} A = 1_{𝑜}$

Metamath Proof Explorer

Theorem oe1m

Proof