Metamath Proof Explorer

Theorem oaf1o

Description: Left addition by a constant is a bijection from ordinals to ordinals greater than the constant. (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Assertion oaf1o ⊢ A ∈ On → x ∈ On ⟼ A + 𝑜 x : On ⟶ 1-1 onto On ∖ A

Proof

Step Hyp Ref Expression
1 oacl ⊢ A ∈ On ∧ x ∈ On → A + 𝑜 x ∈ On
2 oaword1 ⊢ A ∈ On ∧ x ∈ On → A ⊆ A + 𝑜 x
3 ontri1 ⊢ A ∈ On ∧ A + 𝑜 x ∈ On → A ⊆ A + 𝑜 x ↔ ¬ A + 𝑜 x ∈ A
4 1 3 syldan ⊢ A ∈ On ∧ x ∈ On → A ⊆ A + 𝑜 x ↔ ¬ A + 𝑜 x ∈ A
5 2 4 mpbid ⊢ A ∈ On ∧ x ∈ On → ¬ A + 𝑜 x ∈ A
6 1 5 eldifd ⊢ A ∈ On ∧ x ∈ On → A + 𝑜 x ∈ On ∖ A
7 6 ralrimiva ⊢ A ∈ On → ∀ x ∈ On A + 𝑜 x ∈ On ∖ A
8 simpl ⊢ A ∈ On ∧ y ∈ On ∖ A → A ∈ On
9 eldifi ⊢ y ∈ On ∖ A → y ∈ On
10 9 adantl ⊢ A ∈ On ∧ y ∈ On ∖ A → y ∈ On
11 eldifn ⊢ y ∈ On ∖ A → ¬ y ∈ A
12 11 adantl ⊢ A ∈ On ∧ y ∈ On ∖ A → ¬ y ∈ A
13 ontri1 ⊢ A ∈ On ∧ y ∈ On → A ⊆ y ↔ ¬ y ∈ A
14 10 13 syldan ⊢ A ∈ On ∧ y ∈ On ∖ A → A ⊆ y ↔ ¬ y ∈ A
15 12 14 mpbird ⊢ A ∈ On ∧ y ∈ On ∖ A → A ⊆ y
16 oawordeu ⊢ A ∈ On ∧ y ∈ On ∧ A ⊆ y → ∃! x ∈ On A + 𝑜 x = y
17 8 10 15 16 syl21anc ⊢ A ∈ On ∧ y ∈ On ∖ A → ∃! x ∈ On A + 𝑜 x = y
18 eqcom ⊢ A + 𝑜 x = y ↔ y = A + 𝑜 x
19 18 reubii ⊢ ∃! x ∈ On A + 𝑜 x = y ↔ ∃! x ∈ On y = A + 𝑜 x
20 17 19 sylib ⊢ A ∈ On ∧ y ∈ On ∖ A → ∃! x ∈ On y = A + 𝑜 x
21 20 ralrimiva ⊢ A ∈ On → ∀ y ∈ On ∖ A ∃! x ∈ On y = A + 𝑜 x
22 eqid ⊢ x ∈ On ⟼ A + 𝑜 x = x ∈ On ⟼ A + 𝑜 x
23 22 f1ompt ⊢ x ∈ On ⟼ A + 𝑜 x : On ⟶ 1-1 onto On ∖ A ↔ ∀ x ∈ On A + 𝑜 x ∈ On ∖ A ∧ ∀ y ∈ On ∖ A ∃! x ∈ On y = A + 𝑜 x
24 7 21 23 sylanbrc ⊢ A ∈ On → x ∈ On ⟼ A + 𝑜 x : On ⟶ 1-1 onto On ∖ A