composeex - New Foundations Explorer

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

Theorem composeex 5820

Description: The compose function is a set. (Contributed by Scott Fenton, 19-Apr-2021.)

**Assertion**
Ref	Expression
composeex	Compose

Proof of Theorem composeex Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-compose 5748	. . 3 Compose
2		elopab 4696	. . . . 5 $/\$ $/\$ $/\$
3		df-co 4726	. . . . . 6 $/\$
4	3	eleq2i 2417	. . . . 5 $/\$
5		elima1c 4947	. . . . . 6 Ins4 SI₃ Ins2 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c1_c1_c Ins4 SI₃ Ins2 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c1_c
6		elima1c 4947	. . . . . . . 8 Ins4 SI₃ Ins2 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c1_c Ins4 SI₃ Ins2 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c
7		elin 3219	. . . . . . . . . 10 Ins4 SI₃ Ins2 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c Ins4 SI₃ Ins2 $/\$ Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c
8		vex 2862	. . . . . . . . . . . . . 14
9		vex 2862	. . . . . . . . . . . . . 14
10	8, 9	opex 4588	. . . . . . . . . . . . 13
11	10	oqelins4 5794	. . . . . . . . . . . 12 Ins4 SI₃ Ins2 SI₃ Ins2
12		vex 2862	. . . . . . . . . . . . 13
13		vex 2862	. . . . . . . . . . . . 13
14		vex 2862	. . . . . . . . . . . . 13
15	12, 13, 14	otsnelsi3 5805	. . . . . . . . . . . 12 SI₃ Ins2 Ins2
16		elin 3219	. . . . . . . . . . . . 13 Ins2 $/\$ Ins2
17		opelxp 4811	. . . . . . . . . . . . . . . 16 $/\$
18	12, 17	mpbiran 884	. . . . . . . . . . . . . . 15
19		df-br 4640	. . . . . . . . . . . . . . 15
20		brcnv 4892	. . . . . . . . . . . . . . 15
21	18, 19, 20	3bitr2i 264	. . . . . . . . . . . . . 14
22	13	otelins2 5791	. . . . . . . . . . . . . . 15 Ins2
23		df-br 4640	. . . . . . . . . . . . . . 15
24		brcnv 4892	. . . . . . . . . . . . . . 15
25	22, 23, 24	3bitr2i 264	. . . . . . . . . . . . . 14 Ins2
26	21, 25	anbi12i 678	. . . . . . . . . . . . 13 $/\$ Ins2 $/\$
27	13, 12	op1st2nd 5790	. . . . . . . . . . . . 13 $/\$
28	16, 26, 27	3bitri 262	. . . . . . . . . . . 12 Ins2
29	11, 15, 28	3bitri 262	. . . . . . . . . . 11 Ins4 SI₃ Ins2
30		elima1c 4947	. . . . . . . . . . . 12 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c
31		elin 3219	. . . . . . . . . . . . . 14 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c $/\$ Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c
32		snex 4111	. . . . . . . . . . . . . . . . 17
33	32	otelins2 5791	. . . . . . . . . . . . . . . 16 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c
34		df-clel 2349	. . . . . . . . . . . . . . . . 17 $/\$
35		df-br 4640	. . . . . . . . . . . . . . . . 17
36		elima1c 4947	. . . . . . . . . . . . . . . . . 18 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S
37		elin 3219	. . . . . . . . . . . . . . . . . . . 20 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S Ins4 SI₃ Swap $/\$ Ins2 Ins2 Ins2 Ins2 S
38		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . 24
39	38, 10	opex 4588	. . . . . . . . . . . . . . . . . . . . . . 23
40	39	oqelins4 5794	. . . . . . . . . . . . . . . . . . . . . 22 Ins4 SI₃ Swap SI₃ Swap
41		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . 24
42	12, 41, 13	otsnelsi3 5805	. . . . . . . . . . . . . . . . . . . . . . 23 SI₃ Swap Swap
43		df-br 4640	. . . . . . . . . . . . . . . . . . . . . . 23 Swap Swap
44	41, 13	brswap2 4860	. . . . . . . . . . . . . . . . . . . . . . 23 Swap
45	42, 43, 44	3bitr2i 264	. . . . . . . . . . . . . . . . . . . . . 22 SI₃ Swap
46	40, 45	bitri 240	. . . . . . . . . . . . . . . . . . . . 21 Ins4 SI₃ Swap
47		snex 4111	. . . . . . . . . . . . . . . . . . . . . . 23
48	47	otelins2 5791	. . . . . . . . . . . . . . . . . . . . . 22 Ins2 Ins2 Ins2 Ins2 S Ins2 Ins2 Ins2 S
49		snex 4111	. . . . . . . . . . . . . . . . . . . . . . 23
50	49	otelins2 5791	. . . . . . . . . . . . . . . . . . . . . 22 Ins2 Ins2 Ins2 S Ins2 Ins2 S
51	38	otelins2 5791	. . . . . . . . . . . . . . . . . . . . . . 23 Ins2 Ins2 S Ins2 S
52	8	otelins2 5791	. . . . . . . . . . . . . . . . . . . . . . 23 Ins2 S S
53	12, 9	opelssetsn 4760	. . . . . . . . . . . . . . . . . . . . . . 23 S
54	51, 52, 53	3bitri 262	. . . . . . . . . . . . . . . . . . . . . 22 Ins2 Ins2 S
55	48, 50, 54	3bitri 262	. . . . . . . . . . . . . . . . . . . . 21 Ins2 Ins2 Ins2 Ins2 S
56	46, 55	anbi12i 678	. . . . . . . . . . . . . . . . . . . 20 Ins4 SI₃ Swap $/\$ Ins2 Ins2 Ins2 Ins2 S $/\$
57	37, 56	bitri 240	. . . . . . . . . . . . . . . . . . 19 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S $/\$
58	57	exbii 1582	. . . . . . . . . . . . . . . . . 18 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S $/\$
59	36, 58	bitri 240	. . . . . . . . . . . . . . . . 17 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c $/\$
60	34, 35, 59	3bitr4ri 269	. . . . . . . . . . . . . . . 16 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c
61	33, 60	bitri 240	. . . . . . . . . . . . . . 15 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c
62		df-clel 2349	. . . . . . . . . . . . . . . 16 $/\$
63		df-br 4640	. . . . . . . . . . . . . . . 16
64		elima1c 4947	. . . . . . . . . . . . . . . . 17 Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S
65		elin 3219	. . . . . . . . . . . . . . . . . . 19 Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S Ins4 SI₃ $/\$ Ins2 Ins2 Ins2 Ins2 Ins3 S
66	49, 39	opex 4588	. . . . . . . . . . . . . . . . . . . . . 22
67	66	oqelins4 5794	. . . . . . . . . . . . . . . . . . . . 21 Ins4 SI₃ SI₃
68		vex 2862	. . . . . . . . . . . . . . . . . . . . . . 23
69	68, 41, 12	otsnelsi3 5805	. . . . . . . . . . . . . . . . . . . . . 22 SI₃
70		df-br 4640	. . . . . . . . . . . . . . . . . . . . . 22
71	41, 12	opex 4588	. . . . . . . . . . . . . . . . . . . . . . 23
72	71	ideq 4870	. . . . . . . . . . . . . . . . . . . . . 22
73	69, 70, 72	3bitr2i 264	. . . . . . . . . . . . . . . . . . . . 21 SI₃
74	67, 73	bitri 240	. . . . . . . . . . . . . . . . . . . 20 Ins4 SI₃
75	47	otelins2 5791	. . . . . . . . . . . . . . . . . . . . 21 Ins2 Ins2 Ins2 Ins2 Ins3 S Ins2 Ins2 Ins2 Ins3 S
76	32	otelins2 5791	. . . . . . . . . . . . . . . . . . . . 21 Ins2 Ins2 Ins2 Ins3 S Ins2 Ins2 Ins3 S
77	49	otelins2 5791	. . . . . . . . . . . . . . . . . . . . . 22 Ins2 Ins2 Ins3 S Ins2 Ins3 S
78	38	otelins2 5791	. . . . . . . . . . . . . . . . . . . . . 22 Ins2 Ins3 S Ins3 S
79	9	otelins3 5792	. . . . . . . . . . . . . . . . . . . . . . 23 Ins3 S S
80	68, 8	opelssetsn 4760	. . . . . . . . . . . . . . . . . . . . . . 23 S
81	79, 80	bitri 240	. . . . . . . . . . . . . . . . . . . . . 22 Ins3 S
82	77, 78, 81	3bitri 262	. . . . . . . . . . . . . . . . . . . . 21 Ins2 Ins2 Ins3 S
83	75, 76, 82	3bitri 262	. . . . . . . . . . . . . . . . . . . 20 Ins2 Ins2 Ins2 Ins2 Ins3 S
84	74, 83	anbi12i 678	. . . . . . . . . . . . . . . . . . 19 Ins4 SI₃ $/\$ Ins2 Ins2 Ins2 Ins2 Ins3 S $/\$
85	65, 84	bitri 240	. . . . . . . . . . . . . . . . . 18 Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S $/\$
86	85	exbii 1582	. . . . . . . . . . . . . . . . 17 Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S $/\$
87	64, 86	bitri 240	. . . . . . . . . . . . . . . 16 Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c $/\$
88	62, 63, 87	3bitr4ri 269	. . . . . . . . . . . . . . 15 Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c
89	61, 88	anbi12i 678	. . . . . . . . . . . . . 14 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c $/\$ Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c $/\$
90	31, 89	bitri 240	. . . . . . . . . . . . 13 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c $/\$
91	90	exbii 1582	. . . . . . . . . . . 12 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c $/\$
92	30, 91	bitri 240	. . . . . . . . . . 11 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c $/\$
93	29, 92	anbi12i 678	. . . . . . . . . 10 Ins4 SI₃ Ins2 $/\$ Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c $/\$ $/\$
94	7, 93	bitri 240	. . . . . . . . 9 Ins4 SI₃ Ins2 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c $/\$ $/\$
95	94	exbii 1582	. . . . . . . 8 Ins4 SI₃ Ins2 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c $/\$ $/\$
96	6, 95	bitri 240	. . . . . . 7 Ins4 SI₃ Ins2 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c1_c $/\$ $/\$
97	96	exbii 1582	. . . . . 6 Ins4 SI₃ Ins2 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c1_c $/\$ $/\$
98	5, 97	bitri 240	. . . . 5 Ins4 SI₃ Ins2 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c1_c1_c $/\$ $/\$
99	2, 4, 98	3bitr4ri 269	. . . 4 Ins4 SI₃ Ins2 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c1_c1_c
100	99	releqmpt2 5809	. . 3 Ins2 S Ins3 Ins4 SI₃ Ins2 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c1_c1_c1_c
101	1, 100	eqtr4i 2376	. 2 Compose Ins2 S Ins3 Ins4 SI₃ Ins2 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c1_c1_c1_c
102		vvex 4109	. . 3
103		1stex 4739	. . . . . . . . . . 11
104	103	cnvex 5102	. . . . . . . . . 10
105	102, 104	xpex 5115	. . . . . . . . 9
106		2ndex 5112	. . . . . . . . . . 11
107	106	cnvex 5102	. . . . . . . . . 10
108	107	ins2ex 5797	. . . . . . . . 9 Ins2
109	105, 108	inex 4105	. . . . . . . 8 Ins2
110	109	si3ex 5806	. . . . . . 7 SI₃ Ins2
111	110	ins4ex 5799	. . . . . 6 Ins4 SI₃ Ins2
112		swapex 4742	. . . . . . . . . . . . 13 Swap
113	112	si3ex 5806	. . . . . . . . . . . 12 SI₃ Swap
114	113	ins4ex 5799	. . . . . . . . . . 11 Ins4 SI₃ Swap
115		ssetex 4744	. . . . . . . . . . . . . . 15 S
116	115	ins2ex 5797	. . . . . . . . . . . . . 14 Ins2 S
117	116	ins2ex 5797	. . . . . . . . . . . . 13 Ins2 Ins2 S
118	117	ins2ex 5797	. . . . . . . . . . . 12 Ins2 Ins2 Ins2 S
119	118	ins2ex 5797	. . . . . . . . . . 11 Ins2 Ins2 Ins2 Ins2 S
120	114, 119	inex 4105	. . . . . . . . . 10 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S
121		1cex 4142	. . . . . . . . . 10 1_c
122	120, 121	imaex 4747	. . . . . . . . 9 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c
123	122	ins2ex 5797	. . . . . . . 8 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c
124		idex 5504	. . . . . . . . . . . 12
125	124	si3ex 5806	. . . . . . . . . . 11 SI₃
126	125	ins4ex 5799	. . . . . . . . . 10 Ins4 SI₃
127	115	ins3ex 5798	. . . . . . . . . . . . . 14 Ins3 S
128	127	ins2ex 5797	. . . . . . . . . . . . 13 Ins2 Ins3 S
129	128	ins2ex 5797	. . . . . . . . . . . 12 Ins2 Ins2 Ins3 S
130	129	ins2ex 5797	. . . . . . . . . . 11 Ins2 Ins2 Ins2 Ins3 S
131	130	ins2ex 5797	. . . . . . . . . 10 Ins2 Ins2 Ins2 Ins2 Ins3 S
132	126, 131	inex 4105	. . . . . . . . 9 Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S
133	132, 121	imaex 4747	. . . . . . . 8 Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c
134	123, 133	inex 4105	. . . . . . 7 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c
135	134, 121	imaex 4747	. . . . . 6 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c
136	111, 135	inex 4105	. . . . 5 Ins4 SI₃ Ins2 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c
137	136, 121	imaex 4747	. . . 4 Ins4 SI₃ Ins2 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c1_c
138	137, 121	imaex 4747	. . 3 Ins4 SI₃ Ins2 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c1_c1_c
139	102, 102, 138	mpt2exlem 5811	. 2 Ins2 S Ins3 Ins4 SI₃ Ins2 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c1_c1_c1_c1_c
140	101, 139	eqeltri 2423	1 Compose

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 358

