MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfac5lem5 Structured version   Visualization version   Unicode version
Theorem dfac5lem5 8950
Description: Lemma for dfac5 8951. (Contributed by NM, 12-Apr-2004.)
Hypotheses
Ref Expression
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
Ref Expression
dfac5lem5 |- ( ph -> E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) )
Distinct variable groups:   x, f, z, y, w, v, u, t, h   z, B, w, f   x, A, y, z, w
Allowed substitution hints:   ph( x, y, z, w, v, u, t, f, h)   A( v, u, t, f, h)   B( x, y, v, u, t, h)
Proof of Theorem dfac5lem5
Dummy variable g is distinct from all other variables.
StepHypRef Expression
1 dfac5lem.1 . . 3 |- A = { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) }
2 dfac5lem.2 . . 3 |- B = ( U. A i^i y )
3 dfac5lem.3 . . 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 ) ) )
41, 2, 3dfac5lem4 8949 . 2 |- ( ph -> E. y A. z e. A E! v v e. ( z i^i y ) )
5 simpr 477 . . . . . . . . . 10 |- ( ( w =/= (/) /\ w e. h ) -> w e. h )
65a1i 11 . . . . . . . . 9 |- ( A. z e. A E! v v e. ( z i^i y ) -> ( ( w =/= (/) /\ w e. h ) -> w e. h ) )
7 ineq1 3807 . . . . . . . . . . . . 13 |- ( z = ( { w } X. w ) -> ( z i^i y ) = ( ( { w } X. w ) i^i y ) )
87eleq2d 2687 . . . . . . . . . . . 12 |- ( z = ( { w } X. w ) -> ( v e. ( z i^i y ) <-> v e. ( ( { w } X. w ) i^i y ) ) )
98eubidv 2490 . . . . . . . . . . 11 |- ( z = ( { w } X. w ) -> ( E! v v e. ( z i^i y ) <-> E! v v e. ( ( { w } X. w ) i^i y ) ) )
109rspccv 3306 . . . . . . . . . 10 |- ( 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 ) ) )
111dfac5lem3 8948 . . . . . . . . . 10 |- ( ( { w } X. w ) e. A <-> ( w =/= (/) /\ w e. h ) )
12 dfac5lem1 8946 . . . . . . . . . 10 |- ( E! v v e. ( ( { w } X. w ) i^i y ) <-> E! g ( g e. w /\ <. w , g >. e. y ) )
1310, 11, 123imtr3g 284 . . . . . . . . 9 |- ( 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 ) ) )
146, 13jcad 555 . . . . . . . 8 |- ( 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 ) ) ) )
152eleq2i 2693 . . . . . . . . . . 11 |- ( <. w , g >. e. B <-> <. w , g >. e. ( U. A i^i y ) )
16 elin 3796 . . . . . . . . . . 11 |- ( <. w , g >. e. ( U. A i^i y ) <-> ( <. w , g >. e. U. A /\ <. w , g >. e. y ) )
171dfac5lem2 8947 . . . . . . . . . . . . 13 |- ( <. w , g >. e. U. A <-> ( w e. h /\ g e. w ) )
1817anbi1i 731 . . . . . . . . . . . 12 |- ( ( <. w , g >. e. U. A /\ <. w , g >. e. y ) <-> ( ( w e. h /\ g e. w ) /\ <. w , g >. e. y ) )
19 anass 681 . . . . . . . . . . . 12 |- ( ( ( w e. h /\ g e. w ) /\ <. w , g >. e. y ) <-> ( w e. h /\ ( g e. w /\ <. w , g >. e. y ) ) )
2018, 19bitri 264 . . . . . . . . . . 11 |- ( ( <. w , g >. e. U. A /\ <. w , g >. e. y ) <-> ( w e. h /\ ( g e. w /\ <. w , g >. e. y ) ) )
2115, 16, 203bitri 286 . . . . . . . . . 10 |- ( <. w , g >. e. B <-> ( w e. h /\ ( g e. w /\ <. w , g >. e. y ) ) )
2221eubii 2492 . . . . . . . . 9 |- ( E! g <. w , g >. e. B <-> E! g ( w e. h /\ ( g e. w /\ <. w , g >. e. y ) ) )
23 euanv 2534 . . . . . . . . 9 |- ( E! g ( w e. h /\ ( g e. w /\ <. w , g >. e. y ) ) <-> ( w e. h /\ E! g ( g e. w /\ <. w , g >. e. y ) ) )
2422, 23bitr2i 265 . . . . . . . 8 |- ( ( w e. h /\ E! g ( g e. w /\ <. w , g >. e. y ) ) <-> E! g <. w , g >. e. B )
2514, 24syl6ib 241 . . . . . . 7 |- ( A. z e. A E! v v e. ( z i^i y ) -> ( ( w =/= (/) /\ w e. h ) -> E! g <. w , g >. e. B ) )
26 euex 2494 . . . . . . . 8 |- ( E! g <. w , g >. e. B -> E. g <. w , g >. e. B )
27 nfeu1 2480 . . . . . . . . . 10 |- F/ g E! g <. w , g >. e. B
28 nfv 1843 . . . . . . . . . 10 |- F/ g ( B ` w ) e. w
2927, 28nfim 1825 . . . . . . . . 9 |- F/ g ( E! g <. w , g >. e. B -> ( B ` w ) e. w )
3021simprbi 480 . . . . . . . . . . 11 |- ( <. w , g >. e. B -> ( g e. w /\ <. w , g >. e. y ) )
3130simpld 475 . . . . . . . . . 10 |- ( <. w , g >. e. B -> g e. w )
32 tz6.12 6211 . . . . . . . . . . . . 13 |- ( ( <. w , g >. e. B /\ E! g <. w , g >. e. B ) -> ( B ` w ) = g )
3332eleq1d 2686 . . . . . . . . . . . 12 |- ( ( <. w , g >. e. B /\ E! g <. w , g >. e. B ) -> ( ( B ` w ) e. w <-> g e. w ) )
3433biimparc 504 . . . . . . . . . . 11 |- ( ( g e. w /\ ( <. w , g >. e. B /\ E! g <. w , g >. e. B ) ) -> ( B ` w ) e. w )
3534exp32 631 . . . . . . . . . 10 |- ( g e. w -> ( <. w , g >. e. B -> ( E! g <. w , g >. e. B -> ( B ` w ) e. w ) ) )
3631, 35mpcom 38 . . . . . . . . 9 |- ( <. w , g >. e. B -> ( E! g <. w , g >. e. B -> ( B ` w ) e. w ) )
3729, 36exlimi 2086 . . . . . . . 8 |- ( E. g <. w , g >. e. B -> ( E! g <. w , g >. e. B -> ( B ` w ) e. w ) )
3826, 37mpcom 38 . . . . . . 7 |- ( E! g <. w , g >. e. B -> ( B ` w ) e. w )
3925, 38syl6 35 . . . . . 6 |- ( A. z e. A E! v v e. ( z i^i y ) -> ( ( w =/= (/) /\ w e. h ) -> ( B ` w ) e. w ) )
4039expcomd 454 . . . . 5 |- ( A. z e. A E! v v e. ( z i^i y ) -> ( w e. h -> ( w =/= (/) -> ( B ` w ) e. w ) ) )
4140ralrimiv 2965 . . . 4 |- ( A. z e. A E! v v e. ( z i^i y ) -> A. w e. h ( w =/= (/) -> ( B ` w ) e. w ) )
42 vex 3203 . . . . . . 7 |- y e. _V
4342inex2 4800 . . . . . 6 |- ( U. A i^i y ) e. _V
442, 43eqeltri 2697 . . . . 5 |- B e. _V
45 fveq1 6190 . . . . . . . 8 |- ( f = B -> ( f ` w ) = ( B ` w ) )
4645eleq1d 2686 . . . . . . 7 |- ( f = B -> ( ( f ` w ) e. w <-> ( B ` w ) e. w ) )
4746imbi2d 330 . . . . . 6 |- ( f = B -> ( ( w =/= (/) -> ( f ` w ) e. w ) <-> ( w =/= (/) -> ( B ` w ) e. w ) ) )
4847ralbidv 2986 . . . . 5 |- ( f = B -> ( A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) <-> A. w e. h ( w =/= (/) -> ( B ` w ) e. w ) ) )
4944, 48spcev 3300 . . . 4 |- ( A. w e. h ( w =/= (/) -> ( B ` w ) e. w ) -> E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) )
5041, 49syl 17 . . 3 |- ( A. z e. A E! v v e. ( z i^i y ) -> E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) )
5150exlimiv 1858 . 2 |- ( 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 ) )
524, 51syl 17 1 |- ( ph -> E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   E!weu 2470   {cab 2608   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   i^i cin 3573   (/)c0 3915   {csn 4177   <.cop 4183   U.cuni 4436   X. cxp 5112   ` cfv 5888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-xp 5120  df-rel 5121  df-cnv 5122  df-dm 5124  df-rn 5125  df-iota 5851  df-fv 5896
This theorem is referenced by:  dfac5  8951
  Copyright terms: Public domain W3C validator