Definition df-ins3k 4189

Description: Define the Kuratowski third insertion operator. (Contributed by SF, 12-Jan-2015.)

Assertion

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

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

Detailed syntax breakdown of Definition df-ins3k

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cins3k 4178	. 2 class Ins3k 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	. . . . . . . . . . . . . 14 setvar t
12	11	cv 1641	. . . . . . . . . . . . 13 class t
13	12	csn 3738	. . . . . . . . . . . 12 class {t}
14	13	csn 3738	. . . . . . . . . . 11 class {{t}}
15	6, 14	wceq 1642	. . . . . . . . . 10 wff y = {{t}}
16		vu	. . . . . . . . . . . . 13 setvar u
17	16	cv 1641	. . . . . . . . . . . 12 class u
18		vv	. . . . . . . . . . . . 13 setvar v
19	18	cv 1641	. . . . . . . . . . . 12 class v
20	17, 19	copk 4058	. . . . . . . . . . 11 class ⟪u, v⟫
21	8, 20	wceq 1642	. . . . . . . . . 10 wff z = ⟪u, v⟫
22	12, 17	copk 4058	. . . . . . . . . . 11 class ⟪t, u⟫
23	22, 1	wcel 1710	. . . . . . . . . 10 wff ⟪t, u⟫ ∈ A
24	15, 21, 23	w3a 934	. . . . . . . . 9 wff (y = {{t}} ∧ z = ⟪u, v⟫ ∧ ⟪t, u⟫ ∈ A)
25	24, 18	wex 1541	. . . . . . . 8 wff ∃v(y = {{t}} ∧ z = ⟪u, v⟫ ∧ ⟪t, u⟫ ∈ A)
26	25, 16	wex 1541	. . . . . . 7 wff ∃u∃v(y = {{t}} ∧ z = ⟪u, v⟫ ∧ ⟪t, u⟫ ∈ A)
27	26, 11	wex 1541	. . . . . 6 wff ∃t∃u∃v(y = {{t}} ∧ z = ⟪u, v⟫ ∧ ⟪t, u⟫ ∈ A)
28	10, 27	wa 358	. . . . 5 wff (x = ⟪y, z⟫ ∧ ∃t∃u∃v(y = {{t}} ∧ z = ⟪u, v⟫ ∧ ⟪t, u⟫ ∈ A))
29	28, 7	wex 1541	. . . 4 wff ∃z(x = ⟪y, z⟫ ∧ ∃t∃u∃v(y = {{t}} ∧ z = ⟪u, v⟫ ∧ ⟪t, u⟫ ∈ A))
30	29, 5	wex 1541	. . 3 wff ∃y∃z(x = ⟪y, z⟫ ∧ ∃t∃u∃v(y = {{t}} ∧ z = ⟪u, v⟫ ∧ ⟪t, u⟫ ∈ A))
31	30, 3	cab 2339	. 2 class {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃t∃u∃v(y = {{t}} ∧ z = ⟪u, v⟫ ∧ ⟪t, u⟫ ∈ A))}
32	2, 31	wceq 1642	1 wff Ins3k A = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃t∃u∃v(y = {{t}} ∧ z = ⟪u, v⟫ ∧ ⟪t, u⟫ ∈ A))}

This definition is used by:  ins3keq  4220  opkelins3kg  4253  ins3kss  4281