Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj1379 Unicode version

Theorem bnj1379 28863
Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj1379.1  |-  ( ph  <->  A. f  e.  A  Fun  f )
bnj1379.2  |-  D  =  ( dom  f  i^i 
dom  g )
bnj1379.3  |-  ( ps  <->  (
ph  /\  A. f  e.  A  A. g  e.  A  ( f  |`  D )  =  ( g  |`  D )
) )
bnj1379.5  |-  ( ch  <->  ( ps  /\  <. x ,  y >.  e.  U. A  /\  <. x ,  z
>.  e.  U. A ) )
bnj1379.6  |-  ( th  <->  ( ch  /\  f  e.  A  /\  <. x ,  y >.  e.  f ) )
bnj1379.7  |-  ( ta  <->  ( th  /\  g  e.  A  /\  <. x ,  z >.  e.  g ) )
Assertion
Ref Expression
bnj1379  |-  ( ps 
->  Fun  U. A )
Distinct variable groups:    A, f,
g, x, y, z   
x, D    ph, g    ps, x, y, z
Allowed substitution hints:    ph( x, y, z, f)    ps( f,
g)    ch( x, y, z, f, g)    th( x, y, z, f, g)    ta( x, y, z, f, g)    D( y, z, f, g)

Proof of Theorem bnj1379
StepHypRef Expression
1 bnj1379.3 . . . . 5  |-  ( ps  <->  (
ph  /\  A. f  e.  A  A. g  e.  A  ( f  |`  D )  =  ( g  |`  D )
) )
2 bnj1379.1 . . . . . . . 8  |-  ( ph  <->  A. f  e.  A  Fun  f )
32bnj1095 28813 . . . . . . 7  |-  ( ph  ->  A. f ph )
43nfi 1538 . . . . . 6  |-  F/ f
ph
5 nfra1 2593 . . . . . 6  |-  F/ f A. f  e.  A  A. g  e.  A  ( f  |`  D )  =  ( g  |`  D )
64, 5nfan 1771 . . . . 5  |-  F/ f ( ph  /\  A. f  e.  A  A. g  e.  A  (
f  |`  D )  =  ( g  |`  D ) )
71, 6nfxfr 1557 . . . 4  |-  F/ f ps
82bnj946 28806 . . . . . . . 8  |-  ( ph  <->  A. f ( f  e.  A  ->  Fun  f ) )
98biimpi 186 . . . . . . 7  |-  ( ph  ->  A. f ( f  e.  A  ->  Fun  f ) )
10919.21bi 1794 . . . . . 6  |-  ( ph  ->  ( f  e.  A  ->  Fun  f ) )
111, 10bnj832 28787 . . . . 5  |-  ( ps 
->  ( f  e.  A  ->  Fun  f ) )
12 funrel 5272 . . . . 5  |-  ( Fun  f  ->  Rel  f )
1311, 12syl6 29 . . . 4  |-  ( ps 
->  ( f  e.  A  ->  Rel  f ) )
147, 13ralrimi 2624 . . 3  |-  ( ps 
->  A. f  e.  A  Rel  f )
15 reluni 4808 . . 3  |-  ( Rel  U. A  <->  A. f  e.  A  Rel  f )
1614, 15sylibr 203 . 2  |-  ( ps 
->  Rel  U. A )
17 bnj1379.5 . . . . . 6  |-  ( ch  <->  ( ps  /\  <. x ,  y >.  e.  U. A  /\  <. x ,  z
>.  e.  U. A ) )
18 eluni2 3831 . . . . . . . . . . . 12  |-  ( <.
x ,  y >.  e.  U. A  <->  E. f  e.  A  <. x ,  y >.  e.  f
)
1918biimpi 186 . . . . . . . . . . 11  |-  ( <.
x ,  y >.  e.  U. A  ->  E. f  e.  A  <. x ,  y >.  e.  f
)
2019bnj1196 28827 . . . . . . . . . 10  |-  ( <.
x ,  y >.  e.  U. A  ->  E. f
( f  e.  A  /\  <. x ,  y
>.  e.  f ) )
2117, 20bnj836 28790 . . . . . . . . 9  |-  ( ch 
->  E. f ( f  e.  A  /\  <. x ,  y >.  e.  f ) )
22 bnj1379.6 . . . . . . . . 9  |-  ( th  <->  ( ch  /\  f  e.  A  /\  <. x ,  y >.  e.  f ) )
23 nfv 1605 . . . . . . . . . . . 12  |-  F/ f
<. x ,  y >.  e.  U. A
24 nfv 1605 . . . . . . . . . . . 12  |-  F/ f
<. x ,  z >.  e.  U. A
257, 23, 24nf3an 1774 . . . . . . . . . . 11  |-  F/ f ( ps  /\  <. x ,  y >.  e.  U. A  /\  <. x ,  z
>.  e.  U. A )
2617, 25nfxfr 1557 . . . . . . . . . 10  |-  F/ f ch
2726nfri 1742 . . . . . . . . 9  |-  ( ch 
->  A. f ch )
2821, 22, 27bnj1345 28857 . . . . . . . 8  |-  ( ch 
->  E. f th )
2917simp3bi 972 . . . . . . . . . . . . 13  |-  ( ch 
->  <. x ,  z
>.  e.  U. A )
3022, 29bnj835 28789 . . . . . . . . . . . 12  |-  ( th 
->  <. x ,  z
>.  e.  U. A )
31 eluni2 3831 . . . . . . . . . . . . . 14  |-  ( <.
x ,  z >.  e.  U. A  <->  E. g  e.  A  <. x ,  z >.  e.  g
)
3231biimpi 186 . . . . . . . . . . . . 13  |-  ( <.
x ,  z >.  e.  U. A  ->  E. g  e.  A  <. x ,  z >.  e.  g
)
3332bnj1196 28827 . . . . . . . . . . . 12  |-  ( <.
x ,  z >.  e.  U. A  ->  E. g
( g  e.  A  /\  <. x ,  z
>.  e.  g ) )
3430, 33syl 15 . . . . . . . . . . 11  |-  ( th 
->  E. g ( g  e.  A  /\  <. x ,  z >.  e.  g ) )
35 bnj1379.7 . . . . . . . . . . 11  |-  ( ta  <->  ( th  /\  g  e.  A  /\  <. x ,  z >.  e.  g ) )
36 nfv 1605 . . . . . . . . . . . . . . . . . 18  |-  F/ g
ph
37 nfcv 2419 . . . . . . . . . . . . . . . . . . 19  |-  F/_ g A
38 nfra1 2593 . . . . . . . . . . . . . . . . . . 19  |-  F/ g A. g  e.  A  ( f  |`  D )  =  ( g  |`  D )
3937, 38nfral 2596 . . . . . . . . . . . . . . . . . 18  |-  F/ g A. f  e.  A  A. g  e.  A  ( f  |`  D )  =  ( g  |`  D )
4036, 39nfan 1771 . . . . . . . . . . . . . . . . 17  |-  F/ g ( ph  /\  A. f  e.  A  A. g  e.  A  (
f  |`  D )  =  ( g  |`  D ) )
411, 40nfxfr 1557 . . . . . . . . . . . . . . . 16  |-  F/ g ps
42 nfv 1605 . . . . . . . . . . . . . . . 16  |-  F/ g
<. x ,  y >.  e.  U. A
43 nfv 1605 . . . . . . . . . . . . . . . 16  |-  F/ g
<. x ,  z >.  e.  U. A
4441, 42, 43nf3an 1774 . . . . . . . . . . . . . . 15  |-  F/ g ( ps  /\  <. x ,  y >.  e.  U. A  /\  <. x ,  z
>.  e.  U. A )
4517, 44nfxfr 1557 . . . . . . . . . . . . . 14  |-  F/ g ch
46 nfv 1605 . . . . . . . . . . . . . 14  |-  F/ g  f  e.  A
47 nfv 1605 . . . . . . . . . . . . . 14  |-  F/ g
<. x ,  y >.  e.  f
4845, 46, 47nf3an 1774 . . . . . . . . . . . . 13  |-  F/ g ( ch  /\  f  e.  A  /\  <. x ,  y >.  e.  f )
4922, 48nfxfr 1557 . . . . . . . . . . . 12  |-  F/ g th
5049nfri 1742 . . . . . . . . . . 11  |-  ( th 
->  A. g th )
5134, 35, 50bnj1345 28857 . . . . . . . . . 10  |-  ( th 
->  E. g ta )
521simprbi 450 . . . . . . . . . . . . . . . . . 18  |-  ( ps 
->  A. f  e.  A  A. g  e.  A  ( f  |`  D )  =  ( g  |`  D ) )
5317, 52bnj835 28789 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  A. f  e.  A  A. g  e.  A  ( f  |`  D )  =  ( g  |`  D ) )
5422, 53bnj835 28789 . . . . . . . . . . . . . . . 16  |-  ( th 
->  A. f  e.  A  A. g  e.  A  ( f  |`  D )  =  ( g  |`  D ) )
5535, 54bnj835 28789 . . . . . . . . . . . . . . 15  |-  ( ta 
->  A. f  e.  A  A. g  e.  A  ( f  |`  D )  =  ( g  |`  D ) )
5622, 35bnj1219 28833 . . . . . . . . . . . . . . 15  |-  ( ta 
->  f  e.  A
)
5755, 56bnj1294 28850 . . . . . . . . . . . . . 14  |-  ( ta 
->  A. g  e.  A  ( f  |`  D )  =  ( g  |`  D ) )
5835simp2bi 971 . . . . . . . . . . . . . 14  |-  ( ta 
->  g  e.  A
)
5957, 58bnj1294 28850 . . . . . . . . . . . . 13  |-  ( ta 
->  ( f  |`  D )  =  ( g  |`  D ) )
6059fveq1d 5527 . . . . . . . . . . . 12  |-  ( ta 
->  ( ( f  |`  D ) `  x
)  =  ( ( g  |`  D ) `  x ) )
6122simp3bi 972 . . . . . . . . . . . . . . . . 17  |-  ( th 
->  <. x ,  y
>.  e.  f )
6235, 61bnj835 28789 . . . . . . . . . . . . . . . 16  |-  ( ta 
->  <. x ,  y
>.  e.  f )
63 vex 2791 . . . . . . . . . . . . . . . . 17  |-  x  e. 
_V
64 vex 2791 . . . . . . . . . . . . . . . . 17  |-  y  e. 
_V
6563, 64opeldm 4882 . . . . . . . . . . . . . . . 16  |-  ( <.
x ,  y >.  e.  f  ->  x  e. 
dom  f )
6662, 65syl 15 . . . . . . . . . . . . . . 15  |-  ( ta 
->  x  e.  dom  f )
67 vex 2791 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
6863, 67opeldm 4882 . . . . . . . . . . . . . . . 16  |-  ( <.
x ,  z >.  e.  g  ->  x  e. 
dom  g )
6935, 68bnj837 28791 . . . . . . . . . . . . . . 15  |-  ( ta 
->  x  e.  dom  g )
7066, 69bnj1153 28825 . . . . . . . . . . . . . 14  |-  ( ta 
->  x  e.  ( dom  f  i^i  dom  g
) )
71 bnj1379.2 . . . . . . . . . . . . . 14  |-  D  =  ( dom  f  i^i 
dom  g )
7270, 71syl6eleqr 2374 . . . . . . . . . . . . 13  |-  ( ta 
->  x  e.  D
)
73 fvres 5542 . . . . . . . . . . . . 13  |-  ( x  e.  D  ->  (
( f  |`  D ) `
 x )  =  ( f `  x
) )
7472, 73syl 15 . . . . . . . . . . . 12  |-  ( ta 
->  ( ( f  |`  D ) `  x
)  =  ( f `
 x ) )
75 fvres 5542 . . . . . . . . . . . . 13  |-  ( x  e.  D  ->  (
( g  |`  D ) `
 x )  =  ( g `  x
) )
7672, 75syl 15 . . . . . . . . . . . 12  |-  ( ta 
->  ( ( g  |`  D ) `  x
)  =  ( g `
 x ) )
7760, 74, 763eqtr3d 2323 . . . . . . . . . . 11  |-  ( ta 
->  ( f `  x
)  =  ( g `
 x ) )
782biimpi 186 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. f  e.  A  Fun  f )
791, 78bnj832 28787 . . . . . . . . . . . . . . . 16  |-  ( ps 
->  A. f  e.  A  Fun  f )
8017, 79bnj835 28789 . . . . . . . . . . . . . . 15  |-  ( ch 
->  A. f  e.  A  Fun  f )
8122, 80bnj835 28789 . . . . . . . . . . . . . 14  |-  ( th 
->  A. f  e.  A  Fun  f )
8235, 81bnj835 28789 . . . . . . . . . . . . 13  |-  ( ta 
->  A. f  e.  A  Fun  f )
8382, 56bnj1294 28850 . . . . . . . . . . . 12  |-  ( ta 
->  Fun  f )
84 funopfv 5562 . . . . . . . . . . . 12  |-  ( Fun  f  ->  ( <. x ,  y >.  e.  f  ->  ( f `  x )  =  y ) )
8583, 62, 84sylc 56 . . . . . . . . . . 11  |-  ( ta 
->  ( f `  x
)  =  y )
86 funeq 5274 . . . . . . . . . . . . . . 15  |-  ( f  =  g  ->  ( Fun  f  <->  Fun  g ) )
8786cbvralv 2764 . . . . . . . . . . . . . 14  |-  ( A. f  e.  A  Fun  f 
<-> 
A. g  e.  A  Fun  g )
8882, 87sylib 188 . . . . . . . . . . . . 13  |-  ( ta 
->  A. g  e.  A  Fun  g )
8988, 58bnj1294 28850 . . . . . . . . . . . 12  |-  ( ta 
->  Fun  g )
9035simp3bi 972 . . . . . . . . . . . 12  |-  ( ta 
->  <. x ,  z
>.  e.  g )
91 funopfv 5562 . . . . . . . . . . . 12  |-  ( Fun  g  ->  ( <. x ,  z >.  e.  g  ->  ( g `  x )  =  z ) )
9289, 90, 91sylc 56 . . . . . . . . . . 11  |-  ( ta 
->  ( g `  x
)  =  z )
9377, 85, 923eqtr3d 2323 . . . . . . . . . 10  |-  ( ta 
->  y  =  z
)
9451, 93bnj593 28774 . . . . . . . . 9  |-  ( th 
->  E. g  y  =  z )
9594bnj937 28803 . . . . . . . 8  |-  ( th 
->  y  =  z
)
9628, 95bnj593 28774 . . . . . . 7  |-  ( ch 
->  E. f  y  =  z )
9796bnj937 28803 . . . . . 6  |-  ( ch 
->  y  =  z
)
9817, 97sylbir 204 . . . . 5  |-  ( ( ps  /\  <. x ,  y >.  e.  U. A  /\  <. x ,  z
>.  e.  U. A )  ->  y  =  z )
99983expib 1154 . . . 4  |-  ( ps 
->  ( ( <. x ,  y >.  e.  U. A  /\  <. x ,  z
>.  e.  U. A )  ->  y  =  z ) )
10099alrimivv 1618 . . 3  |-  ( ps 
->  A. y A. z
( ( <. x ,  y >.  e.  U. A  /\  <. x ,  z
>.  e.  U. A )  ->  y  =  z ) )
101100alrimiv 1617 . 2  |-  ( ps 
->  A. x A. y A. z ( ( <.
x ,  y >.  e.  U. A  /\  <. x ,  z >.  e.  U. A )  ->  y  =  z ) )
102 dffun4 5267 . 2  |-  ( Fun  U. A  <->  ( Rel  U. A  /\  A. x A. y A. z ( (
<. x ,  y >.  e.  U. A  /\  <. x ,  z >.  e.  U. A )  ->  y  =  z ) ) )
10316, 101, 102sylanbrc 645 1  |-  ( ps 
->  Fun  U. A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934   A.wal 1527   E.wex 1528    = wceq 1623    e. wcel 1684   A.wral 2543   E.wrex 2544    i^i cin 3151   <.cop 3643   U.cuni 3827   dom cdm 4689    |` cres 4691   Rel wrel 4694   Fun wfun 5249   ` cfv 5255
This theorem is referenced by:  bnj1383  28864
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-res 4701  df-iota 5219  df-fun 5257  df-fv 5263
  Copyright terms: Public domain W3C validator