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 e. On -> ( x e. On |-> ( A +o x ) ) : On -1-1-onto-> ( On \ A ) )

Proof

Step Hyp Ref Expression
1 oacl 
 |-  ( ( A e. On /\ x e. On ) -> ( A +o x ) e. On )
2 oaword1 
 |-  ( ( A e. On /\ x e. On ) -> A C_ ( A +o x ) )
3 ontri1 
 |-  ( ( A e. On /\ ( A +o x ) e. On ) -> ( A C_ ( A +o x ) <-> -. ( A +o x ) e. A ) )
4 1 3 syldan 
 |-  ( ( A e. On /\ x e. On ) -> ( A C_ ( A +o x ) <-> -. ( A +o x ) e. A ) )
5 2 4 mpbid 
 |-  ( ( A e. On /\ x e. On ) -> -. ( A +o x ) e. A )
6 1 5 eldifd 
 |-  ( ( A e. On /\ x e. On ) -> ( A +o x ) e. ( On \ A ) )
7 6 ralrimiva 
 |-  ( A e. On -> A. x e. On ( A +o x ) e. ( On \ A ) )
8 simpl 
 |-  ( ( A e. On /\ y e. ( On \ A ) ) -> A e. On )
9 eldifi 
 |-  ( y e. ( On \ A ) -> y e. On )
10 9 adantl 
 |-  ( ( A e. On /\ y e. ( On \ A ) ) -> y e. On )
11 eldifn 
 |-  ( y e. ( On \ A ) -> -. y e. A )
12 11 adantl 
 |-  ( ( A e. On /\ y e. ( On \ A ) ) -> -. y e. A )
13 ontri1 
 |-  ( ( A e. On /\ y e. On ) -> ( A C_ y <-> -. y e. A ) )
14 10 13 syldan 
 |-  ( ( A e. On /\ y e. ( On \ A ) ) -> ( A C_ y <-> -. y e. A ) )
15 12 14 mpbird 
 |-  ( ( A e. On /\ y e. ( On \ A ) ) -> A C_ y )
16 oawordeu 
 |-  ( ( ( A e. On /\ y e. On ) /\ A C_ y ) -> E! x e. On ( A +o x ) = y )
17 8 10 15 16 syl21anc 
 |-  ( ( A e. On /\ y e. ( On \ A ) ) -> E! x e. On ( A +o x ) = y )
18 eqcom 
 |-  ( ( A +o x ) = y <-> y = ( A +o x ) )
19 18 reubii 
 |-  ( E! x e. On ( A +o x ) = y <-> E! x e. On y = ( A +o x ) )
20 17 19 sylib 
 |-  ( ( A e. On /\ y e. ( On \ A ) ) -> E! x e. On y = ( A +o x ) )
21 20 ralrimiva 
 |-  ( A e. On -> A. y e. ( On \ A ) E! x e. On y = ( A +o x ) )
22 eqid 
 |-  ( x e. On |-> ( A +o x ) ) = ( x e. On |-> ( A +o x ) )
23 22 f1ompt 
 |-  ( ( x e. On |-> ( A +o x ) ) : On -1-1-onto-> ( On \ A ) <-> ( A. x e. On ( A +o x ) e. ( On \ A ) /\ A. y e. ( On \ A ) E! x e. On y = ( A +o x ) ) )
24 7 21 23 sylanbrc 
 |-  ( A e. On -> ( x e. On |-> ( A +o x ) ) : On -1-1-onto-> ( On \ A ) )