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 𝐵 ) ) )