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

Theorem otkelins2kg 4253
 Description: Kuratowski ordered triple membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
Assertion
Ref Expression
otkelins2kg ((A V B W C T) → (⟪{{A}}, ⟪B, C⟫⟫ Ins2k D ↔ ⟪A, C D))

Proof of Theorem otkelins2kg
Dummy variables x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snex 4111 . . . 4 {{A}} V
2 opkex 4113 . . . 4 B, C V
3 opkelins2kg 4251 . . . 4 (({{A}} V B, C V) → (⟪{{A}}, ⟪B, C⟫⟫ Ins2k Dxyz({{A}} = {{x}} B, C⟫ = ⟪y, zx, z D)))
41, 2, 3mp2an 653 . . 3 (⟪{{A}}, ⟪B, C⟫⟫ Ins2k Dxyz({{A}} = {{x}} B, C⟫ = ⟪y, zx, z D))
5 3anass 938 . . . . . . 7 (({{A}} = {{x}} B, C⟫ = ⟪y, zx, z D) ↔ ({{A}} = {{x}} (⟪B, C⟫ = ⟪y, zx, z D)))
6 eqcom 2355 . . . . . . . . 9 ({{A}} = {{x}} ↔ {{x}} = {{A}})
7 snex 4111 . . . . . . . . . . 11 {x} V
87sneqb 3876 . . . . . . . . . 10 ({{x}} = {{A}} ↔ {x} = {A})
9 vex 2862 . . . . . . . . . . 11 x V
109sneqb 3876 . . . . . . . . . 10 ({x} = {A} ↔ x = A)
118, 10bitri 240 . . . . . . . . 9 ({{x}} = {{A}} ↔ x = A)
126, 11bitri 240 . . . . . . . 8 ({{A}} = {{x}} ↔ x = A)
1312anbi1i 676 . . . . . . 7 (({{A}} = {{x}} (⟪B, C⟫ = ⟪y, zx, z D)) ↔ (x = A (⟪B, C⟫ = ⟪y, zx, z D)))
145, 13bitri 240 . . . . . 6 (({{A}} = {{x}} B, C⟫ = ⟪y, zx, z D) ↔ (x = A (⟪B, C⟫ = ⟪y, zx, z D)))
15142exbii 1583 . . . . 5 (yz({{A}} = {{x}} B, C⟫ = ⟪y, zx, z D) ↔ yz(x = A (⟪B, C⟫ = ⟪y, zx, z D)))
16 19.42vv 1907 . . . . 5 (yz(x = A (⟪B, C⟫ = ⟪y, zx, z D)) ↔ (x = A yz(⟪B, C⟫ = ⟪y, zx, z D)))
1715, 16bitri 240 . . . 4 (yz({{A}} = {{x}} B, C⟫ = ⟪y, zx, z D) ↔ (x = A yz(⟪B, C⟫ = ⟪y, zx, z D)))
1817exbii 1582 . . 3 (xyz({{A}} = {{x}} B, C⟫ = ⟪y, zx, z D) ↔ x(x = A yz(⟪B, C⟫ = ⟪y, zx, z D)))
194, 18bitri 240 . 2 (⟪{{A}}, ⟪B, C⟫⟫ Ins2k Dx(x = A yz(⟪B, C⟫ = ⟪y, zx, z D)))
20 opkeq1 4059 . . . . . . . 8 (x = A → ⟪x, z⟫ = ⟪A, z⟫)
2120eleq1d 2419 . . . . . . 7 (x = A → (⟪x, z D ↔ ⟪A, z D))
2221anbi2d 684 . . . . . 6 (x = A → ((⟪B, C⟫ = ⟪y, zx, z D) ↔ (⟪B, C⟫ = ⟪y, zA, z D)))
23222exbidv 1628 . . . . 5 (x = A → (yz(⟪B, C⟫ = ⟪y, zx, z D) ↔ yz(⟪B, C⟫ = ⟪y, zA, z D)))
2423ceqsexgv 2971 . . . 4 (A V → (x(x = A yz(⟪B, C⟫ = ⟪y, zx, z D)) ↔ yz(⟪B, C⟫ = ⟪y, zA, z D)))
25243ad2ant1 976 . . 3 ((A V B W C T) → (x(x = A yz(⟪B, C⟫ = ⟪y, zx, z D)) ↔ yz(⟪B, C⟫ = ⟪y, zA, z D)))
26 eqcom 2355 . . . . . . . . . 10 (⟪B, C⟫ = ⟪y, z⟫ ↔ ⟪y, z⟫ = ⟪B, C⟫)
27 vex 2862 . . . . . . . . . . 11 y V
28 vex 2862 . . . . . . . . . . 11 z V
29 opkthg 4131 . . . . . . . . . . 11 ((y V z V C T) → (⟪y, z⟫ = ⟪B, C⟫ ↔ (y = B z = C)))
3027, 28, 29mp3an12 1267 . . . . . . . . . 10 (C T → (⟪y, z⟫ = ⟪B, C⟫ ↔ (y = B z = C)))
3126, 30syl5bb 248 . . . . . . . . 9 (C T → (⟪B, C⟫ = ⟪y, z⟫ ↔ (y = B z = C)))
3231anbi1d 685 . . . . . . . 8 (C T → ((⟪B, C⟫ = ⟪y, zA, z D) ↔ ((y = B z = C) A, z D)))
33322exbidv 1628 . . . . . . 7 (C T → (yz(⟪B, C⟫ = ⟪y, zA, z D) ↔ yz((y = B z = C) A, z D)))
34 anass 630 . . . . . . . . . 10 (((y = B z = C) A, z D) ↔ (y = B (z = C A, z D)))
3534exbii 1582 . . . . . . . . 9 (z((y = B z = C) A, z D) ↔ z(y = B (z = C A, z D)))
36 19.42v 1905 . . . . . . . . 9 (z(y = B (z = C A, z D)) ↔ (y = B z(z = C A, z D)))
3735, 36bitri 240 . . . . . . . 8 (z((y = B z = C) A, z D) ↔ (y = B z(z = C A, z D)))
3837exbii 1582 . . . . . . 7 (yz((y = B z = C) A, z D) ↔ y(y = B z(z = C A, z D)))
3933, 38syl6bb 252 . . . . . 6 (C T → (yz(⟪B, C⟫ = ⟪y, zA, z D) ↔ y(y = B z(z = C A, z D))))
4039adantl 452 . . . . 5 ((B W C T) → (yz(⟪B, C⟫ = ⟪y, zA, z D) ↔ y(y = B z(z = C A, z D))))
41 biidd 228 . . . . . . 7 (y = B → (z(z = C A, z D) ↔ z(z = C A, z D)))
4241ceqsexgv 2971 . . . . . 6 (B W → (y(y = B z(z = C A, z D)) ↔ z(z = C A, z D)))
43 opkeq2 4060 . . . . . . . 8 (z = C → ⟪A, z⟫ = ⟪A, C⟫)
4443eleq1d 2419 . . . . . . 7 (z = C → (⟪A, z D ↔ ⟪A, C D))
4544ceqsexgv 2971 . . . . . 6 (C T → (z(z = C A, z D) ↔ ⟪A, C D))
4642, 45sylan9bb 680 . . . . 5 ((B W C T) → (y(y = B z(z = C A, z D)) ↔ ⟪A, C D))
4740, 46bitrd 244 . . . 4 ((B W C T) → (yz(⟪B, C⟫ = ⟪y, zA, z D) ↔ ⟪A, C D))
48473adant1 973 . . 3 ((A V B W C T) → (yz(⟪B, C⟫ = ⟪y, zA, z D) ↔ ⟪A, C D))
4925, 48bitrd 244 . 2 ((A V B W C T) → (x(x = A yz(⟪B, C⟫ = ⟪y, zx, z D)) ↔ ⟪A, C D))
5019, 49syl5bb 248 1 ((A V B W C T) → (⟪{{A}}, ⟪B, C⟫⟫ Ins2k D ↔ ⟪A, C D))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358   ∧ w3a 934  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2859  {csn 3737  ⟪copk 4057   Ins2k cins2k 4176 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-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-ins2k 4187 This theorem is referenced by:  otkelins2k  4255  opkelimagekg  4271
 Copyright terms: Public domain W3C validator