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 ∖ 𝐴 ) )