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