Step |
Hyp |
Ref |
Expression |
1 |
|
uniimadom.1 |
|- A e. _V |
2 |
|
uniimadom.2 |
|- B e. _V |
3 |
1
|
funimaex |
|- ( Fun F -> ( F " A ) e. _V ) |
4 |
3
|
adantr |
|- ( ( Fun F /\ A. x e. A ( F ` x ) ~<_ B ) -> ( F " A ) e. _V ) |
5 |
|
fvelima |
|- ( ( Fun F /\ y e. ( F " A ) ) -> E. x e. A ( F ` x ) = y ) |
6 |
5
|
ex |
|- ( Fun F -> ( y e. ( F " A ) -> E. x e. A ( F ` x ) = y ) ) |
7 |
|
breq1 |
|- ( ( F ` x ) = y -> ( ( F ` x ) ~<_ B <-> y ~<_ B ) ) |
8 |
7
|
biimpd |
|- ( ( F ` x ) = y -> ( ( F ` x ) ~<_ B -> y ~<_ B ) ) |
9 |
8
|
reximi |
|- ( E. x e. A ( F ` x ) = y -> E. x e. A ( ( F ` x ) ~<_ B -> y ~<_ B ) ) |
10 |
|
r19.36v |
|- ( E. x e. A ( ( F ` x ) ~<_ B -> y ~<_ B ) -> ( A. x e. A ( F ` x ) ~<_ B -> y ~<_ B ) ) |
11 |
9 10
|
syl |
|- ( E. x e. A ( F ` x ) = y -> ( A. x e. A ( F ` x ) ~<_ B -> y ~<_ B ) ) |
12 |
6 11
|
syl6 |
|- ( Fun F -> ( y e. ( F " A ) -> ( A. x e. A ( F ` x ) ~<_ B -> y ~<_ B ) ) ) |
13 |
12
|
com23 |
|- ( Fun F -> ( A. x e. A ( F ` x ) ~<_ B -> ( y e. ( F " A ) -> y ~<_ B ) ) ) |
14 |
13
|
imp |
|- ( ( Fun F /\ A. x e. A ( F ` x ) ~<_ B ) -> ( y e. ( F " A ) -> y ~<_ B ) ) |
15 |
14
|
ralrimiv |
|- ( ( Fun F /\ A. x e. A ( F ` x ) ~<_ B ) -> A. y e. ( F " A ) y ~<_ B ) |
16 |
|
unidom |
|- ( ( ( F " A ) e. _V /\ A. y e. ( F " A ) y ~<_ B ) -> U. ( F " A ) ~<_ ( ( F " A ) X. B ) ) |
17 |
4 15 16
|
syl2anc |
|- ( ( Fun F /\ A. x e. A ( F ` x ) ~<_ B ) -> U. ( F " A ) ~<_ ( ( F " A ) X. B ) ) |
18 |
|
imadomg |
|- ( A e. _V -> ( Fun F -> ( F " A ) ~<_ A ) ) |
19 |
1 18
|
ax-mp |
|- ( Fun F -> ( F " A ) ~<_ A ) |
20 |
2
|
xpdom1 |
|- ( ( F " A ) ~<_ A -> ( ( F " A ) X. B ) ~<_ ( A X. B ) ) |
21 |
19 20
|
syl |
|- ( Fun F -> ( ( F " A ) X. B ) ~<_ ( A X. B ) ) |
22 |
21
|
adantr |
|- ( ( Fun F /\ A. x e. A ( F ` x ) ~<_ B ) -> ( ( F " A ) X. B ) ~<_ ( A X. B ) ) |
23 |
|
domtr |
|- ( ( U. ( F " A ) ~<_ ( ( F " A ) X. B ) /\ ( ( F " A ) X. B ) ~<_ ( A X. B ) ) -> U. ( F " A ) ~<_ ( A X. B ) ) |
24 |
17 22 23
|
syl2anc |
|- ( ( Fun F /\ A. x e. A ( F ` x ) ~<_ B ) -> U. ( F " A ) ~<_ ( A X. B ) ) |