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