wex 1541

wceq 1642

wcel 1710

cvv 2859

cdif 3206

cin 3208

csymdif 3209

csn 3737 1_cc1c 4134

cop 4561

copab 4622 class class class wbr 4639

c1st 4717 Swap cswap 4718 S csset 4719

ccom 4721

cima 4722

cid 4763

cxp 4770

ccnv 4771

c2nd 4783

cmpt2 5653 Compose ccompose 5747 Ins2 cins2 5749 Ins3 cins3 5751 Ins4 cins4 5755 SI₃ csi3 5757

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-13 1712 ax-14 1714 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4078 ax-xp 4079 ax-cnv 4080 ax-1c 4081 ax-sset 4082 ax-si 4083 ax-ins2 4084 ax-ins3 4085 ax-typlower 4086 ax-sn 4087

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3or 935 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-eu 2208 df-mo 2209 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-ne 2518 df-ral 2619 df-rex 2620 df-reu 2621 df-rmo 2622 df-rab 2623 df-v 2861 df-sbc 3047 df-nin 3211 df-compl 3212 df-in 3213 df-un 3214 df-dif 3215 df-symdif 3216 df-ss 3259 df-pss 3261 df-nul 3551 df-if 3663 df-pw 3724 df-sn 3741 df-pr 3742 df-uni 3892 df-int 3927 df-opk 4058 df-1c 4136 df-pw1 4137 df-uni1 4138 df-xpk 4185 df-cnvk 4186 df-ins2k 4187 df-ins3k 4188 df-imak 4189 df-cok 4190 df-p6 4191 df-sik 4192 df-ssetk 4193 df-imagek 4194 df-idk 4195 df-iota 4339 df-0c 4377 df-addc 4378 df-nnc 4379 df-fin 4380 df-lefin 4440 df-ltfin 4441 df-ncfin 4442 df-tfin 4443 df-evenfin 4444 df-oddfin 4445 df-sfin 4446 df-spfin 4447 df-phi 4565 df-op 4566 df-proj1 4567 df-proj2 4568 df-opab 4623 df-br 4640 df-1st 4723 df-swap 4724 df-sset 4725 df-co 4726 df-ima 4727 df-si 4728 df-id 4767 df-xp 4784 df-cnv 4785 df-2nd 4797 df-oprab 5528 df-mpt2 5654 df-txp 5736 df-compose 5748 df-ins2 5750 df-ins3 5752 df-ins4 5756 df-si3 5758

This theorem is referenced by: enmap2lem1 6063 enmap1lem1 6069

W3C validator