Metamath Proof Explorer

Theorem 0pledm

Description: Adjust the domain of the left argument to match the right, which works better in our theorems. (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses 0pledm.1 
|- ( ph -> A C_ CC )
0pledm.2 
|- ( ph -> F Fn A )
Assertion 0pledm 
|- ( ph -> ( 0p oR <_ F <-> ( A X. { 0 } ) oR <_ F ) )

Proof

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