Metamath Proof Explorer

Theorem oeword

Description: Weak ordering property of ordinal exponentiation. (Contributed by NM, 6-Jan-2005) (Revised by Mario Carneiro, 24-May-2015)

Ref Expression
Assertion oeword ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 oeord ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝐵 ) ) )
2 oecan ⊢ ( ( 𝐶 ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐶 ↑o 𝐴 ) = ( 𝐶 ↑o 𝐵 ) ↔ 𝐴 = 𝐵 ) )
3 2 3coml ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( ( 𝐶 ↑o 𝐴 ) = ( 𝐶 ↑o 𝐵 ) ↔ 𝐴 = 𝐵 ) )
4 3 bicomd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( 𝐴 = 𝐵 ↔ ( 𝐶 ↑o 𝐴 ) = ( 𝐶 ↑o 𝐵 ) ) )
5 1 4 orbi12d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ↔ ( ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝐵 ) ∨ ( 𝐶 ↑o 𝐴 ) = ( 𝐶 ↑o 𝐵 ) ) ) )
6 onsseleq ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) )
7 6 3adant3 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) )
8 eldifi ⊢ ( 𝐶 ∈ ( On ∖ 2o ) → 𝐶 ∈ On )
9 id ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) )
10 oecl ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐶 ↑o 𝐴 ) ∈ On )
11 oecl ⊢ ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐶 ↑o 𝐵 ) ∈ On )
12 10 11 anim12dan ⊢ ( ( 𝐶 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) → ( ( 𝐶 ↑o 𝐴 ) ∈ On ∧ ( 𝐶 ↑o 𝐵 ) ∈ On ) )
13 onsseleq ⊢ ( ( ( 𝐶 ↑o 𝐴 ) ∈ On ∧ ( 𝐶 ↑o 𝐵 ) ∈ On ) → ( ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ↔ ( ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝐵 ) ∨ ( 𝐶 ↑o 𝐴 ) = ( 𝐶 ↑o 𝐵 ) ) ) )
14 12 13 syl ⊢ ( ( 𝐶 ∈ On ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) → ( ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ↔ ( ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝐵 ) ∨ ( 𝐶 ↑o 𝐴 ) = ( 𝐶 ↑o 𝐵 ) ) ) )
15 8 9 14 syl2anr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ↔ ( ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝐵 ) ∨ ( 𝐶 ↑o 𝐴 ) = ( 𝐶 ↑o 𝐵 ) ) ) )
16 15 3impa ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ↔ ( ( 𝐶 ↑o 𝐴 ) ∈ ( 𝐶 ↑o 𝐵 ) ∨ ( 𝐶 ↑o 𝐴 ) = ( 𝐶 ↑o 𝐵 ) ) ) )
17 5 7 16 3bitr4d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( On ∖ 2o ) ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐶 ↑o 𝐴 ) ⊆ ( 𝐶 ↑o 𝐵 ) ) )