Metamath Proof Explorer

Theorem onelfvnef1

Description: A sufficient condition for a function on ordinals to be one-to-one. (Contributed by NM, 9-Feb-1997) Extract from tz7.48lem and generalize statement. (Revised by Matthew House, 6-Sep-2026)

Ref Expression
Assertion onelfvnef1 
|- ( ( F : A --> B /\ A C_ On /\ A. x e. A A. y e. A ( y e. x -> ( F ` x ) =/= ( F ` y ) ) ) -> F : A -1-1-> B )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( F : A --> B /\ A C_ On /\ A. x e. A A. y e. A ( y e. x -> ( F ` x ) =/= ( F ` y ) ) ) -> F : A --> B )
2 elequ12 
 |-  ( ( y = z /\ x = w ) -> ( y e. x <-> z e. w ) )
3 2 ancoms 
 |-  ( ( x = w /\ y = z ) -> ( y e. x <-> z e. w ) )
4 fveq2 
 |-  ( x = w -> ( F ` x ) = ( F ` w ) )
5 fveq2 
 |-  ( y = z -> ( F ` y ) = ( F ` z ) )
6 4 5 eqeqan12d 
 |-  ( ( x = w /\ y = z ) -> ( ( F ` x ) = ( F ` y ) <-> ( F ` w ) = ( F ` z ) ) )
7 6 necon3bid 
 |-  ( ( x = w /\ y = z ) -> ( ( F ` x ) =/= ( F ` y ) <-> ( F ` w ) =/= ( F ` z ) ) )
8 3 7 imbi12d 
 |-  ( ( x = w /\ y = z ) -> ( ( y e. x -> ( F ` x ) =/= ( F ` y ) ) <-> ( z e. w -> ( F ` w ) =/= ( F ` z ) ) ) )
9 8 rspc2gv 
 |-  ( ( w e. A /\ z e. A ) -> ( A. x e. A A. y e. A ( y e. x -> ( F ` x ) =/= ( F ` y ) ) -> ( z e. w -> ( F ` w ) =/= ( F ` z ) ) ) )
10 9 ancoms 
 |-  ( ( z e. A /\ w e. A ) -> ( A. x e. A A. y e. A ( y e. x -> ( F ` x ) =/= ( F ` y ) ) -> ( z e. w -> ( F ` w ) =/= ( F ` z ) ) ) )
11 10 impcom 
 |-  ( ( A. x e. A A. y e. A ( y e. x -> ( F ` x ) =/= ( F ` y ) ) /\ ( z e. A /\ w e. A ) ) -> ( z e. w -> ( F ` w ) =/= ( F ` z ) ) )
12 necom 
 |-  ( ( F ` z ) =/= ( F ` w ) <-> ( F ` w ) =/= ( F ` z ) )
13 11 12 imbitrrdi 
 |-  ( ( A. x e. A A. y e. A ( y e. x -> ( F ` x ) =/= ( F ` y ) ) /\ ( z e. A /\ w e. A ) ) -> ( z e. w -> ( F ` z ) =/= ( F ` w ) ) )
14 elequ12 
 |-  ( ( y = w /\ x = z ) -> ( y e. x <-> w e. z ) )
15 14 ancoms 
 |-  ( ( x = z /\ y = w ) -> ( y e. x <-> w e. z ) )
16 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
17 fveq2 
 |-  ( y = w -> ( F ` y ) = ( F ` w ) )
18 16 17 eqeqan12d 
 |-  ( ( x = z /\ y = w ) -> ( ( F ` x ) = ( F ` y ) <-> ( F ` z ) = ( F ` w ) ) )
19 18 necon3bid 
 |-  ( ( x = z /\ y = w ) -> ( ( F ` x ) =/= ( F ` y ) <-> ( F ` z ) =/= ( F ` w ) ) )
