Theorem oewordi

Description: Weak ordering property of ordinal exponentiation. (Contributed by NM, 6-Jan-2005)

	Ref	Expression
Assertion	oewordi	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ⊆ 𝐵 → ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eloni	⊢ ( 𝐶 ∈ On → Ord 𝐶 )
2		ordgt0ge1	⊢ ( Ord 𝐶 → ( ∅ ∈ 𝐶 ↔ 1o ⊆ 𝐶 ) )
3	1 2	syl	⊢ ( 𝐶 ∈ On → ( ∅ ∈ 𝐶 ↔ 1o ⊆ 𝐶 ) )
4		1on	⊢ 1o ∈ On
5		onsseleq	⊢ ( ( 1o ∈ On ∧ 𝐶 ∈ On ) → ( 1o ⊆ 𝐶 ↔ ( 1o ∈ 𝐶 ∨ 1o = 𝐶 ) ) )
6	4 5	mpan	⊢ ( 𝐶 ∈ On → ( 1o ⊆ 𝐶 ↔ ( 1o ∈ 𝐶 ∨ 1o = 𝐶 ) ) )
7	3 6	bitrd	⊢ ( 𝐶 ∈ On → ( ∅ ∈ 𝐶 ↔ ( 1o ∈ 𝐶 ∨ 1o = 𝐶 ) ) )
8	7	3ad2ant3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∅ ∈ 𝐶 ↔ ( 1o ∈ 𝐶 ∨ 1o = 𝐶 ) ) )
9		ondif2	⊢ ( 𝐶 ∈ ( On ∖ 2o ) ↔ ( 𝐶 ∈ On ∧ 1o ∈ 𝐶 ) )
10		oeword	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ) )
11	10	biimpd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( 𝐴 ⊆ 𝐵 → ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ) )
12	11	3expia	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐶 ∈ ( On ∖ 2o ) → ( 𝐴 ⊆ 𝐵 → ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ) ) )
13	9 12	syl5bir	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐶 ∈ On ∧ 1o ∈ 𝐶 ) → ( 𝐴 ⊆ 𝐵 → ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ) ) )
14	13	expd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐶 ∈ On → ( 1o ∈ 𝐶 → ( 𝐴 ⊆ 𝐵 → ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ) ) ) )
15	14	3impia	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 1o ∈ 𝐶 → ( 𝐴 ⊆ 𝐵 → ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ) ) )
16		oe1m	⊢ ( 𝐴 ∈ On → ( 1o ↑o 𝐴 ) = 1o )
17	16	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 1o ↑o 𝐴 ) = 1o )
18		oe1m	⊢ ( 𝐵 ∈ On → ( 1o ↑o 𝐵 ) = 1o )
19	18	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 1o ↑o 𝐵 ) = 1o )
20	17 19	eqtr4d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 1o ↑o 𝐴 ) = ( 1o ↑o 𝐵 ) )
21		eqimss	⊢ ( ( 1o ↑o 𝐴 ) = ( 1o ↑o 𝐵 ) → ( 1o ↑o 𝐴 ) ⊆ ( 1o ↑o 𝐵 ) )
22	20 21	syl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 1o ↑o 𝐴 ) ⊆ ( 1o ↑o 𝐵 ) )
23		oveq1	⊢ ( 1o = 𝐶 → ( 1o ↑o 𝐴 ) = ( 𝐶 ↑o 𝐴 ) )
24		oveq1	⊢ ( 1o = 𝐶 → ( 1o ↑o 𝐵 ) = ( 𝐶 ↑o 𝐵 ) )
25	23 24	sseq12d	⊢ ( 1o = 𝐶 → ( ( 1o ↑o 𝐴 ) ⊆ ( 1o ↑o 𝐵 ) ↔ ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ) )
26	22 25	syl5ibcom	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 1o = 𝐶 → ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ) )
27	26	3adant3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 1o = 𝐶 → ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ) )
28	27	a1dd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 1o = 𝐶 → ( 𝐴 ⊆ 𝐵 → ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ) ) )
29	15 28	jaod	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 1o ∈ 𝐶 ∨ 1o = 𝐶 ) → ( 𝐴 ⊆ 𝐵 → ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ) ) )
30	8 29	sylbid	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∅ ∈ 𝐶 → ( 𝐴 ⊆ 𝐵 → ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ) ) )
31	30	imp	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ⊆ 𝐵 → ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ) )