composeex - New Foundations Explorer

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

Theorem composeex 5821

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 5749	. . 3 Compose
2		elopab 4697	. . . . 5 $/\$ $/\$ $/\$
3		df-co 4727	. . . . . 6 $/\$
4	3	eleq2i 2417	. . . . 5 $/\$
5		elima1c 4948	. . . . . 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 4948	. . . . . . . 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 3220	. . . . . . . . . 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 2863	. . . . . . . . . . . . . 14
9		vex 2863	. . . . . . . . . . . . . 14
10	8, 9	opex 4589	. . . . . . . . . . . . 13
11	10	oqelins4 5795	. . . . . . . . . . . 12 Ins4 SI₃ Ins2 SI₃ Ins2
12		vex 2863	. . . . . . . . . . . . 13
13		vex 2863	. . . . . . . . . . . . 13
14		vex 2863	. . . . . . . . . . . . 13
15	12, 13, 14	otsnelsi3 5806	. . . . . . . . . . . 12 SI₃ Ins2 Ins2
16		elin 3220	. . . . . . . . . . . . 13 Ins2 $/\$ Ins2
17		opelxp 4812	. . . . . . . . . . . . . . . 16 $/\$
18	12, 17	mpbiran 884	. . . . . . . . . . . . . . 15
19		df-br 4641	. . . . . . . . . . . . . . 15
20		brcnv 4893	. . . . . . . . . . . . . . 15
21	18, 19, 20	3bitr2i 264	. . . . . . . . . . . . . 14
22	13	otelins2 5792	. . . . . . . . . . . . . . 15 Ins2
23		df-br 4641	. . . . . . . . . . . . . . 15
24		brcnv 4893	. . . . . . . . . . . . . . 15
25	22, 23, 24	3bitr2i 264	. . . . . . . . . . . . . 14 Ins2
26	21, 25	anbi12i 678	. . . . . . . . . . . . 13 $/\$ Ins2 $/\$
27	13, 12	op1st2nd 5791	. . . . . . . . . . . . 13 $/\$
28	16, 26, 27	3bitri 262	. . . . . . . . . . . 12 Ins2
29	11, 15, 28	3bitri 262	. . . . . . . . . . 11 Ins4 SI₃ Ins2
30		elima1c 4948	. . . . . . . . . . . 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 3220	. . . . . . . . . . . . . 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 4112	. . . . . . . . . . . . . . . . 17
33	32	otelins2 5792	. . . . . . . . . . . . . . . 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 4641	. . . . . . . . . . . . . . . . 17
36		elima1c 4948	. . . . . . . . . . . . . . . . . 18 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S
37		elin 3220	. . . . . . . . . . . . . . . . . . . 20 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S Ins4 SI₃ Swap $/\$ Ins2 Ins2 Ins2 Ins2 S
38		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . 24
39	38, 10	opex 4589	. . . . . . . . . . . . . . . . . . . . . . 23
40	39	oqelins4 5795	. . . . . . . . . . . . . . . . . . . . . 22 Ins4 SI₃ Swap SI₃ Swap
41		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . 24
42	12, 41, 13	otsnelsi3 5806	. . . . . . . . . . . . . . . . . . . . . . 23 SI₃ Swap Swap
43		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . 23 Swap Swap
44	41, 13	brswap2 4861	. . . . . . . . . . . . . . . . . . . . . . 23 Swap
45	42, 43, 44	3bitr2i 264	. . . . . . . . . . . . . . . . . . . . . 22 SI₃ Swap
46	40, 45	bitri 240	. . . . . . . . . . . . . . . . . . . . 21 Ins4 SI₃ Swap
47		snex 4112	. . . . . . . . . . . . . . . . . . . . . . 23
48	47	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . 22 Ins2 Ins2 Ins2 Ins2 S Ins2 Ins2 Ins2 S
49		snex 4112	. . . . . . . . . . . . . . . . . . . . . . 23
50	49	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . 22 Ins2 Ins2 Ins2 S Ins2 Ins2 S
51	38	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . 23 Ins2 Ins2 S Ins2 S
52	8	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . 23 Ins2 S S
53	12, 9	opelssetsn 4761	. . . . . . . . . . . . . . . . . . . . . . 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 4641	. . . . . . . . . . . . . . . 16
64		elima1c 4948	. . . . . . . . . . . . . . . . 17 Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S
65		elin 3220	. . . . . . . . . . . . . . . . . . 19 Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S Ins4 SI₃ $/\$ Ins2 Ins2 Ins2 Ins2 Ins3 S
66	49, 39	opex 4589	. . . . . . . . . . . . . . . . . . . . . 22
67	66	oqelins4 5795	. . . . . . . . . . . . . . . . . . . . 21 Ins4 SI₃ SI₃
68		vex 2863	. . . . . . . . . . . . . . . . . . . . . . 23
69	68, 41, 12	otsnelsi3 5806	. . . . . . . . . . . . . . . . . . . . . 22 SI₃
70		df-br 4641	. . . . . . . . . . . . . . . . . . . . . 22
71	41, 12	opex 4589	. . . . . . . . . . . . . . . . . . . . . . 23
72	71	ideq 4871	. . . . . . . . . . . . . . . . . . . . . 22
73	69, 70, 72	3bitr2i 264	. . . . . . . . . . . . . . . . . . . . 21 SI₃
74	67, 73	bitri 240	. . . . . . . . . . . . . . . . . . . 20 Ins4 SI₃
75	47	otelins2 5792	. . . . . . . . . . . . . . . . . . . . 21 Ins2 Ins2 Ins2 Ins2 Ins3 S Ins2 Ins2 Ins2 Ins3 S
76	32	otelins2 5792	. . . . . . . . . . . . . . . . . . . . 21 Ins2 Ins2 Ins2 Ins3 S Ins2 Ins2 Ins3 S
77	49	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . 22 Ins2 Ins2 Ins3 S Ins2 Ins3 S
78	38	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . 22 Ins2 Ins3 S Ins3 S
79	9	otelins3 5793	. . . . . . . . . . . . . . . . . . . . . . 23 Ins3 S S
80	68, 8	opelssetsn 4761	. . . . . . . . . . . . . . . . . . . . . . 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 5810	. . 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 4110	. . 3
103		1stex 4740	. . . . . . . . . . 11
104	103	cnvex 5103	. . . . . . . . . 10
105	102, 104	xpex 5116	. . . . . . . . 9
106		2ndex 5113	. . . . . . . . . . 11
107	106	cnvex 5103	. . . . . . . . . 10
108	107	ins2ex 5798	. . . . . . . . 9 Ins2
109	105, 108	inex 4106	. . . . . . . 8 Ins2
110	109	si3ex 5807	. . . . . . 7 SI₃ Ins2
111	110	ins4ex 5800	. . . . . 6 Ins4 SI₃ Ins2
112		swapex 4743	. . . . . . . . . . . . 13 Swap
113	112	si3ex 5807	. . . . . . . . . . . 12 SI₃ Swap
114	113	ins4ex 5800	. . . . . . . . . . 11 Ins4 SI₃ Swap
115		ssetex 4745	. . . . . . . . . . . . . . 15 S
116	115	ins2ex 5798	. . . . . . . . . . . . . 14 Ins2 S
117	116	ins2ex 5798	. . . . . . . . . . . . 13 Ins2 Ins2 S
118	117	ins2ex 5798	. . . . . . . . . . . 12 Ins2 Ins2 Ins2 S
119	118	ins2ex 5798	. . . . . . . . . . 11 Ins2 Ins2 Ins2 Ins2 S
120	114, 119	inex 4106	. . . . . . . . . 10 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S
121		1cex 4143	. . . . . . . . . 10 1_c
122	120, 121	imaex 4748	. . . . . . . . 9 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c
123	122	ins2ex 5798	. . . . . . . 8 Ins2 Ins4 SI₃ Swap Ins2 Ins2 Ins2 Ins2 S 1_c
124		idex 5505	. . . . . . . . . . . 12
125	124	si3ex 5807	. . . . . . . . . . 11 SI₃
126	125	ins4ex 5800	. . . . . . . . . 10 Ins4 SI₃
127	115	ins3ex 5799	. . . . . . . . . . . . . 14 Ins3 S
128	127	ins2ex 5798	. . . . . . . . . . . . 13 Ins2 Ins3 S
129	128	ins2ex 5798	. . . . . . . . . . . 12 Ins2 Ins2 Ins3 S
130	129	ins2ex 5798	. . . . . . . . . . 11 Ins2 Ins2 Ins2 Ins3 S
131	130	ins2ex 5798	. . . . . . . . . 10 Ins2 Ins2 Ins2 Ins2 Ins3 S
132	126, 131	inex 4106	. . . . . . . . 9 Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S
133	132, 121	imaex 4748	. . . . . . . 8 Ins4 SI₃ Ins2 Ins2 Ins2 Ins2 Ins3 S 1_c
134	123, 133	inex 4106	. . . . . . 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 4748	. . . . . 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 4106	. . . . 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 4748	. . . 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 4748	. . 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 5812	. 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 2860

