oelim2

Description: Ordinal exponentiation with a limit exponent. Part of Exercise 4.36 of Mendelson p. 250. (Contributed by NM, 6-Jan-2005)

		Ref	Expression
	Assertion	oelim2	$⊢ (A \in On \land (B \in C \land Lim B)) \to A ↑_{𝑜} B = ⋃_{x \in B ∖ 1_{𝑜}} (A ↑_{𝑜} x)$

Proof

Step	Hyp	Ref	Expression
1		limelon	$⊢ (B \in C \land Lim B) \to B \in On$
2		0ellim	$⊢ Lim B \to \emptyset \in B$
3	2	adantl	$⊢ (B \in C \land Lim B) \to \emptyset \in B$
4		oe0m1	$⊢ B \in On \to (\emptyset \in B \leftrightarrow \emptyset ↑_{𝑜} B = \emptyset)$
5	4	biimpa	$⊢ (B \in On \land \emptyset \in B) \to \emptyset ↑_{𝑜} B = \emptyset$
6	1 3 5	syl2anc	$⊢ (B \in C \land Lim B) \to \emptyset ↑_{𝑜} B = \emptyset$
7		eldif	$⊢ x \in (B ∖ 1_{𝑜}) \leftrightarrow (x \in B \land \neg x \in 1_{𝑜})$
8		limord	$⊢ Lim B \to Ord B$
9		ordelon	$⊢ (Ord B \land x \in B) \to x \in On$
10	8 9	sylan	$⊢ (Lim B \land x \in B) \to x \in On$
11		on0eln0	$⊢ x \in On \to (\emptyset \in x \leftrightarrow x \neq \emptyset)$
12		el1o	$⊢ x \in 1_{𝑜} \leftrightarrow x = \emptyset$
13	12	necon3bbii	$⊢ \neg x \in 1_{𝑜} \leftrightarrow x \neq \emptyset$
14	11 13	bitr4di	$⊢ x \in On \to (\emptyset \in x \leftrightarrow \neg x \in 1_{𝑜})$
15		oe0m1	$⊢ x \in On \to (\emptyset \in x \leftrightarrow \emptyset ↑_{𝑜} x = \emptyset)$
16	15	biimpd	$⊢ x \in On \to (\emptyset \in x \to \emptyset ↑_{𝑜} x = \emptyset)$
17	14 16	sylbird	$⊢ x \in On \to (\neg x \in 1_{𝑜} \to \emptyset ↑_{𝑜} x = \emptyset)$
18	10 17	syl	$⊢ (Lim B \land x \in B) \to (\neg x \in 1_{𝑜} \to \emptyset ↑_{𝑜} x = \emptyset)$
19	18	impr	$⊢ (Lim B \land (x \in B \land \neg x \in 1_{𝑜})) \to \emptyset ↑_{𝑜} x = \emptyset$
20	7 19	sylan2b	$⊢ (Lim B \land x \in (B ∖ 1_{𝑜})) \to \emptyset ↑_{𝑜} x = \emptyset$
21	20	iuneq2dv	$⊢ Lim B \to ⋃_{x \in B ∖ 1_{𝑜}} (\emptyset ↑_{𝑜} x) = ⋃_{x \in B ∖ 1_{𝑜}} \emptyset$
22		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
23		limsuc	$⊢ Lim B \to (\emptyset \in B \leftrightarrow suc \emptyset \in B)$
24	2 23	mpbid	$⊢ Lim B \to suc \emptyset \in B$
25	22 24	eqeltrid	$⊢ Lim B \to 1_{𝑜} \in B$
26		1on	$⊢ 1_{𝑜} \in On$
27	26	onirri	$⊢ \neg 1_{𝑜} \in 1_{𝑜}$
28		eldif	$⊢ 1_{𝑜} \in (B ∖ 1_{𝑜}) \leftrightarrow (1_{𝑜} \in B \land \neg 1_{𝑜} \in 1_{𝑜})$
29	25 27 28	sylanblrc	$⊢ Lim B \to 1_{𝑜} \in (B ∖ 1_{𝑜})$
30		ne0i	$⊢ 1_{𝑜} \in (B ∖ 1_{𝑜}) \to B ∖ 1_{𝑜} \neq \emptyset$
31		iunconst	$⊢ B ∖ 1_{𝑜} \neq \emptyset \to ⋃_{x \in B ∖ 1_{𝑜}} \emptyset = \emptyset$
32	29 30 31	3syl	$⊢ Lim B \to ⋃_{x \in B ∖ 1_{𝑜}} \emptyset = \emptyset$
33	21 32	eqtrd	$⊢ Lim B \to ⋃_{x \in B ∖ 1_{𝑜}} (\emptyset ↑_{𝑜} x) = \emptyset$
34	33	adantl	$⊢ (B \in C \land Lim B) \to ⋃_{x \in B ∖ 1_{𝑜}} (\emptyset ↑_{𝑜} x) = \emptyset$
35	6 34	eqtr4d	$⊢ (B \in C \land Lim B) \to \emptyset ↑_{𝑜} B = ⋃_{x \in B ∖ 1_{𝑜}} (\emptyset ↑_{𝑜} x)$
36		oveq1	$⊢ A = \emptyset \to A ↑_{𝑜} B = \emptyset ↑_{𝑜} B$
37		oveq1	$⊢ A = \emptyset \to A ↑_{𝑜} x = \emptyset ↑_{𝑜} x$
38	37	iuneq2d	$⊢ A = \emptyset \to ⋃_{x \in B ∖ 1_{𝑜}} (A ↑_{𝑜} x) = ⋃_{x \in B ∖ 1_{𝑜}} (\emptyset ↑_{𝑜} x)$
39	36 38	eqeq12d	$⊢ A = \emptyset \to (A ↑_{𝑜} B = ⋃_{x \in B ∖ 1_{𝑜}} (A ↑_{𝑜} x) \leftrightarrow \emptyset ↑_{𝑜} B = ⋃_{x \in B ∖ 1_{𝑜}} (\emptyset ↑_{𝑜} x))$
40	35 39	imbitrrid	$⊢ A = \emptyset \to ((B \in C \land Lim B) \to A ↑_{𝑜} B = ⋃_{x \in B ∖ 1_{𝑜}} (A ↑_{𝑜} x))$
41	40	impcom	$⊢ ((B \in C \land Lim B) \land A = \emptyset) \to A ↑_{𝑜} B = ⋃_{x \in B ∖ 1_{𝑜}} (A ↑_{𝑜} x)$
42		oelim	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to A ↑_{𝑜} B = ⋃_{y \in B} (A ↑_{𝑜} y)$
43		limsuc	$⊢ Lim B \to (y \in B \leftrightarrow suc y \in B)$
44	43	biimpa	$⊢ (Lim B \land y \in B) \to suc y \in B$
45		nsuceq0	$⊢ suc y \neq \emptyset$
46		dif1o	$⊢ suc y \in (B ∖ 1_{𝑜}) \leftrightarrow (suc y \in B \land suc y \neq \emptyset)$
47	44 45 46	sylanblrc	$⊢ (Lim B \land y \in B) \to suc y \in (B ∖ 1_{𝑜})$
48	47	ex	$⊢ Lim B \to (y \in B \to suc y \in (B ∖ 1_{𝑜}))$
49	48	ad2antlr	$⊢ ((A \in On \land Lim B) \land \emptyset \in A) \to (y \in B \to suc y \in (B ∖ 1_{𝑜}))$
50		sssucid	$⊢ y \subseteq suc y$
51		ordelon	$⊢ (Ord B \land y \in B) \to y \in On$
52	8 51	sylan	$⊢ (Lim B \land y \in B) \to y \in On$
53		onsuc	$⊢ y \in On \to suc y \in On$
54	52 53	jccir	$⊢ (Lim B \land y \in B) \to (y \in On \land suc y \in On)$
55		id	$⊢ (y \in On \land suc y \in On \land A \in On) \to (y \in On \land suc y \in On \land A \in On)$
56	55	3expa	$⊢ ((y \in On \land suc y \in On) \land A \in On) \to (y \in On \land suc y \in On \land A \in On)$
57	56	ancoms	$⊢ (A \in On \land (y \in On \land suc y \in On)) \to (y \in On \land suc y \in On \land A \in On)$
58	54 57	sylan2	$⊢ (A \in On \land (Lim B \land y \in B)) \to (y \in On \land suc y \in On \land A \in On)$
59	58	anassrs	$⊢ ((A \in On \land Lim B) \land y \in B) \to (y \in On \land suc y \in On \land A \in On)$
60		oewordi	$⊢ ((y \in On \land suc y \in On \land A \in On) \land \emptyset \in A) \to (y \subseteq suc y \to A ↑_{𝑜} y \subseteq A ↑_{𝑜} suc y)$
61	59 60	sylan	$⊢ (((A \in On \land Lim B) \land y \in B) \land \emptyset \in A) \to (y \subseteq suc y \to A ↑_{𝑜} y \subseteq A ↑_{𝑜} suc y)$
62	61	an32s	$⊢ (((A \in On \land Lim B) \land \emptyset \in A) \land y \in B) \to (y \subseteq suc y \to A ↑_{𝑜} y \subseteq A ↑_{𝑜} suc y)$
63	50 62	mpi	$⊢ (((A \in On \land Lim B) \land \emptyset \in A) \land y \in B) \to A ↑_{𝑜} y \subseteq A ↑_{𝑜} suc y$
64	63	ex	$⊢ ((A \in On \land Lim B) \land \emptyset \in A) \to (y \in B \to A ↑_{𝑜} y \subseteq A ↑_{𝑜} suc y)$
65	49 64	jcad	$⊢ ((A \in On \land Lim B) \land \emptyset \in A) \to (y \in B \to (suc y \in (B ∖ 1_{𝑜}) \land A ↑_{𝑜} y \subseteq A ↑_{𝑜} suc y))$
66		oveq2	$⊢ x = suc y \to A ↑_{𝑜} x = A ↑_{𝑜} suc y$
67	66	sseq2d	$⊢ x = suc y \to (A ↑_{𝑜} y \subseteq A ↑_{𝑜} x \leftrightarrow A ↑_{𝑜} y \subseteq A ↑_{𝑜} suc y)$
68	67	rspcev	$⊢ (suc y \in (B ∖ 1_{𝑜}) \land A ↑_{𝑜} y \subseteq A ↑_{𝑜} suc y) \to \exists x \in (B ∖ 1_{𝑜}) A ↑_{𝑜} y \subseteq A ↑_{𝑜} x$
69	65 68	syl6	$⊢ ((A \in On \land Lim B) \land \emptyset \in A) \to (y \in B \to \exists x \in (B ∖ 1_{𝑜}) A ↑_{𝑜} y \subseteq A ↑_{𝑜} x)$
70	69	ralrimiv	$⊢ ((A \in On \land Lim B) \land \emptyset \in A) \to \forall y \in B \exists x \in (B ∖ 1_{𝑜}) A ↑_{𝑜} y \subseteq A ↑_{𝑜} x$
71		iunss2	$⊢ \forall y \in B \exists x \in (B ∖ 1_{𝑜}) A ↑_{𝑜} y \subseteq A ↑_{𝑜} x \to ⋃_{y \in B} (A ↑_{𝑜} y) \subseteq ⋃_{x \in B ∖ 1_{𝑜}} (A ↑_{𝑜} x)$
72	70 71	syl	$⊢ ((A \in On \land Lim B) \land \emptyset \in A) \to ⋃_{y \in B} (A ↑_{𝑜} y) \subseteq ⋃_{x \in B ∖ 1_{𝑜}} (A ↑_{𝑜} x)$
73		difss	$⊢ B ∖ 1_{𝑜} \subseteq B$
74		iunss1	$⊢ B ∖ 1_{𝑜} \subseteq B \to ⋃_{x \in B ∖ 1_{𝑜}} (A ↑_{𝑜} x) \subseteq ⋃_{x \in B} (A ↑_{𝑜} x)$
75	73 74	ax-mp	$⊢ ⋃_{x \in B ∖ 1_{𝑜}} (A ↑_{𝑜} x) \subseteq ⋃_{x \in B} (A ↑_{𝑜} x)$
76		oveq2	$⊢ x = y \to A ↑_{𝑜} x = A ↑_{𝑜} y$
77	76	cbviunv	$⊢ ⋃_{x \in B} (A ↑_{𝑜} x) = ⋃_{y \in B} (A ↑_{𝑜} y)$
78	75 77	sseqtri	$⊢ ⋃_{x \in B ∖ 1_{𝑜}} (A ↑_{𝑜} x) \subseteq ⋃_{y \in B} (A ↑_{𝑜} y)$
79	78	a1i	$⊢ ((A \in On \land Lim B) \land \emptyset \in A) \to ⋃_{x \in B ∖ 1_{𝑜}} (A ↑_{𝑜} x) \subseteq ⋃_{y \in B} (A ↑_{𝑜} y)$
80	72 79	eqssd	$⊢ ((A \in On \land Lim B) \land \emptyset \in A) \to ⋃_{y \in B} (A ↑_{𝑜} y) = ⋃_{x \in B ∖ 1_{𝑜}} (A ↑_{𝑜} x)$
81	80	adantlrl	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to ⋃_{y \in B} (A ↑_{𝑜} y) = ⋃_{x \in B ∖ 1_{𝑜}} (A ↑_{𝑜} x)$
82	42 81	eqtrd	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to A ↑_{𝑜} B = ⋃_{x \in B ∖ 1_{𝑜}} (A ↑_{𝑜} x)$
83	41 82	oe0lem	$⊢ (A \in On \land (B \in C \land Lim B)) \to A ↑_{𝑜} B = ⋃_{x \in B ∖ 1_{𝑜}} (A ↑_{𝑜} x)$

Metamath Proof Explorer

Theorem oelim2

Proof