Metamath Proof Explorer


Theorem smogt

Description: A strictly monotone ordinal function is greater than or equal to its argument. Exercise 1 in TakeutiZaring p. 50. (Contributed by Andrew Salmon, 23-Nov-2011) (Revised by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion smogt
|- ( ( F Fn A /\ Smo F /\ C e. A ) -> C C_ ( F ` C ) )

Proof

Step Hyp Ref Expression
1 id
 |-  ( x = C -> x = C )
2 fveq2
 |-  ( x = C -> ( F ` x ) = ( F ` C ) )
3 1 2 sseq12d
 |-  ( x = C -> ( x C_ ( F ` x ) <-> C C_ ( F ` C ) ) )
4 3 imbi2d
 |-  ( x = C -> ( ( ( F Fn A /\ Smo F ) -> x C_ ( F ` x ) ) <-> ( ( F Fn A /\ Smo F ) -> C C_ ( F ` C ) ) ) )
5 smodm2
 |-  ( ( F Fn A /\ Smo F ) -> Ord A )
6 5 3adant3
 |-  ( ( F Fn A /\ Smo F /\ x e. A ) -> Ord A )
7 simp3
 |-  ( ( F Fn A /\ Smo F /\ x e. A ) -> x e. A )
8 ordelord
 |-  ( ( Ord A /\ x e. A ) -> Ord x )
9 6 7 8 syl2anc
 |-  ( ( F Fn A /\ Smo F /\ x e. A ) -> Ord x )
10 vex
 |-  x e. _V
11 10 elon
 |-  ( x e. On <-> Ord x )
12 9 11 sylibr
 |-  ( ( F Fn A /\ Smo F /\ x e. A ) -> x e. On )
13 eleq1w
 |-  ( x = y -> ( x e. A <-> y e. A ) )
14 13 3anbi3d
 |-  ( x = y -> ( ( F Fn A /\ Smo F /\ x e. A ) <-> ( F Fn A /\ Smo F /\ y e. A ) ) )
15 id
 |-  ( x = y -> x = y )
16 fveq2
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
17 15 16 sseq12d
 |-  ( x = y -> ( x C_ ( F ` x ) <-> y C_ ( F ` y ) ) )
18 14 17 imbi12d
 |-  ( x = y -> ( ( ( F Fn A /\ Smo F /\ x e. A ) -> x C_ ( F ` x ) ) <-> ( ( F Fn A /\ Smo F /\ y e. A ) -> y C_ ( F ` y ) ) ) )
19 simpl1
 |-  ( ( ( F Fn A /\ Smo F /\ x e. A ) /\ y e. x ) -> F Fn A )
20 simpl2
 |-  ( ( ( F Fn A /\ Smo F /\ x e. A ) /\ y e. x ) -> Smo F )
21 ordtr1
 |-  ( Ord A -> ( ( y e. x /\ x e. A ) -> y e. A ) )
22 21 expcomd
 |-  ( Ord A -> ( x e. A -> ( y e. x -> y e. A ) ) )
23 6 7 22 sylc
 |-  ( ( F Fn A /\ Smo F /\ x e. A ) -> ( y e. x -> y e. A ) )
24 23 imp
 |-  ( ( ( F Fn A /\ Smo F /\ x e. A ) /\ y e. x ) -> y e. A )
25 pm2.27
 |-  ( ( F Fn A /\ Smo F /\ y e. A ) -> ( ( ( F Fn A /\ Smo F /\ y e. A ) -> y C_ ( F ` y ) ) -> y C_ ( F ` y ) ) )
26 19 20 24 25 syl3anc
 |-  ( ( ( F Fn A /\ Smo F /\ x e. A ) /\ y e. x ) -> ( ( ( F Fn A /\ Smo F /\ y e. A ) -> y C_ ( F ` y ) ) -> y C_ ( F ` y ) ) )
27 26 ralimdva
 |-  ( ( F Fn A /\ Smo F /\ x e. A ) -> ( A. y e. x ( ( F Fn A /\ Smo F /\ y e. A ) -> y C_ ( F ` y ) ) -> A. y e. x y C_ ( F ` y ) ) )
28 5 3adant3
 |-  ( ( F Fn A /\ Smo F /\ ( x e. A /\ y e. x /\ y C_ ( F ` y ) ) ) -> Ord A )
29 simp31
 |-  ( ( F Fn A /\ Smo F /\ ( x e. A /\ y e. x /\ y C_ ( F ` y ) ) ) -> x e. A )
30 28 29 8 syl2anc
 |-  ( ( F Fn A /\ Smo F /\ ( x e. A /\ y e. x /\ y C_ ( F ` y ) ) ) -> Ord x )
31 simp32
 |-  ( ( F Fn A /\ Smo F /\ ( x e. A /\ y e. x /\ y C_ ( F ` y ) ) ) -> y e. x )
32 ordelord
 |-  ( ( Ord x /\ y e. x ) -> Ord y )
33 30 31 32 syl2anc
 |-  ( ( F Fn A /\ Smo F /\ ( x e. A /\ y e. x /\ y C_ ( F ` y ) ) ) -> Ord y )
