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

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 ( 𝐴 ∈ On → ( 𝑥 ∈ On ↦ ( 𝐴 +o 𝑥 ) ) : On –1-1-onto→ ( On ∖ 𝐴 ) )

Proof

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