20 15 19 imbi12d 
 |-  ( ( x = z /\ y = w ) -> ( ( y e. x -> ( F ` x ) =/= ( F ` y ) ) <-> ( w e. z -> ( F ` z ) =/= ( F ` w ) ) ) )
21 20 rspc2gv 
 |-  ( ( z e. A /\ w e. A ) -> ( A. x e. A A. y e. A ( y e. x -> ( F ` x ) =/= ( F ` y ) ) -> ( w e. z -> ( F ` z ) =/= ( F ` w ) ) ) )
22 21 impcom 
 |-  ( ( A. x e. A A. y e. A ( y e. x -> ( F ` x ) =/= ( F ` y ) ) /\ ( z e. A /\ w e. A ) ) -> ( w e. z -> ( F ` z ) =/= ( F ` w ) ) )
23 13 22 jaod 
 |-  ( ( A. x e. A A. y e. A ( y e. x -> ( F ` x ) =/= ( F ` y ) ) /\ ( z e. A /\ w e. A ) ) -> ( ( z e. w \/ w e. z ) -> ( F ` z ) =/= ( F ` w ) ) )
24 23 necon2bd 
 |-  ( ( A. x e. A A. y e. A ( y e. x -> ( F ` x ) =/= ( F ` y ) ) /\ ( z e. A /\ w e. A ) ) -> ( ( F ` z ) = ( F ` w ) -> -. ( z e. w \/ w e. z ) ) )
25 24 3ad2antl3 
 |-  ( ( ( F : A --> B /\ A C_ On /\ A. x e. A A. y e. A ( y e. x -> ( F ` x ) =/= ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( ( F ` z ) = ( F ` w ) -> -. ( z e. w \/ w e. z ) ) )
26 ssel2 
 |-  ( ( A C_ On /\ z e. A ) -> z e. On )
27 ssel2 
 |-  ( ( A C_ On /\ w e. A ) -> w e. On )
28 eloni 
 |-  ( z e. On -> Ord z )
29 eloni 
 |-  ( w e. On -> Ord w )
30 ordtri3 
 |-  ( ( Ord z /\ Ord w ) -> ( z = w <-> -. ( z e. w \/ w e. z ) ) )
31 28 29 30 syl2an 
 |-  ( ( z e. On /\ w e. On ) -> ( z = w <-> -. ( z e. w \/ w e. z ) ) )
32 26 27 31 syl2an 
 |-  ( ( ( A C_ On /\ z e. A ) /\ ( A C_ On /\ w e. A ) ) -> ( z = w <-> -. ( z e. w \/ w e. z ) ) )
33 32 anandis 
 |-  ( ( A C_ On /\ ( z e. A /\ w e. A ) ) -> ( z = w <-> -. ( z e. w \/ w e. z ) ) )
34 33 3ad2antl2 
 |-  ( ( ( F : A --> B /\ A C_ On /\ A. x e. A A. y e. A ( y e. x -> ( F ` x ) =/= ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( z = w <-> -. ( z e. w \/ w e. z ) ) )
35 25 34 sylibrd 
 |-  ( ( ( F : A --> B /\ A C_ On /\ A. x e. A A. y e. A ( y e. x -> ( F ` x ) =/= ( F ` y ) ) ) /\ ( z e. A /\ w e. A ) ) -> ( ( F ` z ) = ( F ` w ) -> z = w ) )
36 35 ralrimivva 
 |-  ( ( F : A --> B /\ A C_ On /\ A. x e. A A. y e. A ( y e. x -> ( F ` x ) =/= ( F ` y ) ) ) -> A. z e. A A. w e. A ( ( F ` z ) = ( F ` w ) -> z = w ) )
37 dff13 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. z e. A A. w e. A ( ( F ` z ) = ( F ` w ) -> z = w ) ) )
38 1 36 37 sylanbrc 
 |-  ( ( F : A --> B /\ A C_ On /\ A. x e. A A. y e. A ( y e. x -> ( F ` x ) =/= ( F ` y ) ) ) -> F : A -1-1-> B )