Metamath Proof Explorer


Theorem dfac5lem5

Description: Lemma for dfac5 . (Contributed by NM, 12-Apr-2004)

Ref Expression
Hypotheses dfac5lem.1
|- A = { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) }
dfac5lem.2
|- B = ( U. A i^i y )
dfac5lem.3
|- ( ph <-> A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) )
Assertion dfac5lem5
|- ( ph -> E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) )

Proof

Step Hyp Ref Expression
1 dfac5lem.1
 |-  A = { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) }
2 dfac5lem.2
 |-  B = ( U. A i^i y )
3 dfac5lem.3
 |-  ( ph <-> A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) )
4 1 2 3 dfac5lem4
 |-  ( ph -> E. y A. z e. A E! v v e. ( z i^i y ) )
5 simpr
 |-  ( ( w =/= (/) /\ w e. h ) -> w e. h )
6 5 a1i
 |-  ( A. z e. A E! v v e. ( z i^i y ) -> ( ( w =/= (/) /\ w e. h ) -> w e. h ) )
7 ineq1
 |-  ( z = ( { w } X. w ) -> ( z i^i y ) = ( ( { w } X. w ) i^i y ) )
8 7 eleq2d
 |-  ( z = ( { w } X. w ) -> ( v e. ( z i^i y ) <-> v e. ( ( { w } X. w ) i^i y ) ) )
9 8 eubidv
 |-  ( z = ( { w } X. w ) -> ( E! v v e. ( z i^i y ) <-> E! v v e. ( ( { w } X. w ) i^i y ) ) )
10 9 rspccv
 |-  ( A. z e. A E! v v e. ( z i^i y ) -> ( ( { w } X. w ) e. A -> E! v v e. ( ( { w } X. w ) i^i y ) ) )
11 1 dfac5lem3
 |-  ( ( { w } X. w ) e. A <-> ( w =/= (/) /\ w e. h ) )
12 dfac5lem1
 |-  ( E! v v e. ( ( { w } X. w ) i^i y ) <-> E! g ( g e. w /\ <. w , g >. e. y ) )
13 10 11 12 3imtr3g
 |-  ( A. z e. A E! v v e. ( z i^i y ) -> ( ( w =/= (/) /\ w e. h ) -> E! g ( g e. w /\ <. w , g >. e. y ) ) )
14 6 13 jcad
 |-  ( A. z e. A E! v v e. ( z i^i y ) -> ( ( w =/= (/) /\ w e. h ) -> ( w e. h /\ E! g ( g e. w /\ <. w , g >. e. y ) ) ) )
15 2 eleq2i
 |-  ( <. w , g >. e. B <-> <. w , g >. e. ( U. A i^i y ) )
16 elin
 |-  ( <. w , g >. e. ( U. A i^i y ) <-> ( <. w , g >. e. U. A /\ <. w , g >. e. y ) )
17 1 dfac5lem2
 |-  ( <. w , g >. e. U. A <-> ( w e. h /\ g e. w ) )
18 17 anbi1i
 |-  ( ( <. w , g >. e. U. A /\ <. w , g >. e. y ) <-> ( ( w e. h /\ g e. w ) /\ <. w , g >. e. y ) )
19 anass
 |-  ( ( ( w e. h /\ g e. w ) /\ <. w , g >. e. y ) <-> ( w e. h /\ ( g e. w /\ <. w , g >. e. y ) ) )
20 18 19 bitri
 |-  ( ( <. w , g >. e. U. A /\ <. w , g >. e. y ) <-> ( w e. h /\ ( g e. w /\ <. w , g >. e. y ) ) )
21 15 16 20 3bitri
 |-  ( <. w , g >. e. B <-> ( w e. h /\ ( g e. w /\ <. w , g >. e. y ) ) )
22 21 eubii
 |-  ( E! g <. w , g >. e. B <-> E! g ( w e. h /\ ( g e. w /\ <. w , g >. e. y ) ) )
