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