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