Metamath Proof Explorer


Theorem dfac8clem

Description: Lemma for dfac8c . (Contributed by Mario Carneiro, 10-Jan-2013)

Ref Expression
Hypothesis dfac8clem.1
|- F = ( s e. ( A \ { (/) } ) |-> ( iota_ a e. s A. b e. s -. b r a ) )
Assertion dfac8clem
|- ( A e. B -> ( E. r r We U. A -> E. f A. z e. A ( z =/= (/) -> ( f ` z ) e. z ) ) )

Proof

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