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