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