23 euanv
 |-  ( E! g ( w e. h /\ ( g e. w /\ <. w , g >. e. y ) ) <-> ( w e. h /\ E! g ( g e. w /\ <. w , g >. e. y ) ) )
24 22 23 bitr2i
 |-  ( ( w e. h /\ E! g ( g e. w /\ <. w , g >. e. y ) ) <-> E! g <. w , g >. e. B )
25 14 24 syl6ib
 |-  ( A. z e. A E! v v e. ( z i^i y ) -> ( ( w =/= (/) /\ w e. h ) -> E! g <. w , g >. e. B ) )
26 euex
 |-  ( E! g <. w , g >. e. B -> E. g <. w , g >. e. B )
27 nfeu1
 |-  F/ g E! g <. w , g >. e. B
28 nfv
 |-  F/ g ( B ` w ) e. w
29 27 28 nfim
 |-  F/ g ( E! g <. w , g >. e. B -> ( B ` w ) e. w )
30 21 simprbi
 |-  ( <. w , g >. e. B -> ( g e. w /\ <. w , g >. e. y ) )
31 30 simpld
 |-  ( <. w , g >. e. B -> g e. w )
32 tz6.12
 |-  ( ( <. w , g >. e. B /\ E! g <. w , g >. e. B ) -> ( B ` w ) = g )
33 32 eleq1d
 |-  ( ( <. w , g >. e. B /\ E! g <. w , g >. e. B ) -> ( ( B ` w ) e. w <-> g e. w ) )
34 33 biimparc
 |-  ( ( g e. w /\ ( <. w , g >. e. B /\ E! g <. w , g >. e. B ) ) -> ( B ` w ) e. w )
35 34 exp32
 |-  ( g e. w -> ( <. w , g >. e. B -> ( E! g <. w , g >. e. B -> ( B ` w ) e. w ) ) )
36 31 35 mpcom
 |-  ( <. w , g >. e. B -> ( E! g <. w , g >. e. B -> ( B ` w ) e. w ) )
37 29 36 exlimi
 |-  ( E. g <. w , g >. e. B -> ( E! g <. w , g >. e. B -> ( B ` w ) e. w ) )
38 26 37 mpcom
 |-  ( E! g <. w , g >. e. B -> ( B ` w ) e. w )
39 25 38 syl6
 |-  ( A. z e. A E! v v e. ( z i^i y ) -> ( ( w =/= (/) /\ w e. h ) -> ( B ` w ) e. w ) )
40 39 expcomd
 |-  ( A. z e. A E! v v e. ( z i^i y ) -> ( w e. h -> ( w =/= (/) -> ( B ` w ) e. w ) ) )
41 40 ralrimiv
 |-  ( A. z e. A E! v v e. ( z i^i y ) -> A. w e. h ( w =/= (/) -> ( B ` w ) e. w ) )
42 vex
 |-  y e. _V
43 42 inex2
 |-  ( U. A i^i y ) e. _V
44 2 43 eqeltri
 |-  B e. _V
45 fveq1
 |-  ( f = B -> ( f ` w ) = ( B ` w ) )
46 45 eleq1d
 |-  ( f = B -> ( ( f ` w ) e. w <-> ( B ` w ) e. w ) )
47 46 imbi2d
 |-  ( f = B -> ( ( w =/= (/) -> ( f ` w ) e. w ) <-> ( w =/= (/) -> ( B ` w ) e. w ) ) )
48 47 ralbidv
 |-  ( f = B -> ( A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) <-> A. w e. h ( w =/= (/) -> ( B ` w ) e. w ) ) )
49 44 48 spcev
 |-  ( A. w e. h ( w =/= (/) -> ( B ` w ) e. w ) -> E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) )
50 41 49 syl
 |-  ( A. z e. A E! v v e. ( z i^i y ) -> E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) )
51 50 exlimiv
 |-  ( E. y A. z e. A E! v v e. ( z i^i y ) -> E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) )
52 4 51 syl
 |-  ( ph -> E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) )