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

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 
|- ( 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 ) ) )
dfac5lem.3 
|- B = ( U. A 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 
 |-  ( 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 ) ) )
3 dfac5lem.3 
 |-  B = ( U. A i^i y )
4 1 2 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 3 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 imbitrdi 
 |-  ( 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 3 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 ) )