Metamath Proof Explorer


Theorem coe1mul2lem1

Description: An equivalence for coe1mul2 . (Contributed by Stefan O'Rear, 25-Mar-2015)

Ref Expression
Assertion coe1mul2lem1
|- ( ( A e. NN0 /\ X e. ( NN0 ^m 1o ) ) -> ( X oR <_ ( 1o X. { A } ) <-> ( X ` (/) ) e. ( 0 ... A ) ) )

Proof

Step Hyp Ref Expression
1 1on
 |-  1o e. On
2 1 a1i
 |-  ( ( A e. NN0 /\ X e. ( NN0 ^m 1o ) ) -> 1o e. On )
3 fvexd
 |-  ( ( ( A e. NN0 /\ X e. ( NN0 ^m 1o ) ) /\ a e. 1o ) -> ( X ` (/) ) e. _V )
4 simpll
 |-  ( ( ( A e. NN0 /\ X e. ( NN0 ^m 1o ) ) /\ a e. 1o ) -> A e. NN0 )
5 df1o2
 |-  1o = { (/) }
6 nn0ex
 |-  NN0 e. _V
7 0ex
 |-  (/) e. _V
8 5 6 7 mapsnconst
 |-  ( X e. ( NN0 ^m 1o ) -> X = ( 1o X. { ( X ` (/) ) } ) )
9 8 adantl
 |-  ( ( A e. NN0 /\ X e. ( NN0 ^m 1o ) ) -> X = ( 1o X. { ( X ` (/) ) } ) )
10 fconstmpt
 |-  ( 1o X. { ( X ` (/) ) } ) = ( a e. 1o |-> ( X ` (/) ) )
11 9 10 eqtrdi
 |-  ( ( A e. NN0 /\ X e. ( NN0 ^m 1o ) ) -> X = ( a e. 1o |-> ( X ` (/) ) ) )
12 fconstmpt
 |-  ( 1o X. { A } ) = ( a e. 1o |-> A )
13 12 a1i
 |-  ( ( A e. NN0 /\ X e. ( NN0 ^m 1o ) ) -> ( 1o X. { A } ) = ( a e. 1o |-> A ) )
14 2 3 4 11 13 ofrfval2
 |-  ( ( A e. NN0 /\ X e. ( NN0 ^m 1o ) ) -> ( X oR <_ ( 1o X. { A } ) <-> A. a e. 1o ( X ` (/) ) <_ A ) )
15 1n0
 |-  1o =/= (/)
16 r19.3rzv
 |-  ( 1o =/= (/) -> ( ( X ` (/) ) <_ A <-> A. a e. 1o ( X ` (/) ) <_ A ) )
17 15 16 mp1i
 |-  ( ( A e. NN0 /\ X e. ( NN0 ^m 1o ) ) -> ( ( X ` (/) ) <_ A <-> A. a e. 1o ( X ` (/) ) <_ A ) )
18 elmapi
 |-  ( X e. ( NN0 ^m 1o ) -> X : 1o --> NN0 )
19 0lt1o
 |-  (/) e. 1o
20 ffvelrn
 |-  ( ( X : 1o --> NN0 /\ (/) e. 1o ) -> ( X ` (/) ) e. NN0 )
21 18 19 20 sylancl
 |-  ( X e. ( NN0 ^m 1o ) -> ( X ` (/) ) e. NN0 )
22 21 adantl
 |-  ( ( A e. NN0 /\ X e. ( NN0 ^m 1o ) ) -> ( X ` (/) ) e. NN0 )
23 22 biantrurd
 |-  ( ( A e. NN0 /\ X e. ( NN0 ^m 1o ) ) -> ( ( X ` (/) ) <_ A <-> ( ( X ` (/) ) e. NN0 /\ ( X ` (/) ) <_ A ) ) )
24 fznn0
 |-  ( A e. NN0 -> ( ( X ` (/) ) e. ( 0 ... A ) <-> ( ( X ` (/) ) e. NN0 /\ ( X ` (/) ) <_ A ) ) )
25 24 adantr
 |-  ( ( A e. NN0 /\ X e. ( NN0 ^m 1o ) ) -> ( ( X ` (/) ) e. ( 0 ... A ) <-> ( ( X ` (/) ) e. NN0 /\ ( X ` (/) ) <_ A ) ) )
26 23 25 bitr4d
 |-  ( ( A e. NN0 /\ X e. ( NN0 ^m 1o ) ) -> ( ( X ` (/) ) <_ A <-> ( X ` (/) ) e. ( 0 ... A ) ) )
27 14 17 26 3bitr2d
 |-  ( ( A e. NN0 /\ X e. ( NN0 ^m 1o ) ) -> ( X oR <_ ( 1o X. { A } ) <-> ( X ` (/) ) e. ( 0 ... A ) ) )