ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  funimaexglem Unicode version

Theorem funimaexglem 5064
Description: Lemma for funimaexg 5065. It constitutes the interesting part of funimaexg 5065, in which  B 
C_  dom  A. (Contributed by Jim Kingdon, 27-Dec-2018.)
Assertion
Ref Expression
funimaexglem  |-  ( ( Fun  A  /\  B  e.  C  /\  B  C_  dom  A )  ->  ( A " B )  e. 
_V )

Proof of Theorem funimaexglem
Dummy variables  b  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dffun7 5009 . . . . . . . . . 10  |-  ( Fun 
A  <->  ( Rel  A  /\  A. x  e.  dom  A E* y  x A y ) )
21simprbi 269 . . . . . . . . 9  |-  ( Fun 
A  ->  A. x  e.  dom  A E* y  x A y )
323ad2ant1 962 . . . . . . . 8  |-  ( ( Fun  A  /\  B  e.  C  /\  B  C_  dom  A )  ->  A. x  e.  dom  A E* y  x A y )
4 ssralv 3074 . . . . . . . . 9  |-  ( B 
C_  dom  A  ->  ( A. x  e.  dom  A E* y  x A y  ->  A. x  e.  B  E* y  x A y ) )
543ad2ant3 964 . . . . . . . 8  |-  ( ( Fun  A  /\  B  e.  C  /\  B  C_  dom  A )  ->  ( A. x  e.  dom  A E* y  x A y  ->  A. x  e.  B  E* y  x A y ) )
63, 5mpd 13 . . . . . . 7  |-  ( ( Fun  A  /\  B  e.  C  /\  B  C_  dom  A )  ->  A. x  e.  B  E* y  x A y )
76alrimiv 1799 . . . . . 6  |-  ( ( Fun  A  /\  B  e.  C  /\  B  C_  dom  A )  ->  A. z A. x  e.  B  E* y  x A
y )
8 sseq1 3036 . . . . . . . . . . . . . . . . 17  |-  ( b  =  B  ->  (
b  C_  dom  A  <->  B  C_  dom  A ) )
98biimpar 291 . . . . . . . . . . . . . . . 16  |-  ( ( b  =  B  /\  B  C_  dom  A )  ->  b  C_  dom  A )
1093adant1 959 . . . . . . . . . . . . . . 15  |-  ( ( Fun  A  /\  b  =  B  /\  B  C_  dom  A )  ->  b  C_ 
dom  A )
11 simp1 941 . . . . . . . . . . . . . . 15  |-  ( ( Fun  A  /\  b  =  B  /\  B  C_  dom  A )  ->  Fun  A )
1210, 11jca 300 . . . . . . . . . . . . . 14  |-  ( ( Fun  A  /\  b  =  B  /\  B  C_  dom  A )  ->  (
b  C_  dom  A  /\  Fun  A ) )
13 dffun8 5010 . . . . . . . . . . . . . . . . . 18  |-  ( Fun 
A  <->  ( Rel  A  /\  A. x  e.  dom  A E! y  x A y ) )
1413simprbi 269 . . . . . . . . . . . . . . . . 17  |-  ( Fun 
A  ->  A. x  e.  dom  A E! y  x A y )
1514adantl 271 . . . . . . . . . . . . . . . 16  |-  ( ( b  C_  dom  A  /\  Fun  A )  ->  A. x  e.  dom  A E! y  x A y )
16 ssel 3008 . . . . . . . . . . . . . . . . 17  |-  ( b 
C_  dom  A  ->  ( x  e.  b  ->  x  e.  dom  A ) )
1716adantr 270 . . . . . . . . . . . . . . . 16  |-  ( ( b  C_  dom  A  /\  Fun  A )  ->  (
x  e.  b  ->  x  e.  dom  A ) )
18 rsp 2419 . . . . . . . . . . . . . . . 16  |-  ( A. x  e.  dom  A E! y  x A y  ->  ( x  e. 
dom  A  ->  E! y  x A y ) )
1915, 17, 18sylsyld 57 . . . . . . . . . . . . . . 15  |-  ( ( b  C_  dom  A  /\  Fun  A )  ->  (
x  e.  b  ->  E! y  x A
y ) )
2019ralrimiv 2441 . . . . . . . . . . . . . 14  |-  ( ( b  C_  dom  A  /\  Fun  A )  ->  A. x  e.  b  E! y  x A y )
21 zfrep6 3933 . . . . . . . . . . . . . 14  |-  ( A. x  e.  b  E! y  x A y  ->  E. z A. x  e.  b  E. y  e.  z  x A y )
2212, 20, 213syl 17 . . . . . . . . . . . . 13  |-  ( ( Fun  A  /\  b  =  B  /\  B  C_  dom  A )  ->  E. z A. x  e.  b  E. y  e.  z  x A y )
23 raleq 2558 . . . . . . . . . . . . . . 15  |-  ( b  =  B  ->  ( A. x  e.  b  E. y  e.  z  x A y  <->  A. x  e.  B  E. y  e.  z  x A
y ) )
2423exbidv 1750 . . . . . . . . . . . . . 14  |-  ( b  =  B  ->  ( E. z A. x  e.  b  E. y  e.  z  x A y  <->  E. z A. x  e.  B  E. y  e.  z  x A y ) )
25243ad2ant2 963 . . . . . . . . . . . . 13  |-  ( ( Fun  A  /\  b  =  B  /\  B  C_  dom  A )  ->  ( E. z A. x  e.  b  E. y  e.  z  x A y  <->  E. z A. x  e.  B  E. y  e.  z  x A y ) )
2622, 25mpbid 145 . . . . . . . . . . . 12  |-  ( ( Fun  A  /\  b  =  B  /\  B  C_  dom  A )  ->  E. z A. x  e.  B  E. y  e.  z  x A y )
27263com12 1145 . . . . . . . . . . 11  |-  ( ( b  =  B  /\  Fun  A  /\  B  C_  dom  A )  ->  E. z A. x  e.  B  E. y  e.  z  x A y )
28273expib 1144 . . . . . . . . . 10  |-  ( b  =  B  ->  (
( Fun  A  /\  B  C_  dom  A )  ->  E. z A. x  e.  B  E. y  e.  z  x A
y ) )
2928vtocleg 2683 . . . . . . . . 9  |-  ( B  e.  C  ->  (
( Fun  A  /\  B  C_  dom  A )  ->  E. z A. x  e.  B  E. y  e.  z  x A
y ) )
30293impib 1139 . . . . . . . 8  |-  ( ( B  e.  C  /\  Fun  A  /\  B  C_  dom  A )  ->  E. z A. x  e.  B  E. y  e.  z  x A y )
31303com12 1145 . . . . . . 7  |-  ( ( Fun  A  /\  B  e.  C  /\  B  C_  dom  A )  ->  E. z A. x  e.  B  E. y  e.  z  x A y )
32 df-rex 2361 . . . . . . . . . 10  |-  ( E. y  e.  z  x A y  <->  E. y
( y  e.  z  /\  x A y ) )
33 exancom 1542 . . . . . . . . . 10  |-  ( E. y ( y  e.  z  /\  x A y )  <->  E. y
( x A y  /\  y  e.  z ) )
3432, 33bitri 182 . . . . . . . . 9  |-  ( E. y  e.  z  x A y  <->  E. y
( x A y  /\  y  e.  z ) )
3534ralbii 2380 . . . . . . . 8  |-  ( A. x  e.  B  E. y  e.  z  x A y  <->  A. x  e.  B  E. y
( x A y  /\  y  e.  z ) )
3635exbii 1539 . . . . . . 7  |-  ( E. z A. x  e.  B  E. y  e.  z  x A y  <->  E. z A. x  e.  B  E. y ( x A y  /\  y  e.  z )
)
3731, 36sylib 120 . . . . . 6  |-  ( ( Fun  A  /\  B  e.  C  /\  B  C_  dom  A )  ->  E. z A. x  e.  B  E. y ( x A y  /\  y  e.  z ) )
38 19.29 1554 . . . . . . 7  |-  ( ( A. z A. x  e.  B  E* y  x A y  /\  E. z A. x  e.  B  E. y ( x A y  /\  y  e.  z ) )  ->  E. z ( A. x  e.  B  E* y  x A y  /\  A. x  e.  B  E. y ( x A y  /\  y  e.  z ) ) )
39 nfcv 2225 . . . . . . . . . . 11  |-  F/_ y B
40 nfmo1 1957 . . . . . . . . . . 11  |-  F/ y E* y  x A y
4139, 40nfralxy 2410 . . . . . . . . . 10  |-  F/ y A. x  e.  B  E* y  x A
y
42 nfe1 1428 . . . . . . . . . . 11  |-  F/ y E. y ( x A y  /\  y  e.  z )
4339, 42nfralxy 2410 . . . . . . . . . 10  |-  F/ y A. x  e.  B  E. y ( x A y  /\  y  e.  z )
4441, 43nfan 1500 . . . . . . . . 9  |-  F/ y ( A. x  e.  B  E* y  x A y  /\  A. x  e.  B  E. y ( x A y  /\  y  e.  z ) )
45 r19.26 2493 . . . . . . . . . 10  |-  ( A. x  e.  B  ( E* y  x A
y  /\  E. y
( x A y  /\  y  e.  z ) )  <->  ( A. x  e.  B  E* y  x A y  /\  A. x  e.  B  E. y ( x A y  /\  y  e.  z ) ) )
46 mopick 2023 . . . . . . . . . . 11  |-  ( ( E* y  x A y  /\  E. y
( x A y  /\  y  e.  z ) )  ->  (
x A y  -> 
y  e.  z ) )
4746ralimi 2434 . . . . . . . . . 10  |-  ( A. x  e.  B  ( E* y  x A
y  /\  E. y
( x A y  /\  y  e.  z ) )  ->  A. x  e.  B  ( x A y  ->  y  e.  z ) )
4845, 47sylbir 133 . . . . . . . . 9  |-  ( ( A. x  e.  B  E* y  x A
y  /\  A. x  e.  B  E. y
( x A y  /\  y  e.  z ) )  ->  A. x  e.  B  ( x A y  ->  y  e.  z ) )
4944, 48alrimi 1458 . . . . . . . 8  |-  ( ( A. x  e.  B  E* y  x A
y  /\  A. x  e.  B  E. y
( x A y  /\  y  e.  z ) )  ->  A. y A. x  e.  B  ( x A y  ->  y  e.  z ) )
5049eximi 1534 . . . . . . 7  |-  ( E. z ( A. x  e.  B  E* y  x A y  /\  A. x  e.  B  E. y ( x A y  /\  y  e.  z ) )  ->  E. z A. y A. x  e.  B  (
x A y  -> 
y  e.  z ) )
5138, 50syl 14 . . . . . 6  |-  ( ( A. z A. x  e.  B  E* y  x A y  /\  E. z A. x  e.  B  E. y ( x A y  /\  y  e.  z ) )  ->  E. z A. y A. x  e.  B  (
x A y  -> 
y  e.  z ) )
527, 37, 51syl2anc 403 . . . . 5  |-  ( ( Fun  A  /\  B  e.  C  /\  B  C_  dom  A )  ->  E. z A. y A. x  e.  B  ( x A y  ->  y  e.  z ) )
53 r19.23v 2477 . . . . . . 7  |-  ( A. x  e.  B  (
x A y  -> 
y  e.  z )  <-> 
( E. x  e.  B  x A y  ->  y  e.  z ) )
5453albii 1402 . . . . . 6  |-  ( A. y A. x  e.  B  ( x A y  ->  y  e.  z )  <->  A. y ( E. x  e.  B  x A y  ->  y  e.  z ) )
5554exbii 1539 . . . . 5  |-  ( E. z A. y A. x  e.  B  (
x A y  -> 
y  e.  z )  <->  E. z A. y ( E. x  e.  B  x A y  ->  y  e.  z ) )
5652, 55sylib 120 . . . 4  |-  ( ( Fun  A  /\  B  e.  C  /\  B  C_  dom  A )  ->  E. z A. y ( E. x  e.  B  x A
y  ->  y  e.  z ) )
57 abss 3079 . . . . 5  |-  ( { y  |  E. x  e.  B  x A
y }  C_  z  <->  A. y ( E. x  e.  B  x A
y  ->  y  e.  z ) )
5857exbii 1539 . . . 4  |-  ( E. z { y  |  E. x  e.  B  x A y }  C_  z 
<->  E. z A. y
( E. x  e.  B  x A y  ->  y  e.  z ) )
5956, 58sylibr 132 . . 3  |-  ( ( Fun  A  /\  B  e.  C  /\  B  C_  dom  A )  ->  E. z { y  |  E. x  e.  B  x A y }  C_  z )
60 dfima2 4745 . . . . 5  |-  ( A
" B )  =  { y  |  E. x  e.  B  x A y }
6160sseq1i 3039 . . . 4  |-  ( ( A " B ) 
C_  z  <->  { y  |  E. x  e.  B  x A y }  C_  z )
6261exbii 1539 . . 3  |-  ( E. z ( A " B )  C_  z  <->  E. z { y  |  E. x  e.  B  x A y }  C_  z )
6359, 62sylibr 132 . 2  |-  ( ( Fun  A  /\  B  e.  C  /\  B  C_  dom  A )  ->  E. z
( A " B
)  C_  z )
64 vex 2618 . . . 4  |-  z  e. 
_V
6564ssex 3953 . . 3  |-  ( ( A " B ) 
C_  z  ->  ( A " B )  e. 
_V )
6665exlimiv 1532 . 2  |-  ( E. z ( A " B )  C_  z  ->  ( A " B
)  e.  _V )
6763, 66syl 14 1  |-  ( ( Fun  A  /\  B  e.  C  /\  B  C_  dom  A )  ->  ( A " B )  e. 
_V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    /\ w3a 922   A.wal 1285    = wceq 1287   E.wex 1424    e. wcel 1436   E!weu 1945   E*wmo 1946   {cab 2071   A.wral 2355   E.wrex 2356   _Vcvv 2615    C_ wss 2988   class class class wbr 3822   dom cdm 4413   "cima 4416   Rel wrel 4418   Fun wfun 4977
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3931  ax-sep 3934  ax-pow 3986  ax-pr 4012
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-v 2617  df-un 2992  df-in 2994  df-ss 3001  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-br 3823  df-opab 3877  df-id 4096  df-xp 4419  df-cnv 4421  df-co 4422  df-dm 4423  df-rn 4424  df-res 4425  df-ima 4426  df-fun 4985
This theorem is referenced by:  funimaexg  5065
  Copyright terms: Public domain W3C validator