34 smofvon2
 |-  ( Smo F -> ( F ` x ) e. On )
35 34 3ad2ant2
 |-  ( ( F Fn A /\ Smo F /\ ( x e. A /\ y e. x /\ y C_ ( F ` y ) ) ) -> ( F ` x ) e. On )
36 eloni
 |-  ( ( F ` x ) e. On -> Ord ( F ` x ) )
37 35 36 syl
 |-  ( ( F Fn A /\ Smo F /\ ( x e. A /\ y e. x /\ y C_ ( F ` y ) ) ) -> Ord ( F ` x ) )
38 simp33
 |-  ( ( F Fn A /\ Smo F /\ ( x e. A /\ y e. x /\ y C_ ( F ` y ) ) ) -> y C_ ( F ` y ) )
39 smoel2
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( x e. A /\ y e. x ) ) -> ( F ` y ) e. ( F ` x ) )
40 39 3adantr3
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( x e. A /\ y e. x /\ y C_ ( F ` y ) ) ) -> ( F ` y ) e. ( F ` x ) )
41 40 3impa
 |-  ( ( F Fn A /\ Smo F /\ ( x e. A /\ y e. x /\ y C_ ( F ` y ) ) ) -> ( F ` y ) e. ( F ` x ) )
42 ordtr2
 |-  ( ( Ord y /\ Ord ( F ` x ) ) -> ( ( y C_ ( F ` y ) /\ ( F ` y ) e. ( F ` x ) ) -> y e. ( F ` x ) ) )
43 42 imp
 |-  ( ( ( Ord y /\ Ord ( F ` x ) ) /\ ( y C_ ( F ` y ) /\ ( F ` y ) e. ( F ` x ) ) ) -> y e. ( F ` x ) )
44 33 37 38 41 43 syl22anc
 |-  ( ( F Fn A /\ Smo F /\ ( x e. A /\ y e. x /\ y C_ ( F ` y ) ) ) -> y e. ( F ` x ) )
45 44 3expia
 |-  ( ( F Fn A /\ Smo F ) -> ( ( x e. A /\ y e. x /\ y C_ ( F ` y ) ) -> y e. ( F ` x ) ) )
46 45 3expd
 |-  ( ( F Fn A /\ Smo F ) -> ( x e. A -> ( y e. x -> ( y C_ ( F ` y ) -> y e. ( F ` x ) ) ) ) )
47 46 3impia
 |-  ( ( F Fn A /\ Smo F /\ x e. A ) -> ( y e. x -> ( y C_ ( F ` y ) -> y e. ( F ` x ) ) ) )
48 47 imp
 |-  ( ( ( F Fn A /\ Smo F /\ x e. A ) /\ y e. x ) -> ( y C_ ( F ` y ) -> y e. ( F ` x ) ) )
49 48 ralimdva
 |-  ( ( F Fn A /\ Smo F /\ x e. A ) -> ( A. y e. x y C_ ( F ` y ) -> A. y e. x y e. ( F ` x ) ) )
50 dfss3
 |-  ( x C_ ( F ` x ) <-> A. y e. x y e. ( F ` x ) )
51 49 50 syl6ibr
 |-  ( ( F Fn A /\ Smo F /\ x e. A ) -> ( A. y e. x y C_ ( F ` y ) -> x C_ ( F ` x ) ) )
52 27 51 syldc
 |-  ( A. y e. x ( ( F Fn A /\ Smo F /\ y e. A ) -> y C_ ( F ` y ) ) -> ( ( F Fn A /\ Smo F /\ x e. A ) -> x C_ ( F ` x ) ) )
53 52 a1i
 |-  ( x e. On -> ( A. y e. x ( ( F Fn A /\ Smo F /\ y e. A ) -> y C_ ( F ` y ) ) -> ( ( F Fn A /\ Smo F /\ x e. A ) -> x C_ ( F ` x ) ) ) )
54 18 53 tfis2
 |-  ( x e. On -> ( ( F Fn A /\ Smo F /\ x e. A ) -> x C_ ( F ` x ) ) )
55 12 54 mpcom
 |-  ( ( F Fn A /\ Smo F /\ x e. A ) -> x C_ ( F ` x ) )
56 55 3expia
 |-  ( ( F Fn A /\ Smo F ) -> ( x e. A -> x C_ ( F ` x ) ) )
57 56 com12
 |-  ( x e. A -> ( ( F Fn A /\ Smo F ) -> x C_ ( F ` x ) ) )
58 4 57 vtoclga
 |-  ( C e. A -> ( ( F Fn A /\ Smo F ) -> C C_ ( F ` C ) ) )
59 58 com12
 |-  ( ( F Fn A /\ Smo F ) -> ( C e. A -> C C_ ( F ` C ) ) )
60 59 3impia
 |-  ( ( F Fn A /\ Smo F /\ C e. A ) -> C C_ ( F ` C ) )