cdif 3207

cin 3209

csymdif 3210

csn 3738 1_cc1c 4135

cop 4562

copab 4623 class class class wbr 4640

c1st 4718 Swap cswap 4719 S csset 4720

ccom 4722

cima 4723

cid 4764

cxp 4771

ccnv 4772

c2nd 4784

cmpt2 5654 Compose ccompose 5748 Ins2 cins2 5750 Ins3 cins3 5752 Ins4 cins4 5756 SI₃ csi3 5758

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 4079 ax-xp 4080 ax-cnv 4081 ax-1c 4082 ax-sset 4083 ax-si 4084 ax-ins2 4085 ax-ins3 4086 ax-typlower 4087 ax-sn 4088

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 2479 df-ne 2519 df-ral 2620 df-rex 2621 df-reu 2622 df-rmo 2623 df-rab 2624 df-v 2862 df-sbc 3048 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-ss 3260 df-pss 3262 df-nul 3552 df-if 3664 df-pw 3725 df-sn 3742 df-pr 3743 df-uni 3893 df-int 3928 df-opk 4059 df-1c 4137 df-pw1 4138 df-uni1 4139 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-cok 4191 df-p6 4192 df-sik 4193 df-ssetk 4194 df-imagek 4195 df-idk 4196 df-iota 4340 df-0c 4378 df-addc 4379 df-nnc 4380 df-fin 4381 df-lefin 4441 df-ltfin 4442 df-ncfin 4443 df-tfin 4444 df-evenfin 4445 df-oddfin 4446 df-sfin 4447 df-spfin 4448 df-phi 4566 df-op 4567 df-proj1 4568 df-proj2 4569 df-opab 4624 df-br 4641 df-1st 4724 df-swap 4725 df-sset 4726 df-co 4727 df-ima 4728 df-si 4729 df-id 4768 df-xp 4785 df-cnv 4786 df-2nd 4798 df-oprab 5529 df-mpt2 5655 df-txp 5737 df-compose 5749 df-ins2 5751 df-ins3 5753 df-ins4 5757 df-si3 5759

This theorem is referenced by: enmap2lem1 6064 enmap1lem1 6070

W3C validator