Step |
Hyp |
Ref |
Expression |
1 |
|
cstucnd.1 |
|- ( ph -> U e. ( UnifOn ` X ) ) |
2 |
|
cstucnd.2 |
|- ( ph -> V e. ( UnifOn ` Y ) ) |
3 |
|
cstucnd.3 |
|- ( ph -> A e. Y ) |
4 |
|
fconst6g |
|- ( A e. Y -> ( X X. { A } ) : X --> Y ) |
5 |
3 4
|
syl |
|- ( ph -> ( X X. { A } ) : X --> Y ) |
6 |
1
|
adantr |
|- ( ( ph /\ s e. V ) -> U e. ( UnifOn ` X ) ) |
7 |
|
ustne0 |
|- ( U e. ( UnifOn ` X ) -> U =/= (/) ) |
8 |
6 7
|
syl |
|- ( ( ph /\ s e. V ) -> U =/= (/) ) |
9 |
2
|
ad3antrrr |
|- ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> V e. ( UnifOn ` Y ) ) |
10 |
|
simpllr |
|- ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> s e. V ) |
11 |
3
|
ad3antrrr |
|- ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> A e. Y ) |
12 |
|
ustref |
|- ( ( V e. ( UnifOn ` Y ) /\ s e. V /\ A e. Y ) -> A s A ) |
13 |
9 10 11 12
|
syl3anc |
|- ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> A s A ) |
14 |
|
simprl |
|- ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> x e. X ) |
15 |
|
fvconst2g |
|- ( ( A e. Y /\ x e. X ) -> ( ( X X. { A } ) ` x ) = A ) |
16 |
11 14 15
|
syl2anc |
|- ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> ( ( X X. { A } ) ` x ) = A ) |
17 |
|
simprr |
|- ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> y e. X ) |
18 |
|
fvconst2g |
|- ( ( A e. Y /\ y e. X ) -> ( ( X X. { A } ) ` y ) = A ) |
19 |
11 17 18
|
syl2anc |
|- ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> ( ( X X. { A } ) ` y ) = A ) |
20 |
13 16 19
|
3brtr4d |
|- ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> ( ( X X. { A } ) ` x ) s ( ( X X. { A } ) ` y ) ) |
21 |
20
|
a1d |
|- ( ( ( ( ph /\ s e. V ) /\ r e. U ) /\ ( x e. X /\ y e. X ) ) -> ( x r y -> ( ( X X. { A } ) ` x ) s ( ( X X. { A } ) ` y ) ) ) |
22 |
21
|
ralrimivva |
|- ( ( ( ph /\ s e. V ) /\ r e. U ) -> A. x e. X A. y e. X ( x r y -> ( ( X X. { A } ) ` x ) s ( ( X X. { A } ) ` y ) ) ) |
23 |
22
|
reximdva0 |
|- ( ( ( ph /\ s e. V ) /\ U =/= (/) ) -> E. r e. U A. x e. X A. y e. X ( x r y -> ( ( X X. { A } ) ` x ) s ( ( X X. { A } ) ` y ) ) ) |
24 |
8 23
|
mpdan |
|- ( ( ph /\ s e. V ) -> E. r e. U A. x e. X A. y e. X ( x r y -> ( ( X X. { A } ) ` x ) s ( ( X X. { A } ) ` y ) ) ) |
25 |
24
|
ralrimiva |
|- ( ph -> A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( ( X X. { A } ) ` x ) s ( ( X X. { A } ) ` y ) ) ) |
26 |
|
isucn |
|- ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( ( X X. { A } ) e. ( U uCn V ) <-> ( ( X X. { A } ) : X --> Y /\ A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( ( X X. { A } ) ` x ) s ( ( X X. { A } ) ` y ) ) ) ) ) |
27 |
1 2 26
|
syl2anc |
|- ( ph -> ( ( X X. { A } ) e. ( U uCn V ) <-> ( ( X X. { A } ) : X --> Y /\ A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( ( X X. { A } ) ` x ) s ( ( X X. { A } ) ` y ) ) ) ) ) |
28 |
5 25 27
|
mpbir2and |
|- ( ph -> ( X X. { A } ) e. ( U uCn V ) ) |