Theorem oeworde

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

	Ref	Expression
Assertion	oeworde	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → 𝐵 ⊆ ( 𝐴 ↑o 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑥 = ∅ → 𝑥 = ∅ )
2		oveq2	⊢ ( 𝑥 = ∅ → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o ∅ ) )
3	1 2	sseq12d	⊢ ( 𝑥 = ∅ → ( 𝑥 ⊆ ( 𝐴 ↑o 𝑥 ) ↔ ∅ ⊆ ( 𝐴 ↑o ∅ ) ) )
4		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
5		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o 𝑦 ) )
6	4 5	sseq12d	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ ( 𝐴 ↑o 𝑥 ) ↔ 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) ) )
7		id	⊢ ( 𝑥 = suc 𝑦 → 𝑥 = suc 𝑦 )
8		oveq2	⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o suc 𝑦 ) )
9	7 8	sseq12d	⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 ⊆ ( 𝐴 ↑o 𝑥 ) ↔ suc 𝑦 ⊆ ( 𝐴 ↑o suc 𝑦 ) ) )
10		id	⊢ ( 𝑥 = 𝐵 → 𝑥 = 𝐵 )
11		oveq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o 𝐵 ) )
12	10 11	sseq12d	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ⊆ ( 𝐴 ↑o 𝑥 ) ↔ 𝐵 ⊆ ( 𝐴 ↑o 𝐵 ) ) )
13		0ss	⊢ ∅ ⊆ ( 𝐴 ↑o ∅ )
14	13	a1i	⊢ ( 𝐴 ∈ ( On ∖ 2o ) → ∅ ⊆ ( 𝐴 ↑o ∅ ) )
15		eloni	⊢ ( 𝑦 ∈ On → Ord 𝑦 )
16		eldifi	⊢ ( 𝐴 ∈ ( On ∖ 2o ) → 𝐴 ∈ On )
17		oecl	⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o 𝑦 ) ∈ On )
18	16 17	sylan	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o 𝑦 ) ∈ On )
19		eloni	⊢ ( ( 𝐴 ↑o 𝑦 ) ∈ On → Ord ( 𝐴 ↑o 𝑦 ) )
20	18 19	syl	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → Ord ( 𝐴 ↑o 𝑦 ) )
21		ordsucsssuc	⊢ ( ( Ord 𝑦 ∧ Ord ( 𝐴 ↑o 𝑦 ) ) → ( 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) ↔ suc 𝑦 ⊆ suc ( 𝐴 ↑o 𝑦 ) ) )
22	15 20 21	syl2an2	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) ↔ suc 𝑦 ⊆ suc ( 𝐴 ↑o 𝑦 ) ) )
23		suceloni	⊢ ( 𝑦 ∈ On → suc 𝑦 ∈ On )
24		oecl	⊢ ( ( 𝐴 ∈ On ∧ suc 𝑦 ∈ On ) → ( 𝐴 ↑o suc 𝑦 ) ∈ On )
25	16 23 24	syl2an	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o suc 𝑦 ) ∈ On )
26		eloni	⊢ ( ( 𝐴 ↑o suc 𝑦 ) ∈ On → Ord ( 𝐴 ↑o suc 𝑦 ) )
27	25 26	syl	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → Ord ( 𝐴 ↑o suc 𝑦 ) )
28		id	⊢ ( 𝐴 ∈ ( On ∖ 2o ) → 𝐴 ∈ ( On ∖ 2o ) )
29		vex	⊢ 𝑦 ∈ V
30	29	sucid	⊢ 𝑦 ∈ suc 𝑦
31		oeordi	⊢ ( ( suc 𝑦 ∈ On ∧ 𝐴 ∈ ( On ∖ 2o ) ) → ( 𝑦 ∈ suc 𝑦 → ( 𝐴 ↑o 𝑦 ) ∈ ( 𝐴 ↑o suc 𝑦 ) ) )
32	30 31	mpi	⊢ ( ( suc 𝑦 ∈ On ∧ 𝐴 ∈ ( On ∖ 2o ) ) → ( 𝐴 ↑o 𝑦 ) ∈ ( 𝐴 ↑o suc 𝑦 ) )
33	23 28 32	syl2anr	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( 𝐴 ↑o 𝑦 ) ∈ ( 𝐴 ↑o suc 𝑦 ) )
34		ordsucss	⊢ ( Ord ( 𝐴 ↑o suc 𝑦 ) → ( ( 𝐴 ↑o 𝑦 ) ∈ ( 𝐴 ↑o suc 𝑦 ) → suc ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) ) )
35	27 33 34	sylc	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → suc ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) )
36		sstr2	⊢ ( suc 𝑦 ⊆ suc ( 𝐴 ↑o 𝑦 ) → ( suc ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) → suc 𝑦 ⊆ ( 𝐴 ↑o suc 𝑦 ) ) )
37	35 36	syl5com	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( suc 𝑦 ⊆ suc ( 𝐴 ↑o 𝑦 ) → suc 𝑦 ⊆ ( 𝐴 ↑o suc 𝑦 ) ) )
38	22 37	sylbid	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝑦 ∈ On ) → ( 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) → suc 𝑦 ⊆ ( 𝐴 ↑o suc 𝑦 ) ) )
39	38	expcom	⊢ ( 𝑦 ∈ On → ( 𝐴 ∈ ( On ∖ 2o ) → ( 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) → suc 𝑦 ⊆ ( 𝐴 ↑o suc 𝑦 ) ) ) )
40		dif20el	⊢ ( 𝐴 ∈ ( On ∖ 2o ) → ∅ ∈ 𝐴 )
41	16 40	jca	⊢ ( 𝐴 ∈ ( On ∖ 2o ) → ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) )
42		ss2iun	⊢ ( ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) → ∪ 𝑦 ∈ 𝑥 𝑦 ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
43		limuni	⊢ ( Lim 𝑥 → 𝑥 = ∪ 𝑥 )
44		uniiun	⊢ ∪ 𝑥 = ∪ 𝑦 ∈ 𝑥 𝑦
45	43 44	eqtrdi	⊢ ( Lim 𝑥 → 𝑥 = ∪ 𝑦 ∈ 𝑥 𝑦 )
46	45	adantr	⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ) → 𝑥 = ∪ 𝑦 ∈ 𝑥 𝑦 )
47		vex	⊢ 𝑥 ∈ V
48		oelim	⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
49	47 48	mpanlr1	⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝑥 ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
50	49	anasss	⊢ ( ( 𝐴 ∈ On ∧ ( Lim 𝑥 ∧ ∅ ∈ 𝐴 ) ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
51	50	an12s	⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ) → ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) )
52	46 51	sseq12d	⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ) → ( 𝑥 ⊆ ( 𝐴 ↑o 𝑥 ) ↔ ∪ 𝑦 ∈ 𝑥 𝑦 ⊆ ∪ 𝑦 ∈ 𝑥 ( 𝐴 ↑o 𝑦 ) ) )
53	42 52	syl5ibr	⊢ ( ( Lim 𝑥 ∧ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ) → ( ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) → 𝑥 ⊆ ( 𝐴 ↑o 𝑥 ) ) )
54	53	ex	⊢ ( Lim 𝑥 → ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) → 𝑥 ⊆ ( 𝐴 ↑o 𝑥 ) ) ) )
55	41 54	syl5	⊢ ( Lim 𝑥 → ( 𝐴 ∈ ( On ∖ 2o ) → ( ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ ( 𝐴 ↑o 𝑦 ) → 𝑥 ⊆ ( 𝐴 ↑o 𝑥 ) ) ) )
56	3 6 9 12 14 39 55	tfinds3	⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ ( On ∖ 2o ) → 𝐵 ⊆ ( 𝐴 ↑o 𝐵 ) ) )
57	56	impcom	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → 𝐵 ⊆ ( 𝐴 ↑o 𝐵 ) )