Theorem composeex 5820

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

Assertion

Ref	Expression
composeex	⊢ Compose ∈ V

Proof of Theorem composeex

Dummy variables x y z w t u v are mutually distinct and distinct from all other variables.

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

Syntax hints:   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2859   ∖ cdif 3206   ∩ cin 3208   ⊕ csymdif 3209  {csn 3737  1_cc1c 4134  ⟨cop 4561  {copab 4622   class class class wbr 4639  1^st c1st 4717   Swap cswap 4718   S csset 4719   ∘ ccom 4721   “ cima 4722   I cid 4763   × cxp 4770  ^◡ccnv 4771  2^nd 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