This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oewordi

Description: Weak ordering property of ordinal exponentiation. Lemma 3.19 of Schloeder p. 10. (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 biimtrrid ⊢ ( ( 𝐴 ∈ 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 𝐵 ) ) )