Step |
Hyp |
Ref |
Expression |
1 |
|
dfac8clem.1 |
|- F = ( s e. ( A \ { (/) } ) |-> ( iota_ a e. s A. b e. s -. b r a ) ) |
2 |
|
eldifsn |
|- ( s e. ( A \ { (/) } ) <-> ( s e. A /\ s =/= (/) ) ) |
3 |
|
elssuni |
|- ( s e. A -> s C_ U. A ) |
4 |
3
|
ad2antrl |
|- ( ( ( A e. B /\ r We U. A ) /\ ( s e. A /\ s =/= (/) ) ) -> s C_ U. A ) |
5 |
|
simplr |
|- ( ( ( A e. B /\ r We U. A ) /\ ( s e. A /\ s =/= (/) ) ) -> r We U. A ) |
6 |
|
vex |
|- r e. _V |
7 |
|
exse2 |
|- ( r e. _V -> r Se U. A ) |
8 |
6 7
|
mp1i |
|- ( ( ( A e. B /\ r We U. A ) /\ ( s e. A /\ s =/= (/) ) ) -> r Se U. A ) |
9 |
|
simprr |
|- ( ( ( A e. B /\ r We U. A ) /\ ( s e. A /\ s =/= (/) ) ) -> s =/= (/) ) |
10 |
|
wereu2 |
|- ( ( ( r We U. A /\ r Se U. A ) /\ ( s C_ U. A /\ s =/= (/) ) ) -> E! a e. s A. b e. s -. b r a ) |
11 |
5 8 4 9 10
|
syl22anc |
|- ( ( ( A e. B /\ r We U. A ) /\ ( s e. A /\ s =/= (/) ) ) -> E! a e. s A. b e. s -. b r a ) |
12 |
|
riotacl |
|- ( E! a e. s A. b e. s -. b r a -> ( iota_ a e. s A. b e. s -. b r a ) e. s ) |
13 |
11 12
|
syl |
|- ( ( ( A e. B /\ r We U. A ) /\ ( s e. A /\ s =/= (/) ) ) -> ( iota_ a e. s A. b e. s -. b r a ) e. s ) |
14 |
4 13
|
sseldd |
|- ( ( ( A e. B /\ r We U. A ) /\ ( s e. A /\ s =/= (/) ) ) -> ( iota_ a e. s A. b e. s -. b r a ) e. U. A ) |
15 |
2 14
|
sylan2b |
|- ( ( ( A e. B /\ r We U. A ) /\ s e. ( A \ { (/) } ) ) -> ( iota_ a e. s A. b e. s -. b r a ) e. U. A ) |
16 |
15 1
|
fmptd |
|- ( ( A e. B /\ r We U. A ) -> F : ( A \ { (/) } ) --> U. A ) |
17 |
|
difexg |
|- ( A e. B -> ( A \ { (/) } ) e. _V ) |
18 |
17
|
adantr |
|- ( ( A e. B /\ r We U. A ) -> ( A \ { (/) } ) e. _V ) |
19 |
|
uniexg |
|- ( A e. B -> U. A e. _V ) |
20 |
19
|
adantr |
|- ( ( A e. B /\ r We U. A ) -> U. A e. _V ) |
21 |
|
fex2 |
|- ( ( F : ( A \ { (/) } ) --> U. A /\ ( A \ { (/) } ) e. _V /\ U. A e. _V ) -> F e. _V ) |
22 |
16 18 20 21
|
syl3anc |
|- ( ( A e. B /\ r We U. A ) -> F e. _V ) |
23 |
|
riotaex |
|- ( iota_ a e. s A. b e. s -. b r a ) e. _V |
24 |
1
|
fvmpt2 |
|- ( ( s e. ( A \ { (/) } ) /\ ( iota_ a e. s A. b e. s -. b r a ) e. _V ) -> ( F ` s ) = ( iota_ a e. s A. b e. s -. b r a ) ) |
25 |
23 24
|
mpan2 |
|- ( s e. ( A \ { (/) } ) -> ( F ` s ) = ( iota_ a e. s A. b e. s -. b r a ) ) |
26 |
2 25
|
sylbir |
|- ( ( s e. A /\ s =/= (/) ) -> ( F ` s ) = ( iota_ a e. s A. b e. s -. b r a ) ) |
27 |
26
|
adantl |
|- ( ( ( A e. B /\ r We U. A ) /\ ( s e. A /\ s =/= (/) ) ) -> ( F ` s ) = ( iota_ a e. s A. b e. s -. b r a ) ) |
28 |
27 13
|
eqeltrd |
|- ( ( ( A e. B /\ r We U. A ) /\ ( s e. A /\ s =/= (/) ) ) -> ( F ` s ) e. s ) |
29 |
28
|
expr |
|- ( ( ( A e. B /\ r We U. A ) /\ s e. A ) -> ( s =/= (/) -> ( F ` s ) e. s ) ) |
30 |
29
|
ralrimiva |
|- ( ( A e. B /\ r We U. A ) -> A. s e. A ( s =/= (/) -> ( F ` s ) e. s ) ) |
31 |
|
nfv |
|- F/ s z =/= (/) |
32 |
|
nfmpt1 |
|- F/_ s ( s e. ( A \ { (/) } ) |-> ( iota_ a e. s A. b e. s -. b r a ) ) |
33 |
1 32
|
nfcxfr |
|- F/_ s F |
34 |
|
nfcv |
|- F/_ s z |
35 |
33 34
|
nffv |
|- F/_ s ( F ` z ) |
36 |
35
|
nfel1 |
|- F/ s ( F ` z ) e. z |
37 |
31 36
|
nfim |
|- F/ s ( z =/= (/) -> ( F ` z ) e. z ) |
38 |
|
nfv |
|- F/ z ( s =/= (/) -> ( F ` s ) e. s ) |
39 |
|
neeq1 |
|- ( z = s -> ( z =/= (/) <-> s =/= (/) ) ) |
40 |
|
fveq2 |
|- ( z = s -> ( F ` z ) = ( F ` s ) ) |
41 |
|
id |
|- ( z = s -> z = s ) |
42 |
40 41
|
eleq12d |
|- ( z = s -> ( ( F ` z ) e. z <-> ( F ` s ) e. s ) ) |
43 |
39 42
|
imbi12d |
|- ( z = s -> ( ( z =/= (/) -> ( F ` z ) e. z ) <-> ( s =/= (/) -> ( F ` s ) e. s ) ) ) |
44 |
37 38 43
|
cbvralw |
|- ( A. z e. A ( z =/= (/) -> ( F ` z ) e. z ) <-> A. s e. A ( s =/= (/) -> ( F ` s ) e. s ) ) |
45 |
30 44
|
sylibr |
|- ( ( A e. B /\ r We U. A ) -> A. z e. A ( z =/= (/) -> ( F ` z ) e. z ) ) |
46 |
|
fveq1 |
|- ( f = F -> ( f ` z ) = ( F ` z ) ) |
47 |
46
|
eleq1d |
|- ( f = F -> ( ( f ` z ) e. z <-> ( F ` z ) e. z ) ) |
48 |
47
|
imbi2d |
|- ( f = F -> ( ( z =/= (/) -> ( f ` z ) e. z ) <-> ( z =/= (/) -> ( F ` z ) e. z ) ) ) |
49 |
48
|
ralbidv |
|- ( f = F -> ( A. z e. A ( z =/= (/) -> ( f ` z ) e. z ) <-> A. z e. A ( z =/= (/) -> ( F ` z ) e. z ) ) ) |
50 |
22 45 49
|
spcedv |
|- ( ( A e. B /\ r We U. A ) -> E. f A. z e. A ( z =/= (/) -> ( f ` z ) e. z ) ) |
51 |
50
|
ex |
|- ( A e. B -> ( r We U. A -> E. f A. z e. A ( z =/= (/) -> ( f ` z ) e. z ) ) ) |
52 |
51
|
exlimdv |
|- ( A e. B -> ( E. r r We U. A -> E. f A. z e. A ( z =/= (/) -> ( f ` z ) e. z ) ) ) |