NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  brimage GIF version

Theorem brimage 5793
Description: Binary relationship over the image function. (Contributed by SF, 11-Feb-2015.)
Hypotheses
Ref Expression
brimage.1 A V
brimage.2 B V
Assertion
Ref Expression
brimage (AImageRBB = (RA))

Proof of Theorem brimage
Dummy variables x y t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elima1c 4947 . . . 4 (A, B (( Ins2 S Ins3 ( S SI R)) “ 1c) ↔ x{x}, A, B ( Ins2 S Ins3 ( S SI R)))
2 elsymdif 3223 . . . . . 6 ({x}, A, B ( Ins2 S Ins3 ( S SI R)) ↔ ¬ ({x}, A, B Ins2 S {x}, A, B Ins3 ( S SI R)))
3 brimage.1 . . . . . . . . 9 A V
43otelins2 5791 . . . . . . . 8 ({x}, A, B Ins2 S {x}, B S )
5 vex 2862 . . . . . . . . 9 x V
6 brimage.2 . . . . . . . . 9 B V
75, 6opelssetsn 4760 . . . . . . . 8 ({x}, B S x B)
84, 7bitri 240 . . . . . . 7 ({x}, A, B Ins2 S x B)
96otelins3 5792 . . . . . . . 8 ({x}, A, B Ins3 ( S SI R) ↔ {x}, A ( S SI R))
10 brcnv 4892 . . . . . . . . . . . . . 14 ({x} SI Rtt SI R{x})
115brsnsi2 5776 . . . . . . . . . . . . . 14 (t SI R{x} ↔ y(t = {y} yRx))
1210, 11bitri 240 . . . . . . . . . . . . 13 ({x} SI Rty(t = {y} yRx))
1312anbi1i 676 . . . . . . . . . . . 12 (({x} SI Rt t S A) ↔ (y(t = {y} yRx) t S A))
14 19.41v 1901 . . . . . . . . . . . 12 (y((t = {y} yRx) t S A) ↔ (y(t = {y} yRx) t S A))
1513, 14bitr4i 243 . . . . . . . . . . 11 (({x} SI Rt t S A) ↔ y((t = {y} yRx) t S A))
1615exbii 1582 . . . . . . . . . 10 (t({x} SI Rt t S A) ↔ ty((t = {y} yRx) t S A))
17 excom 1741 . . . . . . . . . 10 (ty((t = {y} yRx) t S A) ↔ yt((t = {y} yRx) t S A))
18 anass 630 . . . . . . . . . . . . 13 (((t = {y} yRx) t S A) ↔ (t = {y} (yRx t S A)))
1918exbii 1582 . . . . . . . . . . . 12 (t((t = {y} yRx) t S A) ↔ t(t = {y} (yRx t S A)))
20 snex 4111 . . . . . . . . . . . . 13 {y} V
21 breq1 4642 . . . . . . . . . . . . . . 15 (t = {y} → (t S A ↔ {y} S A))
2221anbi2d 684 . . . . . . . . . . . . . 14 (t = {y} → ((yRx t S A) ↔ (yRx {y} S A)))
23 ancom 437 . . . . . . . . . . . . . . 15 ((yRx {y} S A) ↔ ({y} S A yRx))
24 vex 2862 . . . . . . . . . . . . . . . . 17 y V
2524, 3brssetsn 4759 . . . . . . . . . . . . . . . 16 ({y} S Ay A)
2625anbi1i 676 . . . . . . . . . . . . . . 15 (({y} S A yRx) ↔ (y A yRx))
2723, 26bitri 240 . . . . . . . . . . . . . 14 ((yRx {y} S A) ↔ (y A yRx))
2822, 27syl6bb 252 . . . . . . . . . . . . 13 (t = {y} → ((yRx t S A) ↔ (y A yRx)))
2920, 28ceqsexv 2894 . . . . . . . . . . . 12 (t(t = {y} (yRx t S A)) ↔ (y A yRx))
3019, 29bitri 240 . . . . . . . . . . 11 (t((t = {y} yRx) t S A) ↔ (y A yRx))
3130exbii 1582 . . . . . . . . . 10 (yt((t = {y} yRx) t S A) ↔ y(y A yRx))
3216, 17, 313bitri 262 . . . . . . . . 9 (t({x} SI Rt t S A) ↔ y(y A yRx))
33 opelco 4884 . . . . . . . . 9 ({x}, A ( S SI R) ↔ t({x} SI Rt t S A))
34 elima2 4755 . . . . . . . . 9 (x (RA) ↔ y(y A yRx))
3532, 33, 343bitr4i 268 . . . . . . . 8 ({x}, A ( S SI R) ↔ x (RA))
369, 35bitri 240 . . . . . . 7 ({x}, A, B Ins3 ( S SI R) ↔ x (RA))
378, 36bibi12i 306 . . . . . 6 (({x}, A, B Ins2 S {x}, A, B Ins3 ( S SI R)) ↔ (x Bx (RA)))
382, 37xchbinx 301 . . . . 5 ({x}, A, B ( Ins2 S Ins3 ( S SI R)) ↔ ¬ (x Bx (RA)))
3938exbii 1582 . . . 4 (x{x}, A, B ( Ins2 S Ins3 ( S SI R)) ↔ x ¬ (x Bx (RA)))
40 exnal 1574 . . . 4 (x ¬ (x Bx (RA)) ↔ ¬ x(x Bx (RA)))
411, 39, 403bitri 262 . . 3 (A, B (( Ins2 S Ins3 ( S SI R)) “ 1c) ↔ ¬ x(x Bx (RA)))
4241con2bii 322 . 2 (x(x Bx (RA)) ↔ ¬ A, B (( Ins2 S Ins3 ( S SI R)) “ 1c))
43 dfcleq 2347 . 2 (B = (RA) ↔ x(x Bx (RA)))
44 df-image 5754 . . . 4 ImageR = ∼ (( Ins2 S Ins3 ( S SI R)) “ 1c)
4544breqi 4645 . . 3 (AImageRBA ∼ (( Ins2 S Ins3 ( S SI R)) “ 1c)B)
46 df-br 4640 . . 3 (A ∼ (( Ins2 S Ins3 ( S SI R)) “ 1c)BA, B ∼ (( Ins2 S Ins3 ( S SI R)) “ 1c))
473, 6opex 4588 . . . 4 A, B V
4847elcompl 3225 . . 3 (A, B ∼ (( Ins2 S Ins3 ( S SI R)) “ 1c) ↔ ¬ A, B (( Ins2 S Ins3 ( S SI R)) “ 1c))
4945, 46, 483bitri 262 . 2 (AImageRB ↔ ¬ A, B (( Ins2 S Ins3 ( S SI R)) “ 1c))
5042, 43, 493bitr4ri 269 1 (AImageRBB = (RA))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 176   wa 358  wal 1540  wex 1541   = wceq 1642   wcel 1710  Vcvv 2859  ccompl 3205  csymdif 3209  {csn 3737  1cc1c 4134  cop 4561   class class class wbr 4639   S csset 4719   SI csi 4720   ccom 4721  cima 4722  ccnv 4771   Ins2 cins2 5749   Ins3 cins3 5751  Imagecimage 5753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-sset 4725  df-co 4726  df-ima 4727  df-si 4728  df-cnv 4785  df-2nd 4797  df-txp 5736  df-ins2 5750  df-ins3 5752  df-image 5754
This theorem is referenced by:  fnsex  5832  clos1ex  5876  mapexi  6003  enex  6031  ovcelem1  6171  ceex  6174  nchoicelem10  6298
  Copyright terms: Public domain W3C validator