df-ins4 - New Foundations Explorer

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

Definition df-ins4 5757

Description: Define the fourth insertion operation. (Contributed by SF, 9-Feb-2015.)

**Assertion**
Ref	Expression
df-ins4	⊢ Ins4 A = (^◡(1^st ⊗ ((1^st ∘ 2^nd ) ⊗ ((1^st ∘ 2^nd ) ∘ 2^nd ))) “ A)

**Detailed syntax breakdown of Definition df-ins4**
Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cins4 5756	. 2 class Ins4 A
3		c1st 4718	. . . . 5 class 1^st
4		c2nd 4784	. . . . . . 7 class 2^nd
5	3, 4	ccom 4722	. . . . . 6 class (1^st ∘ 2^nd )
6	5, 4	ccom 4722	. . . . . 6 class ((1^st ∘ 2^nd ) ∘ 2^nd )
7	5, 6	ctxp 5736	. . . . 5 class ((1^st ∘ 2^nd ) ⊗ ((1^st ∘ 2^nd ) ∘ 2^nd ))
8	3, 7	ctxp 5736	. . . 4 class (1^st ⊗ ((1^st ∘ 2^nd ) ⊗ ((1^st ∘ 2^nd ) ∘ 2^nd )))
9	8	ccnv 4772	. . 3 class ^◡(1^st ⊗ ((1^st ∘ 2^nd ) ⊗ ((1^st ∘ 2^nd ) ∘ 2^nd )))
10	9, 1	cima 4723	. 2 class (^◡(1^st ⊗ ((1^st ∘ 2^nd ) ⊗ ((1^st ∘ 2^nd ) ∘ 2^nd ))) “ A)
11	2, 10	wceq 1642	1 wff Ins4 A = (^◡(1^st ⊗ ((1^st ∘ 2^nd ) ⊗ ((1^st ∘ 2^nd ) ∘ 2^nd ))) “ A)

Colors of variables: wff setvar class

This definition is referenced by: oqelins4 5795 ins4ex 5800

Copyright terms: Public domain