Step |
Hyp |
Ref |
Expression |
1 |
|
0pledm.1 |
|- ( ph -> A C_ CC ) |
2 |
|
0pledm.2 |
|- ( ph -> F Fn A ) |
3 |
|
sseqin2 |
|- ( A C_ CC <-> ( CC i^i A ) = A ) |
4 |
1 3
|
sylib |
|- ( ph -> ( CC i^i A ) = A ) |
5 |
4
|
raleqdv |
|- ( ph -> ( A. x e. ( CC i^i A ) 0 <_ ( F ` x ) <-> A. x e. A 0 <_ ( F ` x ) ) ) |
6 |
|
0cn |
|- 0 e. CC |
7 |
|
fnconstg |
|- ( 0 e. CC -> ( CC X. { 0 } ) Fn CC ) |
8 |
6 7
|
ax-mp |
|- ( CC X. { 0 } ) Fn CC |
9 |
|
df-0p |
|- 0p = ( CC X. { 0 } ) |
10 |
9
|
fneq1i |
|- ( 0p Fn CC <-> ( CC X. { 0 } ) Fn CC ) |
11 |
8 10
|
mpbir |
|- 0p Fn CC |
12 |
11
|
a1i |
|- ( ph -> 0p Fn CC ) |
13 |
|
cnex |
|- CC e. _V |
14 |
13
|
a1i |
|- ( ph -> CC e. _V ) |
15 |
|
ssexg |
|- ( ( A C_ CC /\ CC e. _V ) -> A e. _V ) |
16 |
1 13 15
|
sylancl |
|- ( ph -> A e. _V ) |
17 |
|
eqid |
|- ( CC i^i A ) = ( CC i^i A ) |
18 |
|
0pval |
|- ( x e. CC -> ( 0p ` x ) = 0 ) |
19 |
18
|
adantl |
|- ( ( ph /\ x e. CC ) -> ( 0p ` x ) = 0 ) |
20 |
|
eqidd |
|- ( ( ph /\ x e. A ) -> ( F ` x ) = ( F ` x ) ) |
21 |
12 2 14 16 17 19 20
|
ofrfval |
|- ( ph -> ( 0p oR <_ F <-> A. x e. ( CC i^i A ) 0 <_ ( F ` x ) ) ) |
22 |
|
fnconstg |
|- ( 0 e. CC -> ( A X. { 0 } ) Fn A ) |
23 |
6 22
|
ax-mp |
|- ( A X. { 0 } ) Fn A |
24 |
23
|
a1i |
|- ( ph -> ( A X. { 0 } ) Fn A ) |
25 |
|
inidm |
|- ( A i^i A ) = A |
26 |
|
c0ex |
|- 0 e. _V |
27 |
26
|
fvconst2 |
|- ( x e. A -> ( ( A X. { 0 } ) ` x ) = 0 ) |
28 |
27
|
adantl |
|- ( ( ph /\ x e. A ) -> ( ( A X. { 0 } ) ` x ) = 0 ) |
29 |
24 2 16 16 25 28 20
|
ofrfval |
|- ( ph -> ( ( A X. { 0 } ) oR <_ F <-> A. x e. A 0 <_ ( F ` x ) ) ) |
30 |
5 21 29
|
3bitr4d |
|- ( ph -> ( 0p oR <_ F <-> ( A X. { 0 } ) oR <_ F ) ) |