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

Theorem opkelcokg 4261
 Description: Membership in a Kuratowski composition. (Contributed by SF, 13-Jan-2015.)
Assertion
Ref Expression
opkelcokg ((A V B W) → (⟪A, B (C k D) ↔ x(⟪A, x D x, B C)))
Distinct variable groups:   x,A   x,B   x,C   x,D
Allowed substitution hints:   V(x)   W(x)

Proof of Theorem opkelcokg
Dummy variables y z w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 2867 . 2 (A VA V)
2 elex 2867 . 2 (B WB V)
3 df-cok 4190 . . . . 5 (C k D) = (( Ins2k CIns3k kD) “k V)
43eleq2i 2417 . . . 4 (⟪A, B (C k D) ↔ ⟪A, B (( Ins2k CIns3k kD) “k V))
5 opkex 4113 . . . . 5 A, B V
65elimakv 4260 . . . 4 (⟪A, B (( Ins2k CIns3k kD) “k V) ↔ yy, ⟪A, B⟫⟫ ( Ins2k CIns3k kD))
7 vex 2862 . . . . . . . . . 10 y V
8 opkelins2kg 4251 . . . . . . . . . 10 ((y V A, B V) → (⟪y, ⟪A, B⟫⟫ Ins2k Cxzw(y = {{x}} A, B⟫ = ⟪z, wx, w C)))
97, 5, 8mp2an 653 . . . . . . . . 9 (⟪y, ⟪A, B⟫⟫ Ins2k Cxzw(y = {{x}} A, B⟫ = ⟪z, wx, w C))
10 3anass 938 . . . . . . . . . . . 12 ((y = {{x}} A, B⟫ = ⟪z, wx, w C) ↔ (y = {{x}} (⟪A, B⟫ = ⟪z, wx, w C)))
11102exbii 1583 . . . . . . . . . . 11 (zw(y = {{x}} A, B⟫ = ⟪z, wx, w C) ↔ zw(y = {{x}} (⟪A, B⟫ = ⟪z, wx, w C)))
12 19.42vv 1907 . . . . . . . . . . 11 (zw(y = {{x}} (⟪A, B⟫ = ⟪z, wx, w C)) ↔ (y = {{x}} zw(⟪A, B⟫ = ⟪z, wx, w C)))
1311, 12bitri 240 . . . . . . . . . 10 (zw(y = {{x}} A, B⟫ = ⟪z, wx, w C) ↔ (y = {{x}} zw(⟪A, B⟫ = ⟪z, wx, w C)))
1413exbii 1582 . . . . . . . . 9 (xzw(y = {{x}} A, B⟫ = ⟪z, wx, w C) ↔ x(y = {{x}} zw(⟪A, B⟫ = ⟪z, wx, w C)))
159, 14bitri 240 . . . . . . . 8 (⟪y, ⟪A, B⟫⟫ Ins2k Cx(y = {{x}} zw(⟪A, B⟫ = ⟪z, wx, w C)))
1615anbi1i 676 . . . . . . 7 ((⟪y, ⟪A, B⟫⟫ Ins2k C y, ⟪A, B⟫⟫ Ins3k kD) ↔ (x(y = {{x}} zw(⟪A, B⟫ = ⟪z, wx, w C)) y, ⟪A, B⟫⟫ Ins3k kD))
17 elin 3219 . . . . . . 7 (⟪y, ⟪A, B⟫⟫ ( Ins2k CIns3k kD) ↔ (⟪y, ⟪A, B⟫⟫ Ins2k C y, ⟪A, B⟫⟫ Ins3k kD))
18 19.41v 1901 . . . . . . 7 (x((y = {{x}} zw(⟪A, B⟫ = ⟪z, wx, w C)) y, ⟪A, B⟫⟫ Ins3k kD) ↔ (x(y = {{x}} zw(⟪A, B⟫ = ⟪z, wx, w C)) y, ⟪A, B⟫⟫ Ins3k kD))
1916, 17, 183bitr4i 268 . . . . . 6 (⟪y, ⟪A, B⟫⟫ ( Ins2k CIns3k kD) ↔ x((y = {{x}} zw(⟪A, B⟫ = ⟪z, wx, w C)) y, ⟪A, B⟫⟫ Ins3k kD))
2019exbii 1582 . . . . 5 (yy, ⟪A, B⟫⟫ ( Ins2k CIns3k kD) ↔ yx((y = {{x}} zw(⟪A, B⟫ = ⟪z, wx, w C)) y, ⟪A, B⟫⟫ Ins3k kD))
21 excom 1741 . . . . 5 (yx((y = {{x}} zw(⟪A, B⟫ = ⟪z, wx, w C)) y, ⟪A, B⟫⟫ Ins3k kD) ↔ xy((y = {{x}} zw(⟪A, B⟫ = ⟪z, wx, w C)) y, ⟪A, B⟫⟫ Ins3k kD))
22 anass 630 . . . . . . . 8 (((y = {{x}} zw(⟪A, B⟫ = ⟪z, wx, w C)) y, ⟪A, B⟫⟫ Ins3k kD) ↔ (y = {{x}} (zw(⟪A, B⟫ = ⟪z, wx, w C) y, ⟪A, B⟫⟫ Ins3k kD)))
2322exbii 1582 . . . . . . 7 (y((y = {{x}} zw(⟪A, B⟫ = ⟪z, wx, w C)) y, ⟪A, B⟫⟫ Ins3k kD) ↔ y(y = {{x}} (zw(⟪A, B⟫ = ⟪z, wx, w C) y, ⟪A, B⟫⟫ Ins3k kD)))
24 snex 4111 . . . . . . . 8 {{x}} V
25 opkeq1 4059 . . . . . . . . . 10 (y = {{x}} → ⟪y, ⟪A, B⟫⟫ = ⟪{{x}}, ⟪A, B⟫⟫)
2625eleq1d 2419 . . . . . . . . 9 (y = {{x}} → (⟪y, ⟪A, B⟫⟫ Ins3k kD ↔ ⟪{{x}}, ⟪A, B⟫⟫ Ins3k kD))
2726anbi2d 684 . . . . . . . 8 (y = {{x}} → ((zw(⟪A, B⟫ = ⟪z, wx, w C) y, ⟪A, B⟫⟫ Ins3k kD) ↔ (zw(⟪A, B⟫ = ⟪z, wx, w C) ⟪{{x}}, ⟪A, B⟫⟫ Ins3k kD)))
2824, 27ceqsexv 2894 . . . . . . 7 (y(y = {{x}} (zw(⟪A, B⟫ = ⟪z, wx, w C) y, ⟪A, B⟫⟫ Ins3k kD)) ↔ (zw(⟪A, B⟫ = ⟪z, wx, w C) ⟪{{x}}, ⟪A, B⟫⟫ Ins3k kD))
2923, 28bitri 240 . . . . . 6 (y((y = {{x}} zw(⟪A, B⟫ = ⟪z, wx, w C)) y, ⟪A, B⟫⟫ Ins3k kD) ↔ (zw(⟪A, B⟫ = ⟪z, wx, w C) ⟪{{x}}, ⟪A, B⟫⟫ Ins3k kD))
3029exbii 1582 . . . . 5 (xy((y = {{x}} zw(⟪A, B⟫ = ⟪z, wx, w C)) y, ⟪A, B⟫⟫ Ins3k kD) ↔ x(zw(⟪A, B⟫ = ⟪z, wx, w C) ⟪{{x}}, ⟪A, B⟫⟫ Ins3k kD))
3120, 21, 303bitri 262 . . . 4 (yy, ⟪A, B⟫⟫ ( Ins2k CIns3k kD) ↔ x(zw(⟪A, B⟫ = ⟪z, wx, w C) ⟪{{x}}, ⟪A, B⟫⟫ Ins3k kD))
324, 6, 313bitri 262 . . 3 (⟪A, B (C k D) ↔ x(zw(⟪A, B⟫ = ⟪z, wx, w C) ⟪{{x}}, ⟪A, B⟫⟫ Ins3k kD))
33 ancom 437 . . . . 5 ((zw(⟪A, B⟫ = ⟪z, wx, w C) ⟪{{x}}, ⟪A, B⟫⟫ Ins3k kD) ↔ (⟪{{x}}, ⟪A, B⟫⟫ Ins3k kD zw(⟪A, B⟫ = ⟪z, wx, w C)))
34 vex 2862 . . . . . . . 8 x V
35 otkelins3kg 4254 . . . . . . . 8 ((x V A V B V) → (⟪{{x}}, ⟪A, B⟫⟫ Ins3k kD ↔ ⟪x, A kD))
3634, 35mp3an1 1264 . . . . . . 7 ((A V B V) → (⟪{{x}}, ⟪A, B⟫⟫ Ins3k kD ↔ ⟪x, A kD))
37 opkelcnvkg 4249 . . . . . . . . 9 ((x V A V) → (⟪x, A kD ↔ ⟪A, x D))
3834, 37mpan 651 . . . . . . . 8 (A V → (⟪x, A kD ↔ ⟪A, x D))
3938adantr 451 . . . . . . 7 ((A V B V) → (⟪x, A kD ↔ ⟪A, x D))
4036, 39bitrd 244 . . . . . 6 ((A V B V) → (⟪{{x}}, ⟪A, B⟫⟫ Ins3k kD ↔ ⟪A, x D))
41 eqcom 2355 . . . . . . . . . 10 (⟪A, B⟫ = ⟪z, w⟫ ↔ ⟪z, w⟫ = ⟪A, B⟫)
4241anbi1i 676 . . . . . . . . 9 ((⟪A, B⟫ = ⟪z, wx, w C) ↔ (⟪z, w⟫ = ⟪A, Bx, w C))
43422exbii 1583 . . . . . . . 8 (zw(⟪A, B⟫ = ⟪z, wx, w C) ↔ zw(⟪z, w⟫ = ⟪A, Bx, w C))
44 vex 2862 . . . . . . . . . . . . . 14 z V
45 vex 2862 . . . . . . . . . . . . . 14 w V
46 opkthg 4131 . . . . . . . . . . . . . 14 ((z V w V B V) → (⟪z, w⟫ = ⟪A, B⟫ ↔ (z = A w = B)))
4744, 45, 46mp3an12 1267 . . . . . . . . . . . . 13 (B V → (⟪z, w⟫ = ⟪A, B⟫ ↔ (z = A w = B)))
4847anbi1d 685 . . . . . . . . . . . 12 (B V → ((⟪z, w⟫ = ⟪A, Bx, w C) ↔ ((z = A w = B) x, w C)))
49 anass 630 . . . . . . . . . . . 12 (((z = A w = B) x, w C) ↔ (z = A (w = B x, w C)))
5048, 49syl6bb 252 . . . . . . . . . . 11 (B V → ((⟪z, w⟫ = ⟪A, Bx, w C) ↔ (z = A (w = B x, w C))))
51502exbidv 1628 . . . . . . . . . 10 (B V → (zw(⟪z, w⟫ = ⟪A, Bx, w C) ↔ zw(z = A (w = B x, w C))))
5251adantl 452 . . . . . . . . 9 ((A V B V) → (zw(⟪z, w⟫ = ⟪A, Bx, w C) ↔ zw(z = A (w = B x, w C))))
53 eeanv 1913 . . . . . . . . 9 (zw(z = A (w = B x, w C)) ↔ (z z = A w(w = B x, w C)))
5452, 53syl6bb 252 . . . . . . . 8 ((A V B V) → (zw(⟪z, w⟫ = ⟪A, Bx, w C) ↔ (z z = A w(w = B x, w C))))
5543, 54syl5bb 248 . . . . . . 7 ((A V B V) → (zw(⟪A, B⟫ = ⟪z, wx, w C) ↔ (z z = A w(w = B x, w C))))
56 elisset 2869 . . . . . . . . . 10 (A V → z z = A)
5756biantrurd 494 . . . . . . . . 9 (A V → (w(w = B x, w C) ↔ (z z = A w(w = B x, w C))))
5857bicomd 192 . . . . . . . 8 (A V → ((z z = A w(w = B x, w C)) ↔ w(w = B x, w C)))
59 opkeq2 4060 . . . . . . . . . 10 (w = B → ⟪x, w⟫ = ⟪x, B⟫)
6059eleq1d 2419 . . . . . . . . 9 (w = B → (⟪x, w C ↔ ⟪x, B C))
6160ceqsexgv 2971 . . . . . . . 8 (B V → (w(w = B x, w C) ↔ ⟪x, B C))
6258, 61sylan9bb 680 . . . . . . 7 ((A V B V) → ((z z = A w(w = B x, w C)) ↔ ⟪x, B C))
6355, 62bitrd 244 . . . . . 6 ((A V B V) → (zw(⟪A, B⟫ = ⟪z, wx, w C) ↔ ⟪x, B C))
6440, 63anbi12d 691 . . . . 5 ((A V B V) → ((⟪{{x}}, ⟪A, B⟫⟫ Ins3k kD zw(⟪A, B⟫ = ⟪z, wx, w C)) ↔ (⟪A, x D x, B C)))
6533, 64syl5bb 248 . . . 4 ((A V B V) → ((zw(⟪A, B⟫ = ⟪z, wx, w C) ⟪{{x}}, ⟪A, B⟫⟫ Ins3k kD) ↔ (⟪A, x D x, B C)))
6665exbidv 1626 . . 3 ((A V B V) → (x(zw(⟪A, B⟫ = ⟪z, wx, w C) ⟪{{x}}, ⟪A, B⟫⟫ Ins3k kD) ↔ x(⟪A, x D x, B C)))
6732, 66syl5bb 248 . 2 ((A V B V) → (⟪A, B (C k D) ↔ x(⟪A, x D x, B C)))
681, 2, 67syl2an 463 1 ((A V B W) → (⟪A, B (C k D) ↔ x(⟪A, x D x, B C)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358   ∧ w3a 934  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2859   ∩ cin 3208  {csn 3737  ⟪copk 4057  ◡kccnvk 4175   Ins2k cins2k 4176   Ins3k cins3k 4177   “k cimak 4179   ∘k ccomk 4180 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-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-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190 This theorem is referenced by:  opkelcok  4262  opkelimagekg  4271
 Copyright terms: Public domain W3C validator