oen0

Description: Ordinal exponentiation with a nonzero mantissa is nonzero. Proposition 8.32 of TakeutiZaring p. 67. (Contributed by NM, 4-Jan-2005)

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = \emptyset \to A ↑_{𝑜} x = A ↑_{𝑜} \emptyset$
2	1	eleq2d	$⊢ x = \emptyset \to (\emptyset \in (A ↑_{𝑜} x) \leftrightarrow \emptyset \in (A ↑_{𝑜} \emptyset))$
3		oveq2	$⊢ x = y \to A ↑_{𝑜} x = A ↑_{𝑜} y$
4	3	eleq2d	$⊢ x = y \to (\emptyset \in (A ↑_{𝑜} x) \leftrightarrow \emptyset \in (A ↑_{𝑜} y))$
5		oveq2	$⊢ x = suc y \to A ↑_{𝑜} x = A ↑_{𝑜} suc y$
6	5	eleq2d	$⊢ x = suc y \to (\emptyset \in (A ↑_{𝑜} x) \leftrightarrow \emptyset \in (A ↑_{𝑜} suc y))$
7		oveq2	$⊢ x = B \to A ↑_{𝑜} x = A ↑_{𝑜} B$
8	7	eleq2d	$⊢ x = B \to (\emptyset \in (A ↑_{𝑜} x) \leftrightarrow \emptyset \in (A ↑_{𝑜} B))$
9		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
10		oe0	$⊢ A \in On \to A ↑_{𝑜} \emptyset = 1_{𝑜}$
11	9 10	eleqtrrid	$⊢ A \in On \to \emptyset \in (A ↑_{𝑜} \emptyset)$
12	11	adantr	$⊢ (A \in On \land \emptyset \in A) \to \emptyset \in (A ↑_{𝑜} \emptyset)$
13		oecl	$⊢ (A \in On \land y \in On) \to A ↑_{𝑜} y \in On$
14		omordi	$⊢ ((A \in On \land A ↑_{𝑜} y \in On) \land \emptyset \in (A ↑_{𝑜} y)) \to (\emptyset \in A \to (A ↑_{𝑜} y) \cdot_{𝑜} \emptyset \in ((A ↑_{𝑜} y) \cdot_{𝑜} A))$
15		om0	$⊢ A ↑_{𝑜} y \in On \to (A ↑_{𝑜} y) \cdot_{𝑜} \emptyset = \emptyset$
16	15	eleq1d	$⊢ A ↑_{𝑜} y \in On \to ((A ↑_{𝑜} y) \cdot_{𝑜} \emptyset \in ((A ↑_{𝑜} y) \cdot_{𝑜} A) \leftrightarrow \emptyset \in ((A ↑_{𝑜} y) \cdot_{𝑜} A))$
17	16	ad2antlr	$⊢ ((A \in On \land A ↑_{𝑜} y \in On) \land \emptyset \in (A ↑_{𝑜} y)) \to ((A ↑_{𝑜} y) \cdot_{𝑜} \emptyset \in ((A ↑_{𝑜} y) \cdot_{𝑜} A) \leftrightarrow \emptyset \in ((A ↑_{𝑜} y) \cdot_{𝑜} A))$
18	14 17	sylibd	$⊢ ((A \in On \land A ↑_{𝑜} y \in On) \land \emptyset \in (A ↑_{𝑜} y)) \to (\emptyset \in A \to \emptyset \in ((A ↑_{𝑜} y) \cdot_{𝑜} A))$
19	13 18	syldanl	$⊢ ((A \in On \land y \in On) \land \emptyset \in (A ↑_{𝑜} y)) \to (\emptyset \in A \to \emptyset \in ((A ↑_{𝑜} y) \cdot_{𝑜} A))$
20		oesuc	$⊢ (A \in On \land y \in On) \to A ↑_{𝑜} suc y = (A ↑_{𝑜} y) \cdot_{𝑜} A$
21	20	eleq2d	$⊢ (A \in On \land y \in On) \to (\emptyset \in (A ↑_{𝑜} suc y) \leftrightarrow \emptyset \in ((A ↑_{𝑜} y) \cdot_{𝑜} A))$
22	21	adantr	$⊢ ((A \in On \land y \in On) \land \emptyset \in (A ↑_{𝑜} y)) \to (\emptyset \in (A ↑_{𝑜} suc y) \leftrightarrow \emptyset \in ((A ↑_{𝑜} y) \cdot_{𝑜} A))$
23	19 22	sylibrd	$⊢ ((A \in On \land y \in On) \land \emptyset \in (A ↑_{𝑜} y)) \to (\emptyset \in A \to \emptyset \in (A ↑_{𝑜} suc y))$
24	23	exp31	$⊢ A \in On \to (y \in On \to (\emptyset \in (A ↑_{𝑜} y) \to (\emptyset \in A \to \emptyset \in (A ↑_{𝑜} suc y))))$
25	24	com12	$⊢ y \in On \to (A \in On \to (\emptyset \in (A ↑_{𝑜} y) \to (\emptyset \in A \to \emptyset \in (A ↑_{𝑜} suc y))))$
26	25	com34	$⊢ y \in On \to (A \in On \to (\emptyset \in A \to (\emptyset \in (A ↑_{𝑜} y) \to \emptyset \in (A ↑_{𝑜} suc y))))$
27	26	impd	$⊢ y \in On \to ((A \in On \land \emptyset \in A) \to (\emptyset \in (A ↑_{𝑜} y) \to \emptyset \in (A ↑_{𝑜} suc y)))$
28		0ellim	$⊢ Lim x \to \emptyset \in x$
29		eqimss2	$⊢ A ↑_{𝑜} \emptyset = 1_{𝑜} \to 1_{𝑜} \subseteq A ↑_{𝑜} \emptyset$
30	10 29	syl	$⊢ A \in On \to 1_{𝑜} \subseteq A ↑_{𝑜} \emptyset$
31		oveq2	$⊢ y = \emptyset \to A ↑_{𝑜} y = A ↑_{𝑜} \emptyset$
32	31	sseq2d	$⊢ y = \emptyset \to (1_{𝑜} \subseteq A ↑_{𝑜} y \leftrightarrow 1_{𝑜} \subseteq A ↑_{𝑜} \emptyset)$
33	32	rspcev	$⊢ (\emptyset \in x \land 1_{𝑜} \subseteq A ↑_{𝑜} \emptyset) \to \exists y \in x 1_{𝑜} \subseteq A ↑_{𝑜} y$
34	28 30 33	syl2an	$⊢ (Lim x \land A \in On) \to \exists y \in x 1_{𝑜} \subseteq A ↑_{𝑜} y$
35		ssiun	$⊢ \exists y \in x 1_{𝑜} \subseteq A ↑_{𝑜} y \to 1_{𝑜} \subseteq ⋃_{y \in x} (A ↑_{𝑜} y)$
36	34 35	syl	$⊢ (Lim x \land A \in On) \to 1_{𝑜} \subseteq ⋃_{y \in x} (A ↑_{𝑜} y)$
37	36	adantrr	$⊢ (Lim x \land (A \in On \land \emptyset \in A)) \to 1_{𝑜} \subseteq ⋃_{y \in x} (A ↑_{𝑜} y)$
38		vex	$⊢ x \in V$
39		oelim	$⊢ ((A \in On \land (x \in V \land Lim x)) \land \emptyset \in A) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
40	38 39	mpanlr1	$⊢ ((A \in On \land Lim x) \land \emptyset \in A) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
41	40	anasss	$⊢ (A \in On \land (Lim x \land \emptyset \in A)) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
42	41	an12s	$⊢ (Lim x \land (A \in On \land \emptyset \in A)) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
43	37 42	sseqtrrd	$⊢ (Lim x \land (A \in On \land \emptyset \in A)) \to 1_{𝑜} \subseteq A ↑_{𝑜} x$
44		limelon	$⊢ (x \in V \land Lim x) \to x \in On$
45	38 44	mpan	$⊢ Lim x \to x \in On$
46		oecl	$⊢ (A \in On \land x \in On) \to A ↑_{𝑜} x \in On$
47	46	ancoms	$⊢ (x \in On \land A \in On) \to A ↑_{𝑜} x \in On$
48	45 47	sylan	$⊢ (Lim x \land A \in On) \to A ↑_{𝑜} x \in On$
49		eloni	$⊢ A ↑_{𝑜} x \in On \to Ord (A ↑_{𝑜} x)$
50		ordgt0ge1	$⊢ Ord (A ↑_{𝑜} x) \to (\emptyset \in (A ↑_{𝑜} x) \leftrightarrow 1_{𝑜} \subseteq A ↑_{𝑜} x)$
51	48 49 50	3syl	$⊢ (Lim x \land A \in On) \to (\emptyset \in (A ↑_{𝑜} x) \leftrightarrow 1_{𝑜} \subseteq A ↑_{𝑜} x)$
52	51	adantrr	$⊢ (Lim x \land (A \in On \land \emptyset \in A)) \to (\emptyset \in (A ↑_{𝑜} x) \leftrightarrow 1_{𝑜} \subseteq A ↑_{𝑜} x)$
53	43 52	mpbird	$⊢ (Lim x \land (A \in On \land \emptyset \in A)) \to \emptyset \in (A ↑_{𝑜} x)$
54	53	ex	$⊢ Lim x \to ((A \in On \land \emptyset \in A) \to \emptyset \in (A ↑_{𝑜} x))$
55	54	a1dd	$⊢ Lim x \to ((A \in On \land \emptyset \in A) \to (\forall y \in x \emptyset \in (A ↑_{𝑜} y) \to \emptyset \in (A ↑_{𝑜} x)))$
56	2 4 6 8 12 27 55	tfinds3	$⊢ B \in On \to ((A \in On \land \emptyset \in A) \to \emptyset \in (A ↑_{𝑜} B))$
57	56	expd	$⊢ B \in On \to (A \in On \to (\emptyset \in A \to \emptyset \in (A ↑_{𝑜} B)))$
58	57	com12	$⊢ A \in On \to (B \in On \to (\emptyset \in A \to \emptyset \in (A ↑_{𝑜} B)))$
59	58	imp31	$⊢ ((A \in On \land B \in On) \land \emptyset \in A) \to \emptyset \in (A ↑_{𝑜} B)$

Metamath Proof Explorer

Theorem oen0

Proof