oeworde

Description: Ordinal exponentiation compared to its exponent. Proposition 8.37 of TakeutiZaring p. 68. Lemma 3.20 of Schloeder p. 10. (Contributed by NM, 7-Jan-2005) (Revised by Mario Carneiro, 24-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ x = \emptyset \to x = \emptyset$
2		oveq2	$⊢ x = \emptyset \to A ↑_{𝑜} x = A ↑_{𝑜} \emptyset$
3	1 2	sseq12d	$⊢ x = \emptyset \to (x \subseteq A ↑_{𝑜} x \leftrightarrow \emptyset \subseteq A ↑_{𝑜} \emptyset)$
4		id	$⊢ x = y \to x = y$
5		oveq2	$⊢ x = y \to A ↑_{𝑜} x = A ↑_{𝑜} y$
6	4 5	sseq12d	$⊢ x = y \to (x \subseteq A ↑_{𝑜} x \leftrightarrow y \subseteq A ↑_{𝑜} y)$
7		id	$⊢ x = suc y \to x = suc y$
8		oveq2	$⊢ x = suc y \to A ↑_{𝑜} x = A ↑_{𝑜} suc y$
9	7 8	sseq12d	$⊢ x = suc y \to (x \subseteq A ↑_{𝑜} x \leftrightarrow suc y \subseteq A ↑_{𝑜} suc y)$
10		id	$⊢ x = B \to x = B$
11		oveq2	$⊢ x = B \to A ↑_{𝑜} x = A ↑_{𝑜} B$
12	10 11	sseq12d	$⊢ x = B \to (x \subseteq A ↑_{𝑜} x \leftrightarrow B \subseteq A ↑_{𝑜} B)$
13		0ss	$⊢ \emptyset \subseteq A ↑_{𝑜} \emptyset$
14	13	a1i	$⊢ A \in (On ∖ 2_{𝑜}) \to \emptyset \subseteq A ↑_{𝑜} \emptyset$
15		eloni	$⊢ y \in On \to Ord y$
16		eldifi	$⊢ A \in (On ∖ 2_{𝑜}) \to A \in On$
17		oecl	$⊢ (A \in On \land y \in On) \to A ↑_{𝑜} y \in On$
18	16 17	sylan	$⊢ (A \in (On ∖ 2_{𝑜}) \land y \in On) \to A ↑_{𝑜} y \in On$
19		eloni	$⊢ A ↑_{𝑜} y \in On \to Ord (A ↑_{𝑜} y)$
20	18 19	syl	$⊢ (A \in (On ∖ 2_{𝑜}) \land y \in On) \to Ord (A ↑_{𝑜} y)$
21		ordsucsssuc	$⊢ (Ord y \land Ord (A ↑_{𝑜} y)) \to (y \subseteq A ↑_{𝑜} y \leftrightarrow suc y \subseteq suc (A ↑_{𝑜} y))$
22	15 20 21	syl2an2	$⊢ (A \in (On ∖ 2_{𝑜}) \land y \in On) \to (y \subseteq A ↑_{𝑜} y \leftrightarrow suc y \subseteq suc (A ↑_{𝑜} y))$
23		onsuc	$⊢ y \in On \to suc y \in On$
24		oecl	$⊢ (A \in On \land suc y \in On) \to A ↑_{𝑜} suc y \in On$
25	16 23 24	syl2an	$⊢ (A \in (On ∖ 2_{𝑜}) \land y \in On) \to A ↑_{𝑜} suc y \in On$
26		eloni	$⊢ A ↑_{𝑜} suc y \in On \to Ord (A ↑_{𝑜} suc y)$
27	25 26	syl	$⊢ (A \in (On ∖ 2_{𝑜}) \land y \in On) \to Ord (A ↑_{𝑜} suc y)$
28		id	$⊢ A \in (On ∖ 2_{𝑜}) \to A \in (On ∖ 2_{𝑜})$
29		vex	$⊢ y \in V$
30	29	sucid	$⊢ y \in suc y$
31		oeordi	$⊢ (suc y \in On \land A \in (On ∖ 2_{𝑜})) \to (y \in suc y \to A ↑_{𝑜} y \in (A ↑_{𝑜} suc y))$
32	30 31	mpi	$⊢ (suc y \in On \land A \in (On ∖ 2_{𝑜})) \to A ↑_{𝑜} y \in (A ↑_{𝑜} suc y)$
33	23 28 32	syl2anr	$⊢ (A \in (On ∖ 2_{𝑜}) \land y \in On) \to A ↑_{𝑜} y \in (A ↑_{𝑜} suc y)$
34		ordsucss	$⊢ Ord (A ↑_{𝑜} suc y) \to (A ↑_{𝑜} y \in (A ↑_{𝑜} suc y) \to suc (A ↑_{𝑜} y) \subseteq A ↑_{𝑜} suc y)$
35	27 33 34	sylc	$⊢ (A \in (On ∖ 2_{𝑜}) \land y \in On) \to suc (A ↑_{𝑜} y) \subseteq A ↑_{𝑜} suc y$
36		sstr2	$⊢ suc y \subseteq suc (A ↑_{𝑜} y) \to (suc (A ↑_{𝑜} y) \subseteq A ↑_{𝑜} suc y \to suc y \subseteq A ↑_{𝑜} suc y)$
37	35 36	syl5com	$⊢ (A \in (On ∖ 2_{𝑜}) \land y \in On) \to (suc y \subseteq suc (A ↑_{𝑜} y) \to suc y \subseteq A ↑_{𝑜} suc y)$
38	22 37	sylbid	$⊢ (A \in (On ∖ 2_{𝑜}) \land y \in On) \to (y \subseteq A ↑_{𝑜} y \to suc y \subseteq A ↑_{𝑜} suc y)$
39	38	expcom	$⊢ y \in On \to (A \in (On ∖ 2_{𝑜}) \to (y \subseteq A ↑_{𝑜} y \to suc y \subseteq A ↑_{𝑜} suc y))$
40		dif20el	$⊢ A \in (On ∖ 2_{𝑜}) \to \emptyset \in A$
41	16 40	jca	$⊢ A \in (On ∖ 2_{𝑜}) \to (A \in On \land \emptyset \in A)$
42		ss2iun	$⊢ \forall y \in x y \subseteq A ↑_{𝑜} y \to ⋃_{y \in x} y \subseteq ⋃_{y \in x} (A ↑_{𝑜} y)$
43		limuni	$⊢ Lim x \to x = ⋃ x$
44		uniiun	$⊢ ⋃ x = ⋃_{y \in x} y$
45	43 44	eqtrdi	$⊢ Lim x \to x = ⋃_{y \in x} y$
46	45	adantr	$⊢ (Lim x \land (A \in On \land \emptyset \in A)) \to x = ⋃_{y \in x} y$
47		vex	$⊢ x \in V$
48		oelim	$⊢ ((A \in On \land (x \in V \land Lim x)) \land \emptyset \in A) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
49	47 48	mpanlr1	$⊢ ((A \in On \land Lim x) \land \emptyset \in A) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
50	49	anasss	$⊢ (A \in On \land (Lim x \land \emptyset \in A)) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
51	50	an12s	$⊢ (Lim x \land (A \in On \land \emptyset \in A)) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
52	46 51	sseq12d	$⊢ (Lim x \land (A \in On \land \emptyset \in A)) \to (x \subseteq A ↑_{𝑜} x \leftrightarrow ⋃_{y \in x} y \subseteq ⋃_{y \in x} (A ↑_{𝑜} y))$
53	42 52	imbitrrid	$⊢ (Lim x \land (A \in On \land \emptyset \in A)) \to (\forall y \in x y \subseteq A ↑_{𝑜} y \to x \subseteq A ↑_{𝑜} x)$
54	53	ex	$⊢ Lim x \to ((A \in On \land \emptyset \in A) \to (\forall y \in x y \subseteq A ↑_{𝑜} y \to x \subseteq A ↑_{𝑜} x))$
55	41 54	syl5	$⊢ Lim x \to (A \in (On ∖ 2_{𝑜}) \to (\forall y \in x y \subseteq A ↑_{𝑜} y \to x \subseteq A ↑_{𝑜} x))$
56	3 6 9 12 14 39 55	tfinds3	$⊢ B \in On \to (A \in (On ∖ 2_{𝑜}) \to B \subseteq A ↑_{𝑜} B)$
57	56	impcom	$⊢ (A \in (On ∖ 2_{𝑜}) \land B \in On) \to B \subseteq A ↑_{𝑜} B$

Metamath Proof Explorer

Theorem oeworde

Proof