NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  dfimak2 Structured version   Unicode version

Theorem dfimak2 4298
Description: Alternate definition of Kuratowski image. This is the first of a series of definitions throughout the file designed to prove existence of various operations. (Contributed by SF, 14-Jan-2015.)
Assertion
Ref Expression
dfimak2 k P6 1c k SIk k

Proof of Theorem dfimak2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-rex 2620 . . . 4
2 exancom 1586 . . . 4
3 vex 2862 . . . . . . 7
4 elp6 4263 . . . . . . 7 P6 1c k SIk k 1c k SIk k
53, 4ax-mp 8 . . . . . 6 P6 1c k SIk k 1c k SIk k
6 elun 3220 . . . . . . . 8 1c k SIk k 1c k SIk k
7 opkex 4113 . . . . . . . . . . 11
87elcompl 3225 . . . . . . . . . 10 1c k 1c k
9 snex 4111 . . . . . . . . . . 11
10 vex 2862 . . . . . . . . . . . 12
1110, 9opkelxpk 4248 . . . . . . . . . . 11 1c k 1c
129, 11mpbiran2 885 . . . . . . . . . 10 1c k 1c
138, 12xchbinx 301 . . . . . . . . 9 1c k 1c
1413orbi1i 506 . . . . . . . 8 1c k SIk k 1c SIk k
15 iman 413 . . . . . . . . 9 1c SIk k 1c SIk k
16 imor 401 . . . . . . . . 9 1c SIk k 1c SIk k
17 el1c 4139 . . . . . . . . . . . 12 1c
1817anbi1i 676 . . . . . . . . . . 11 1c SIk k SIk k
19 19.41v 1901 . . . . . . . . . . 11 SIk k SIk k
2018, 19bitr4i 243 . . . . . . . . . 10 1c SIk k SIk k
2120notbii 287 . . . . . . . . 9 1c SIk k SIk k
2215, 16, 213bitr3i 266 . . . . . . . 8 1c SIk k SIk k
236, 14, 223bitri 262 . . . . . . 7 1c k SIk k SIk k
2423albii 1566 . . . . . 6 1c k SIk k SIk k
25 alnex 1543 . . . . . . 7 SIk k SIk k
26 excom 1741 . . . . . . . 8 SIk k SIk k
27 snex 4111 . . . . . . . . . . 11
28 opkeq1 4059 . . . . . . . . . . . . . 14
2928eleq1d 2419 . . . . . . . . . . . . 13 SIk k SIk k
30 vex 2862 . . . . . . . . . . . . . . 15
3130, 3opksnelsik 4265 . . . . . . . . . . . . . 14 SIk k k
32 opkex 4113 . . . . . . . . . . . . . . 15
3332elcompl 3225 . . . . . . . . . . . . . 14 k k
3431, 33bitri 240 . . . . . . . . . . . . 13 SIk k k
3529, 34syl6bb 252 . . . . . . . . . . . 12 SIk k k
3635notbid 285 . . . . . . . . . . 11 SIk k k
3727, 36ceqsexv 2894 . . . . . . . . . 10 SIk k k
38 elin 3219 . . . . . . . . . . 11 k k
39 notnot 282 . . . . . . . . . . 11 k k
4030, 3opkelxpk 4248 . . . . . . . . . . . . 13 k
413, 40mpbiran2 885 . . . . . . . . . . . 12 k
4241anbi2i 675 . . . . . . . . . . 11 k
4338, 39, 423bitr3i 266 . . . . . . . . . 10 k
4437, 43bitri 240 . . . . . . . . 9 SIk k
4544exbii 1582 . . . . . . . 8 SIk k
4626, 45bitri 240 . . . . . . 7 SIk k
4725, 46xchbinx 301 . . . . . 6 SIk k
485, 24, 473bitri 262 . . . . 5 P6 1c k SIk k
4948con2bii 322 . . . 4 P6 1c k SIk k
501, 2, 493bitri 262 . . 3 P6 1c k SIk k
513elimak 4259 . . 3 k
523elcompl 3225 . . 3 P6 1c k SIk k P6 1c k SIk k
5350, 51, 523bitr4i 268 . 2 k P6 1c k SIk k
5453eqriv 2350 1 k P6 1c k SIk k
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wb 176   wo 357   wa 358  wal 1540  wex 1541   wceq 1642   wcel 1710  wrex 2615  cvv 2859   ∼ ccompl 3205   cun 3207   cin 3208  csn 3737  copk 4057  1cc1c 4134   k cxpk 4174   P6 cp6 4178  kcimak 4179   SIk csik 4181
This theorem is referenced by:  imakexg  4299
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-ss 3259  df-nul 3551  df-sn 3741  df-pr 3742  df-opk 4058  df-1c 4136  df-xpk 4185  df-imak 4189  df-p6 4191  df-sik 4192
  Copyright terms: Public domain W3C validator