Metamath Proof Explorer

Theorem smo11

Description: A strictly monotone ordinal function is one-to-one. (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion smo11 
|- ( ( F : A --> B /\ Smo F ) -> F : A -1-1-> B )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( F : A --> B /\ Smo F ) -> F : A --> B )
2 ffn 
 |-  ( F : A --> B -> F Fn A )
3 smodm2 
 |-  ( ( F Fn A /\ Smo F ) -> Ord A )
4 ordelord 
 |-  ( ( Ord A /\ z e. A ) -> Ord z )
5 4 ex 
 |-  ( Ord A -> ( z e. A -> Ord z ) )
6 3 5 syl 
 |-  ( ( F Fn A /\ Smo F ) -> ( z e. A -> Ord z ) )
7 ordelord 
 |-  ( ( Ord A /\ w e. A ) -> Ord w )
8 7 ex 
 |-  ( Ord A -> ( w e. A -> Ord w ) )
9 3 8 syl 
 |-  ( ( F Fn A /\ Smo F ) -> ( w e. A -> Ord w ) )
10 6 9 anim12d 
 |-  ( ( F Fn A /\ Smo F ) -> ( ( z e. A /\ w e. A ) -> ( Ord z /\ Ord w ) ) )
11 ordtri3or 
 |-  ( ( Ord z /\ Ord w ) -> ( z e. w \/ z = w \/ w e. z ) )
12 simp1rr 
 |-  ( ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) /\ z e. w /\ ( F ` z ) = ( F ` w ) ) -> w e. A )
13 smoel2 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( x e. A /\ y e. x ) ) -> ( F ` y ) e. ( F ` x ) )
14 13 ralrimivva 
 |-  ( ( F Fn A /\ Smo F ) -> A. x e. A A. y e. x ( F ` y ) e. ( F ` x ) )
15 14 adantr 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) -> A. x e. A A. y e. x ( F ` y ) e. ( F ` x ) )
16 15 3ad2ant1 
 |-  ( ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) /\ z e. w /\ ( F ` z ) = ( F ` w ) ) -> A. x e. A A. y e. x ( F ` y ) e. ( F ` x ) )
17 simp2 
 |-  ( ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) /\ z e. w /\ ( F ` z ) = ( F ` w ) ) -> z e. w )
18 simp3 
 |-  ( ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) /\ z e. w /\ ( F ` z ) = ( F ` w ) ) -> ( F ` z ) = ( F ` w ) )
19 fveq2 
 |-  ( x = w -> ( F ` x ) = ( F ` w ) )
20 19 eleq2d 
 |-  ( x = w -> ( ( F ` y ) e. ( F ` x ) <-> ( F ` y ) e. ( F ` w ) ) )
21 20 raleqbi1dv 
 |-  ( x = w -> ( A. y e. x ( F ` y ) e. ( F ` x ) <-> A. y e. w ( F ` y ) e. ( F ` w ) ) )
22 21 rspcv 
 |-  ( w e. A -> ( A. x e. A A. y e. x ( F ` y ) e. ( F ` x ) -> A. y e. w ( F ` y ) e. ( F ` w ) ) )
23 fveq2 
 |-  ( y = z -> ( F ` y ) = ( F ` z ) )
24 23 eleq1d 
 |-  ( y = z -> ( ( F ` y ) e. ( F ` w ) <-> ( F ` z ) e. ( F ` w ) ) )
25 24 rspccv 
 |-  ( A. y e. w ( F ` y ) e. ( F ` w ) -> ( z e. w -> ( F ` z ) e. ( F ` w ) ) )
26 22 25 syl6 
 |-  ( w e. A -> ( A. x e. A A. y e. x ( F ` y ) e. ( F ` x ) -> ( z e. w -> ( F ` z ) e. ( F ` w ) ) ) )
27 26 3imp 
 |-  ( ( w e. A /\ A. x e. A A. y e. x ( F ` y ) e. ( F ` x ) /\ z e. w ) -> ( F ` z ) e. ( F ` w ) )
28 eleq1 
 |-  ( ( F ` z ) = ( F ` w ) -> ( ( F ` z ) e. ( F ` w ) <-> ( F ` w ) e. ( F ` w ) ) )
29 28 biimpac 
 |-  ( ( ( F ` z ) e. ( F ` w ) /\ ( F ` z ) = ( F ` w ) ) -> ( F ` w ) e. ( F ` w ) )
30 27 29 sylan 
 |-  ( ( ( w e. A /\ A. x e. A A. y e. x ( F ` y ) e. ( F ` x ) /\ z e. w ) /\ ( F ` z ) = ( F ` w ) ) -> ( F ` w ) e. ( F ` w ) )
31 12 16 17 18 30 syl31anc 
 |-  ( ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) /\ z e. w /\ ( F ` z ) = ( F ` w ) ) -> ( F ` w ) e. ( F ` w ) )
32 smofvon2 
 |-  ( Smo F -> ( F ` w ) e. On )
33 eloni 
 |-  ( ( F ` w ) e. On -> Ord ( F ` w ) )
34 ordirr 
 |-  ( Ord ( F ` w ) -> -. ( F ` w ) e. ( F ` w ) )
35 32 33 34 3syl 
 |-  ( Smo F -> -. ( F ` w ) e. ( F ` w ) )
36 35 ad2antlr 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) -> -. ( F ` w ) e. ( F ` w ) )
37 36 3ad2ant1 
 |-  ( ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) /\ z e. w /\ ( F ` z ) = ( F ` w ) ) -> -. ( F ` w ) e. ( F ` w ) )
