Step |
Hyp |
Ref |
Expression |
1 |
|
utopustuq.1 |
|- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) ) |
2 |
|
simp-6l |
|- ( ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) /\ u e. U ) /\ b = ( u " { p } ) ) -> ( U e. ( UnifOn ` X ) /\ p e. X ) ) |
3 |
|
simp-7l |
|- ( ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) /\ u e. U ) /\ b = ( u " { p } ) ) -> U e. ( UnifOn ` X ) ) |
4 |
|
simp-4r |
|- ( ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) /\ u e. U ) /\ b = ( u " { p } ) ) -> w e. U ) |
5 |
|
simplr |
|- ( ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) /\ u e. U ) /\ b = ( u " { p } ) ) -> u e. U ) |
6 |
|
ustincl |
|- ( ( U e. ( UnifOn ` X ) /\ w e. U /\ u e. U ) -> ( w i^i u ) e. U ) |
7 |
3 4 5 6
|
syl3anc |
|- ( ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) /\ u e. U ) /\ b = ( u " { p } ) ) -> ( w i^i u ) e. U ) |
8 |
|
ineq12 |
|- ( ( a = ( w " { p } ) /\ b = ( u " { p } ) ) -> ( a i^i b ) = ( ( w " { p } ) i^i ( u " { p } ) ) ) |
9 |
|
inimasn |
|- ( p e. _V -> ( ( w i^i u ) " { p } ) = ( ( w " { p } ) i^i ( u " { p } ) ) ) |
10 |
9
|
elv |
|- ( ( w i^i u ) " { p } ) = ( ( w " { p } ) i^i ( u " { p } ) ) |
11 |
8 10
|
eqtr4di |
|- ( ( a = ( w " { p } ) /\ b = ( u " { p } ) ) -> ( a i^i b ) = ( ( w i^i u ) " { p } ) ) |
12 |
11
|
ad4ant24 |
|- ( ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) /\ u e. U ) /\ b = ( u " { p } ) ) -> ( a i^i b ) = ( ( w i^i u ) " { p } ) ) |
13 |
|
imaeq1 |
|- ( x = ( w i^i u ) -> ( x " { p } ) = ( ( w i^i u ) " { p } ) ) |
14 |
13
|
rspceeqv |
|- ( ( ( w i^i u ) e. U /\ ( a i^i b ) = ( ( w i^i u ) " { p } ) ) -> E. x e. U ( a i^i b ) = ( x " { p } ) ) |
15 |
7 12 14
|
syl2anc |
|- ( ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) /\ u e. U ) /\ b = ( u " { p } ) ) -> E. x e. U ( a i^i b ) = ( x " { p } ) ) |
16 |
|
vex |
|- a e. _V |
17 |
16
|
inex1 |
|- ( a i^i b ) e. _V |
18 |
1
|
ustuqtoplem |
|- ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ ( a i^i b ) e. _V ) -> ( ( a i^i b ) e. ( N ` p ) <-> E. x e. U ( a i^i b ) = ( x " { p } ) ) ) |
19 |
17 18
|
mpan2 |
|- ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( ( a i^i b ) e. ( N ` p ) <-> E. x e. U ( a i^i b ) = ( x " { p } ) ) ) |
20 |
19
|
biimpar |
|- ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ E. x e. U ( a i^i b ) = ( x " { p } ) ) -> ( a i^i b ) e. ( N ` p ) ) |
21 |
2 15 20
|
syl2anc |
|- ( ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) /\ u e. U ) /\ b = ( u " { p } ) ) -> ( a i^i b ) e. ( N ` p ) ) |
22 |
1
|
ustuqtoplem |
|- ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ b e. _V ) -> ( b e. ( N ` p ) <-> E. u e. U b = ( u " { p } ) ) ) |
23 |
22
|
elvd |
|- ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( b e. ( N ` p ) <-> E. u e. U b = ( u " { p } ) ) ) |
24 |
23
|
biimpa |
|- ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ b e. ( N ` p ) ) -> E. u e. U b = ( u " { p } ) ) |
25 |
24
|
ad5ant13 |
|- ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> E. u e. U b = ( u " { p } ) ) |
26 |
21 25
|
r19.29a |
|- ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> ( a i^i b ) e. ( N ` p ) ) |
27 |
1
|
ustuqtoplem |
|- ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. _V ) -> ( a e. ( N ` p ) <-> E. w e. U a = ( w " { p } ) ) ) |
28 |
27
|
elvd |
|- ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( a e. ( N ` p ) <-> E. w e. U a = ( w " { p } ) ) ) |
29 |
28
|
biimpa |
|- ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> E. w e. U a = ( w " { p } ) ) |
30 |
29
|
adantr |
|- ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) -> E. w e. U a = ( w " { p } ) ) |
31 |
26 30
|
r19.29a |
|- ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ b e. ( N ` p ) ) -> ( a i^i b ) e. ( N ` p ) ) |
32 |
31
|
ralrimiva |
|- ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> A. b e. ( N ` p ) ( a i^i b ) e. ( N ` p ) ) |
33 |
32
|
ralrimiva |
|- ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> A. a e. ( N ` p ) A. b e. ( N ` p ) ( a i^i b ) e. ( N ` p ) ) |
34 |
|
fvex |
|- ( N ` p ) e. _V |
35 |
|
inficl |
|- ( ( N ` p ) e. _V -> ( A. a e. ( N ` p ) A. b e. ( N ` p ) ( a i^i b ) e. ( N ` p ) <-> ( fi ` ( N ` p ) ) = ( N ` p ) ) ) |
36 |
34 35
|
ax-mp |
|- ( A. a e. ( N ` p ) A. b e. ( N ` p ) ( a i^i b ) e. ( N ` p ) <-> ( fi ` ( N ` p ) ) = ( N ` p ) ) |
37 |
33 36
|
sylib |
|- ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( fi ` ( N ` p ) ) = ( N ` p ) ) |
38 |
|
eqimss |
|- ( ( fi ` ( N ` p ) ) = ( N ` p ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) ) |
39 |
37 38
|
syl |
|- ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) ) |