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 imbitrrdi 
 |-  ( ( 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 ) )