oelimcl

Description: The ordinal exponential with a limit ordinal is a limit ordinal. (Contributed by Mario Carneiro, 29-May-2015)

		Ref	Expression
	Assertion	oelimcl	$⊢ (A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \to Lim (A ↑_{𝑜} B)$

Proof

Step	Hyp	Ref	Expression
1		eldifi	$⊢ A \in (On ∖ 2_{𝑜}) \to A \in On$
2		limelon	$⊢ (B \in C \land Lim B) \to B \in On$
3		oecl	$⊢ (A \in On \land B \in On) \to A ↑_{𝑜} B \in On$
4	1 2 3	syl2an	$⊢ (A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \to A ↑_{𝑜} B \in On$
5		eloni	$⊢ A ↑_{𝑜} B \in On \to Ord (A ↑_{𝑜} B)$
6	4 5	syl	$⊢ (A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \to Ord (A ↑_{𝑜} B)$
7	1	adantr	$⊢ (A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \to A \in On$
8	2	adantl	$⊢ (A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \to B \in On$
9		dif20el	$⊢ A \in (On ∖ 2_{𝑜}) \to \emptyset \in A$
10	9	adantr	$⊢ (A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \to \emptyset \in A$
11		oen0	$⊢ ((A \in On \land B \in On) \land \emptyset \in A) \to \emptyset \in (A ↑_{𝑜} B)$
12	7 8 10 11	syl21anc	$⊢ (A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \to \emptyset \in (A ↑_{𝑜} B)$
13		oelim2	$⊢ (A \in On \land (B \in C \land Lim B)) \to A ↑_{𝑜} B = ⋃_{y \in B ∖ 1_{𝑜}} (A ↑_{𝑜} y)$
14	1 13	sylan	$⊢ (A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \to A ↑_{𝑜} B = ⋃_{y \in B ∖ 1_{𝑜}} (A ↑_{𝑜} y)$
15	14	eleq2d	$⊢ (A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \to (x \in (A ↑_{𝑜} B) \leftrightarrow x \in ⋃_{y \in B ∖ 1_{𝑜}} (A ↑_{𝑜} y))$
16		eliun	$⊢ x \in ⋃_{y \in B ∖ 1_{𝑜}} (A ↑_{𝑜} y) \leftrightarrow \exists y \in (B ∖ 1_{𝑜}) x \in (A ↑_{𝑜} y)$
17		eldifi	$⊢ y \in (B ∖ 1_{𝑜}) \to y \in B$
18	7	adantr	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land (y \in B \land x \in (A ↑_{𝑜} y))) \to A \in On$
19	8	adantr	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land (y \in B \land x \in (A ↑_{𝑜} y))) \to B \in On$
20		simprl	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land (y \in B \land x \in (A ↑_{𝑜} y))) \to y \in B$
21		onelon	$⊢ (B \in On \land y \in B) \to y \in On$
22	19 20 21	syl2anc	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land (y \in B \land x \in (A ↑_{𝑜} y))) \to y \in On$
23		oecl	$⊢ (A \in On \land y \in On) \to A ↑_{𝑜} y \in On$
24	18 22 23	syl2anc	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land (y \in B \land x \in (A ↑_{𝑜} y))) \to A ↑_{𝑜} y \in On$
25		eloni	$⊢ A ↑_{𝑜} y \in On \to Ord (A ↑_{𝑜} y)$
26	24 25	syl	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land (y \in B \land x \in (A ↑_{𝑜} y))) \to Ord (A ↑_{𝑜} y)$
27		simprr	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land (y \in B \land x \in (A ↑_{𝑜} y))) \to x \in (A ↑_{𝑜} y)$
28		ordsucss	$⊢ Ord (A ↑_{𝑜} y) \to (x \in (A ↑_{𝑜} y) \to suc x \subseteq A ↑_{𝑜} y)$
29	26 27 28	sylc	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land (y \in B \land x \in (A ↑_{𝑜} y))) \to suc x \subseteq A ↑_{𝑜} y$
30		simpll	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land (y \in B \land x \in (A ↑_{𝑜} y))) \to A \in (On ∖ 2_{𝑜})$
31		oeordi	$⊢ (B \in On \land A \in (On ∖ 2_{𝑜})) \to (y \in B \to A ↑_{𝑜} y \in (A ↑_{𝑜} B))$
32	19 30 31	syl2anc	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land (y \in B \land x \in (A ↑_{𝑜} y))) \to (y \in B \to A ↑_{𝑜} y \in (A ↑_{𝑜} B))$
33	20 32	mpd	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land (y \in B \land x \in (A ↑_{𝑜} y))) \to A ↑_{𝑜} y \in (A ↑_{𝑜} B)$
34		onelon	$⊢ (A ↑_{𝑜} y \in On \land x \in (A ↑_{𝑜} y)) \to x \in On$
35	24 27 34	syl2anc	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land (y \in B \land x \in (A ↑_{𝑜} y))) \to x \in On$
36		suceloni	$⊢ x \in On \to suc x \in On$
37	35 36	syl	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land (y \in B \land x \in (A ↑_{𝑜} y))) \to suc x \in On$
38	4	adantr	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land (y \in B \land x \in (A ↑_{𝑜} y))) \to A ↑_{𝑜} B \in On$
39		ontr2	$⊢ (suc x \in On \land A ↑_{𝑜} B \in On) \to ((suc x \subseteq A ↑_{𝑜} y \land A ↑_{𝑜} y \in (A ↑_{𝑜} B)) \to suc x \in (A ↑_{𝑜} B))$
40	37 38 39	syl2anc	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land (y \in B \land x \in (A ↑_{𝑜} y))) \to ((suc x \subseteq A ↑_{𝑜} y \land A ↑_{𝑜} y \in (A ↑_{𝑜} B)) \to suc x \in (A ↑_{𝑜} B))$
41	29 33 40	mp2and	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land (y \in B \land x \in (A ↑_{𝑜} y))) \to suc x \in (A ↑_{𝑜} B)$
42	41	expr	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land y \in B) \to (x \in (A ↑_{𝑜} y) \to suc x \in (A ↑_{𝑜} B))$
43	17 42	sylan2	$⊢ ((A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \land y \in (B ∖ 1_{𝑜})) \to (x \in (A ↑_{𝑜} y) \to suc x \in (A ↑_{𝑜} B))$
44	43	rexlimdva	$⊢ (A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \to (\exists y \in (B ∖ 1_{𝑜}) x \in (A ↑_{𝑜} y) \to suc x \in (A ↑_{𝑜} B))$
45	16 44	syl5bi	$⊢ (A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \to (x \in ⋃_{y \in B ∖ 1_{𝑜}} (A ↑_{𝑜} y) \to suc x \in (A ↑_{𝑜} B))$
46	15 45	sylbid	$⊢ (A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \to (x \in (A ↑_{𝑜} B) \to suc x \in (A ↑_{𝑜} B))$
47	46	ralrimiv	$⊢ (A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \to \forall x \in (A ↑_{𝑜} B) suc x \in (A ↑_{𝑜} B)$
48		dflim4	$⊢ Lim (A ↑_{𝑜} B) \leftrightarrow (Ord (A ↑_{𝑜} B) \land \emptyset \in (A ↑_{𝑜} B) \land \forall x \in (A ↑_{𝑜} B) suc x \in (A ↑_{𝑜} B))$
49	6 12 47 48	syl3anbrc	$⊢ (A \in (On ∖ 2_{𝑜}) \land (B \in C \land Lim B)) \to Lim (A ↑_{𝑜} B)$

Metamath Proof Explorer

Theorem oelimcl

Proof