38 31 37 pm2.21dd 
 |-  ( ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) /\ z e. w /\ ( F ` z ) = ( F ` w ) ) -> z = w )
39 38 3exp 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) -> ( z e. w -> ( ( F ` z ) = ( F ` w ) -> z = w ) ) )
40 ax-1 
 |-  ( z = w -> ( ( F ` z ) = ( F ` w ) -> z = w ) )
41 40 a1i 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) -> ( z = w -> ( ( F ` z ) = ( F ` w ) -> z = w ) ) )
42 simp1rl 
 |-  ( ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) /\ w e. z /\ ( F ` z ) = ( F ` w ) ) -> z e. A )
43 15 3ad2ant1 
 |-  ( ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) /\ w e. z /\ ( F ` z ) = ( F ` w ) ) -> A. x e. A A. y e. x ( F ` y ) e. ( F ` x ) )
44 simp2 
 |-  ( ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) /\ w e. z /\ ( F ` z ) = ( F ` w ) ) -> w e. z )
45 simp3 
 |-  ( ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) /\ w e. z /\ ( F ` z ) = ( F ` w ) ) -> ( F ` z ) = ( F ` w ) )
46 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
47 46 eleq2d 
 |-  ( x = z -> ( ( F ` y ) e. ( F ` x ) <-> ( F ` y ) e. ( F ` z ) ) )
48 47 raleqbi1dv 
 |-  ( x = z -> ( A. y e. x ( F ` y ) e. ( F ` x ) <-> A. y e. z ( F ` y ) e. ( F ` z ) ) )
49 48 rspcv 
 |-  ( z e. A -> ( A. x e. A A. y e. x ( F ` y ) e. ( F ` x ) -> A. y e. z ( F ` y ) e. ( F ` z ) ) )
50 fveq2 
 |-  ( y = w -> ( F ` y ) = ( F ` w ) )
51 50 eleq1d 
 |-  ( y = w -> ( ( F ` y ) e. ( F ` z ) <-> ( F ` w ) e. ( F ` z ) ) )
52 51 rspccv 
 |-  ( A. y e. z ( F ` y ) e. ( F ` z ) -> ( w e. z -> ( F ` w ) e. ( F ` z ) ) )
53 49 52 syl6 
 |-  ( z e. A -> ( A. x e. A A. y e. x ( F ` y ) e. ( F ` x ) -> ( w e. z -> ( F ` w ) e. ( F ` z ) ) ) )
54 53 3imp 
 |-  ( ( z e. A /\ A. x e. A A. y e. x ( F ` y ) e. ( F ` x ) /\ w e. z ) -> ( F ` w ) e. ( F ` z ) )
55 eleq2 
 |-  ( ( F ` z ) = ( F ` w ) -> ( ( F ` w ) e. ( F ` z ) <-> ( F ` w ) e. ( F ` w ) ) )
56 55 biimpac 
 |-  ( ( ( F ` w ) e. ( F ` z ) /\ ( F ` z ) = ( F ` w ) ) -> ( F ` w ) e. ( F ` w ) )
57 54 56 sylan 
 |-  ( ( ( z e. A /\ A. x e. A A. y e. x ( F ` y ) e. ( F ` x ) /\ w e. z ) /\ ( F ` z ) = ( F ` w ) ) -> ( F ` w ) e. ( F ` w ) )
58 42 43 44 45 57 syl31anc 
 |-  ( ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) /\ w e. z /\ ( F ` z ) = ( F ` w ) ) -> ( F ` w ) e. ( F ` w ) )
59 36 3ad2ant1 
 |-  ( ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) /\ w e. z /\ ( F ` z ) = ( F ` w ) ) -> -. ( F ` w ) e. ( F ` w ) )
60 58 59 pm2.21dd 
 |-  ( ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) /\ w e. z /\ ( F ` z ) = ( F ` w ) ) -> z = w )
61 60 3exp 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) -> ( w e. z -> ( ( F ` z ) = ( F ` w ) -> z = w ) ) )
62 39 41 61 3jaod 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) -> ( ( z e. w \/ z = w \/ w e. z ) -> ( ( F ` z ) = ( F ` w ) -> z = w ) ) )
63 11 62 syl5 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( z e. A /\ w e. A ) ) -> ( ( Ord z /\ Ord w ) -> ( ( F ` z ) = ( F ` w ) -> z = w ) ) )
64 63 ex 
 |-  ( ( F Fn A /\ Smo F ) -> ( ( z e. A /\ w e. A ) -> ( ( Ord z /\ Ord w ) -> ( ( F ` z ) = ( F ` w ) -> z = w ) ) ) )
65 10 64 mpdd 
 |-  ( ( F Fn A /\ Smo F ) -> ( ( z e. A /\ w e. A ) -> ( ( F ` z ) = ( F ` w ) -> z = w ) ) )
66 65 ralrimivv 
 |-  ( ( F Fn A /\ Smo F ) -> A. z e. A A. w e. A ( ( F ` z ) = ( F ` w ) -> z = w ) )
67 2 66 sylan 
 |-  ( ( F : A --> B /\ Smo F ) -> A. z e. A A. w e. A ( ( F ` z ) = ( F ` w ) -> z = w ) )
68 dff13 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. z e. A A. w e. A ( ( F ` z ) = ( F ` w ) -> z = w ) ) )
69 1 67 68 sylanbrc 
 |-  ( ( F : A --> B /\ Smo F ) -> F : A -1-1-> B )