This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem aceq3lem

Description: Lemma for dfac3 . (Contributed by NM, 2-Apr-2004) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypothesis aceq3lem.1 
|- F = ( w e. dom y |-> ( f ` { u | w y u } ) )
Assertion aceq3lem 
|- ( A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> E. f ( f C_ y /\ f Fn dom y ) )

Proof

Step Hyp Ref Expression
1 aceq3lem.1 
 |-  F = ( w e. dom y |-> ( f ` { u | w y u } ) )
2 vex 
 |-  y e. _V
3 2 rnex 
 |-  ran y e. _V
4 3 pwex 
 |-  ~P ran y e. _V
5 raleq 
 |-  ( x = ~P ran y -> ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) <-> A. z e. ~P ran y ( z =/= (/) -> ( f ` z ) e. z ) ) )
6 5 exbidv 
 |-  ( x = ~P ran y -> ( E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) <-> E. f A. z e. ~P ran y ( z =/= (/) -> ( f ` z ) e. z ) ) )
7 4 6 spcv 
 |-  ( A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> E. f A. z e. ~P ran y ( z =/= (/) -> ( f ` z ) e. z ) )
8 df-mpt 
 |-  ( w e. dom y |-> ( f ` { u | w y u } ) ) = { <. w , h >. | ( w e. dom y /\ h = ( f ` { u | w y u } ) ) }
9 1 8 eqtri 
 |-  F = { <. w , h >. | ( w e. dom y /\ h = ( f ` { u | w y u } ) ) }
10 vex 
 |-  w e. _V
11 10 eldm 
 |-  ( w e. dom y <-> E. u w y u )
12 abn0 
 |-  ( { u | w y u } =/= (/) <-> E. u w y u )
13 11 12 bitr4i 
 |-  ( w e. dom y <-> { u | w y u } =/= (/) )
14 vex 
 |-  u e. _V
15 10 14 brelrn 
 |-  ( w y u -> u e. ran y )
16 15 abssi 
 |-  { u | w y u } C_ ran y
17 3 16 elpwi2 
 |-  { u | w y u } e. ~P ran y
18 neeq1 
 |-  ( z = { u | w y u } -> ( z =/= (/) <-> { u | w y u } =/= (/) ) )
19 fveq2 
 |-  ( z = { u | w y u } -> ( f ` z ) = ( f ` { u | w y u } ) )
20 id 
 |-  ( z = { u | w y u } -> z = { u | w y u } )
21 19 20 eleq12d 
 |-  ( z = { u | w y u } -> ( ( f ` z ) e. z <-> ( f ` { u | w y u } ) e. { u | w y u } ) )
22 18 21 imbi12d 
 |-  ( z = { u | w y u } -> ( ( z =/= (/) -> ( f ` z ) e. z ) <-> ( { u | w y u } =/= (/) -> ( f ` { u | w y u } ) e. { u | w y u } ) ) )
23 22 rspcv 
 |-  ( { u | w y u } e. ~P ran y -> ( A. z e. ~P ran y ( z =/= (/) -> ( f ` z ) e. z ) -> ( { u | w y u } =/= (/) -> ( f ` { u | w y u } ) e. { u | w y u } ) ) )
24 17 23 ax-mp 
 |-  ( A. z e. ~P ran y ( z =/= (/) -> ( f ` z ) e. z ) -> ( { u | w y u } =/= (/) -> ( f ` { u | w y u } ) e. { u | w y u } ) )
25 13 24 biimtrid 
 |-  ( A. z e. ~P ran y ( z =/= (/) -> ( f ` z ) e. z ) -> ( w e. dom y -> ( f ` { u | w y u } ) e. { u | w y u } ) )
26 25 imp 
 |-  ( ( A. z e. ~P ran y ( z =/= (/) -> ( f ` z ) e. z ) /\ w e. dom y ) -> ( f ` { u | w y u } ) e. { u | w y u } )
27 fvex 
 |-  ( f ` { u | w y u } ) e. _V
28 breq2 
 |-  ( z = ( f ` { u | w y u } ) -> ( w y z <-> w y ( f ` { u | w y u } ) ) )
29 breq2 
 |-  ( u = z -> ( w y u <-> w y z ) )
30 29 cbvabv 
 |-  { u | w y u } = { z | w y z }
31 27 28 30 elab2 
 |-  ( ( f ` { u | w y u } ) e. { u | w y u } <-> w y ( f ` { u | w y u } ) )
32 26 31 sylib 
 |-  ( ( A. z e. ~P ran y ( z =/= (/) -> ( f ` z ) e. z ) /\ w e. dom y ) -> w y ( f ` { u | w y u } ) )
33 breq2 
 |-  ( h = ( f ` { u | w y u } ) -> ( w y h <-> w y ( f ` { u | w y u } ) ) )
34 32 33 syl5ibrcom 
 |-  ( ( A. z e. ~P ran y ( z =/= (/) -> ( f ` z ) e. z ) /\ w e. dom y ) -> ( h = ( f ` { u | w y u } ) -> w y h ) )
35 34 expimpd 
 |-  ( A. z e. ~P ran y ( z =/= (/) -> ( f ` z ) e. z ) -> ( ( w e. dom y /\ h = ( f ` { u | w y u } ) ) -> w y h ) )
36 35 ssopab2dv 
 |-  ( A. z e. ~P ran y ( z =/= (/) -> ( f ` z ) e. z ) -> { <. w , h >. | ( w e. dom y /\ h = ( f ` { u | w y u } ) ) } C_ { <. w , h >. | w y h } )
37 opabss 
 |-  { <. w , h >. | w y h } C_ y
38 36 37 sstrdi 
 |-  ( A. z e. ~P ran y ( z =/= (/) -> ( f ` z ) e. z ) -> { <. w , h >. | ( w e. dom y /\ h = ( f ` { u | w y u } ) ) } C_ y )
39 9 38 eqsstrid 
 |-  ( A. z e. ~P ran y ( z =/= (/) -> ( f ` z ) e. z ) -> F C_ y )
40 27 1 fnmpti 
 |-  F Fn dom y
41 2 ssex 
 |-  ( F C_ y -> F e. _V )
42 41 adantr 
 |-  ( ( F C_ y /\ F Fn dom y ) -> F e. _V )
43 sseq1 
 |-  ( g = F -> ( g C_ y <-> F C_ y ) )
44 fneq1 
 |-  ( g = F -> ( g Fn dom y <-> F Fn dom y ) )
45 43 44 anbi12d 
 |-  ( g = F -> ( ( g C_ y /\ g Fn dom y ) <-> ( F C_ y /\ F Fn dom y ) ) )
46 45 spcegv 
 |-  ( F e. _V -> ( ( F C_ y /\ F Fn dom y ) -> E. g ( g C_ y /\ g Fn dom y ) ) )
47 42 46 mpcom 
 |-  ( ( F C_ y /\ F Fn dom y ) -> E. g ( g C_ y /\ g Fn dom y ) )
48 39 40 47 sylancl 
 |-  ( A. z e. ~P ran y ( z =/= (/) -> ( f ` z ) e. z ) -> E. g ( g C_ y /\ g Fn dom y ) )
49 48 exlimiv 
 |-  ( E. f A. z e. ~P ran y ( z =/= (/) -> ( f ` z ) e. z ) -> E. g ( g C_ y /\ g Fn dom y ) )
50 7 49 syl 
 |-  ( A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> E. g ( g C_ y /\ g Fn dom y ) )
51 sseq1 
 |-  ( g = f -> ( g C_ y <-> f C_ y ) )
52 fneq1 
 |-  ( g = f -> ( g Fn dom y <-> f Fn dom y ) )
53 51 52 anbi12d 
 |-  ( g = f -> ( ( g C_ y /\ g Fn dom y ) <-> ( f C_ y /\ f Fn dom y ) ) )
54 53 cbvexvw 
 |-  ( E. g ( g C_ y /\ g Fn dom y ) <-> E. f ( f C_ y /\ f Fn dom y ) )
55 50 54 sylib 
 |-  ( A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> E. f ( f C_ y /\ f Fn dom y ) )