Definition df-sik 4193

Description: Define the Kuratowski singleton image operation. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-sik	⊢ SIk A = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃t∃u(y = {t} ∧ z = {u} ∧ ⟪t, u⟫ ∈ A))}

Distinct variable group:   x,A,y,z,t,u

Detailed syntax breakdown of Definition df-sik

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	csik 4182	. 2 class SIk A
3		vx	. . . . . . . 8 setvar x
4	3	cv 1641	. . . . . . 7 class x
5		vy	. . . . . . . . 9 setvar y
6	5	cv 1641	. . . . . . . 8 class y
7		vz	. . . . . . . . 9 setvar z
8	7	cv 1641	. . . . . . . 8 class z
9	6, 8	copk 4058	. . . . . . 7 class ⟪y, z⟫
10	4, 9	wceq 1642	. . . . . 6 wff x = ⟪y, z⟫
11		vt	. . . . . . . . . . . 12 setvar t
12	11	cv 1641	. . . . . . . . . . 11 class t
13	12	csn 3738	. . . . . . . . . 10 class {t}
14	6, 13	wceq 1642	. . . . . . . . 9 wff y = {t}
15		vu	. . . . . . . . . . . 12 setvar u
16	15	cv 1641	. . . . . . . . . . 11 class u
17	16	csn 3738	. . . . . . . . . 10 class {u}
18	8, 17	wceq 1642	. . . . . . . . 9 wff z = {u}
19	12, 16	copk 4058	. . . . . . . . . 10 class ⟪t, u⟫
20	19, 1	wcel 1710	. . . . . . . . 9 wff ⟪t, u⟫ ∈ A
21	14, 18, 20	w3a 934	. . . . . . . 8 wff (y = {t} ∧ z = {u} ∧ ⟪t, u⟫ ∈ A)
22	21, 15	wex 1541	. . . . . . 7 wff ∃u(y = {t} ∧ z = {u} ∧ ⟪t, u⟫ ∈ A)
23	22, 11	wex 1541	. . . . . 6 wff ∃t∃u(y = {t} ∧ z = {u} ∧ ⟪t, u⟫ ∈ A)
24	10, 23	wa 358	. . . . 5 wff (x = ⟪y, z⟫ ∧ ∃t∃u(y = {t} ∧ z = {u} ∧ ⟪t, u⟫ ∈ A))
25	24, 7	wex 1541	. . . 4 wff ∃z(x = ⟪y, z⟫ ∧ ∃t∃u(y = {t} ∧ z = {u} ∧ ⟪t, u⟫ ∈ A))
26	25, 5	wex 1541	. . 3 wff ∃y∃z(x = ⟪y, z⟫ ∧ ∃t∃u(y = {t} ∧ z = {u} ∧ ⟪t, u⟫ ∈ A))
27	26, 3	cab 2339	. 2 class {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃t∃u(y = {t} ∧ z = {u} ∧ ⟪t, u⟫ ∈ A))}
28	2, 27	wceq 1642	1 wff SIk A = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃t∃u(y = {t} ∧ z = {u} ∧ ⟪t, u⟫ ∈ A))}

This definition is used by:  sikeq  4242  opkelsikg  4265  sikssvvk  4267  sikss1c1c  4268