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

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

Proof of Theorem otkelins3kg
Dummy variables x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snex 4111 . . 3 {{A}} V
2 opkex 4113 . . 3 B, C V
3 opkelins3kg 4252 . . 3 (({{A}} V B, C V) → (⟪{{A}}, ⟪B, C⟫⟫ Ins3k Dxyz({{A}} = {{x}} B, C⟫ = ⟪y, zx, y D)))
41, 2, 3mp2an 653 . 2 (⟪{{A}}, ⟪B, C⟫⟫ Ins3k Dxyz({{A}} = {{x}} B, C⟫ = ⟪y, zx, y D))
5 3anass 938 . . . . . . . . 9 (({{A}} = {{x}} B, C⟫ = ⟪y, zx, y D) ↔ ({{A}} = {{x}} (⟪B, C⟫ = ⟪y, zx, y D)))
6 eqcom 2355 . . . . . . . . . . 11 ({{A}} = {{x}} ↔ {{x}} = {{A}})
7 snex 4111 . . . . . . . . . . . . 13 {x} V
87sneqb 3876 . . . . . . . . . . . 12 ({{x}} = {{A}} ↔ {x} = {A})
9 vex 2862 . . . . . . . . . . . . 13 x V
109sneqb 3876 . . . . . . . . . . . 12 ({x} = {A} ↔ x = A)
118, 10bitri 240 . . . . . . . . . . 11 ({{x}} = {{A}} ↔ x = A)
126, 11bitri 240 . . . . . . . . . 10 ({{A}} = {{x}} ↔ x = A)
1312anbi1i 676 . . . . . . . . 9 (({{A}} = {{x}} (⟪B, C⟫ = ⟪y, zx, y D)) ↔ (x = A (⟪B, C⟫ = ⟪y, zx, y D)))
145, 13bitri 240 . . . . . . . 8 (({{A}} = {{x}} B, C⟫ = ⟪y, zx, y D) ↔ (x = A (⟪B, C⟫ = ⟪y, zx, y D)))
15142exbii 1583 . . . . . . 7 (yz({{A}} = {{x}} B, C⟫ = ⟪y, zx, y D) ↔ yz(x = A (⟪B, C⟫ = ⟪y, zx, y D)))
16 19.42vv 1907 . . . . . . 7 (yz(x = A (⟪B, C⟫ = ⟪y, zx, y D)) ↔ (x = A yz(⟪B, C⟫ = ⟪y, zx, y D)))
1715, 16bitri 240 . . . . . 6 (yz({{A}} = {{x}} B, C⟫ = ⟪y, zx, y D) ↔ (x = A yz(⟪B, C⟫ = ⟪y, zx, y D)))
1817exbii 1582 . . . . 5 (xyz({{A}} = {{x}} B, C⟫ = ⟪y, zx, y D) ↔ x(x = A yz(⟪B, C⟫ = ⟪y, zx, y D)))
19 opkeq1 4059 . . . . . . . . 9 (x = A → ⟪x, y⟫ = ⟪A, y⟫)
2019eleq1d 2419 . . . . . . . 8 (x = A → (⟪x, y D ↔ ⟪A, y D))
2120anbi2d 684 . . . . . . 7 (x = A → ((⟪B, C⟫ = ⟪y, zx, y D) ↔ (⟪B, C⟫ = ⟪y, zA, y D)))
22212exbidv 1628 . . . . . 6 (x = A → (yz(⟪B, C⟫ = ⟪y, zx, y D) ↔ yz(⟪B, C⟫ = ⟪y, zA, y D)))
2322ceqsexgv 2971 . . . . 5 (A V → (x(x = A yz(⟪B, C⟫ = ⟪y, zx, y D)) ↔ yz(⟪B, C⟫ = ⟪y, zA, y D)))
2418, 23syl5bb 248 . . . 4 (A V → (xyz({{A}} = {{x}} B, C⟫ = ⟪y, zx, y D) ↔ yz(⟪B, C⟫ = ⟪y, zA, y D)))
25243ad2ant1 976 . . 3 ((A V B W C T) → (xyz({{A}} = {{x}} B, C⟫ = ⟪y, zx, y D) ↔ yz(⟪B, C⟫ = ⟪y, zA, y D)))
26 eqcom 2355 . . . . . . . . . . 11 (⟪B, C⟫ = ⟪y, z⟫ ↔ ⟪y, z⟫ = ⟪B, C⟫)
27 vex 2862 . . . . . . . . . . . 12 y V
28 vex 2862 . . . . . . . . . . . 12 z V
29 opkthg 4131 . . . . . . . . . . . 12 ((y V z V C T) → (⟪y, z⟫ = ⟪B, C⟫ ↔ (y = B z = C)))
3027, 28, 29mp3an12 1267 . . . . . . . . . . 11 (C T → (⟪y, z⟫ = ⟪B, C⟫ ↔ (y = B z = C)))
3126, 30syl5bb 248 . . . . . . . . . 10 (C T → (⟪B, C⟫ = ⟪y, z⟫ ↔ (y = B z = C)))
3231anbi1d 685 . . . . . . . . 9 (C T → ((⟪B, C⟫ = ⟪y, zA, y D) ↔ ((y = B z = C) A, y D)))
33 anass 630 . . . . . . . . 9 (((y = B z = C) A, y D) ↔ (y = B (z = C A, y D)))
3432, 33syl6bb 252 . . . . . . . 8 (C T → ((⟪B, C⟫ = ⟪y, zA, y D) ↔ (y = B (z = C A, y D))))
35342exbidv 1628 . . . . . . 7 (C T → (yz(⟪B, C⟫ = ⟪y, zA, y D) ↔ yz(y = B (z = C A, y D))))
36 exdistr 1906 . . . . . . 7 (yz(y = B (z = C A, y D)) ↔ y(y = B z(z = C A, y D)))
3735, 36syl6bb 252 . . . . . 6 (C T → (yz(⟪B, C⟫ = ⟪y, zA, y D) ↔ y(y = B z(z = C A, y D))))
3837adantl 452 . . . . 5 ((B W C T) → (yz(⟪B, C⟫ = ⟪y, zA, y D) ↔ y(y = B z(z = C A, y D))))
39 opkeq2 4060 . . . . . . . . . 10 (y = B → ⟪A, y⟫ = ⟪A, B⟫)
4039eleq1d 2419 . . . . . . . . 9 (y = B → (⟪A, y D ↔ ⟪A, B D))
4140anbi2d 684 . . . . . . . 8 (y = B → ((z = C A, y D) ↔ (z = C A, B D)))
4241exbidv 1626 . . . . . . 7 (y = B → (z(z = C A, y D) ↔ z(z = C A, B D)))
4342ceqsexgv 2971 . . . . . 6 (B W → (y(y = B z(z = C A, y D)) ↔ z(z = C A, B D)))
44 biidd 228 . . . . . . 7 (z = C → (⟪A, B D ↔ ⟪A, B D))
4544ceqsexgv 2971 . . . . . 6 (C T → (z(z = C A, B D) ↔ ⟪A, B D))
4643, 45sylan9bb 680 . . . . 5 ((B W C T) → (y(y = B z(z = C A, y D)) ↔ ⟪A, B D))
4738, 46bitrd 244 . . . 4 ((B W C T) → (yz(⟪B, C⟫ = ⟪y, zA, y D) ↔ ⟪A, B D))
48473adant1 973 . . 3 ((A V B W C T) → (yz(⟪B, C⟫ = ⟪y, zA, y D) ↔ ⟪A, B D))
4925, 48bitrd 244 . 2 ((A V B W C T) → (xyz({{A}} = {{x}} B, C⟫ = ⟪y, zx, y D) ↔ ⟪A, B D))
504, 49syl5bb 248 1 ((A V B W C T) → (⟪{{A}}, ⟪B, C⟫⟫ Ins3k D ↔ ⟪A, B 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   Ins3k cins3k 4177 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-ins3k 4188 This theorem is referenced by:  otkelins3k  4256  opkelcokg  4261  opkelimagekg  4271
 Copyright terms: Public domain W3C validator