Theorem usgrexmpl2lem

Description: Lemma for usgrexmpl2 . (Contributed by AV, 3-Aug-2025)

	Ref	Expression
Hypotheses	usgrexmpl2.v	$$⊢V=\left(0\dots 5\right)$$
	usgrexmpl2.e	$$⊢E=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩$$
Assertion	usgrexmpl2lem	$$⊢E:\mathrm{dom}E\underset{1-1}{⟶}\left\{e\in 𝒫V|\left|e\right|=2\right\}$$

Proof

Step	Hyp	Ref	Expression
1		usgrexmpl2.v	$$⊢V=\left(0\dots 5\right)$$
2		usgrexmpl2.e	$$⊢E=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩$$
3		prex	$$⊢\left\{0,1\right\}\in \mathrm{V}$$
4		prex	$$⊢\left\{1,2\right\}\in \mathrm{V}$$
5		prex	$$⊢\left\{2,3\right\}\in \mathrm{V}$$
6	3 4 5	3pm3.2i	$$⊢\left(\left\{0,1\right\}\in \mathrm{V}\wedge \left\{1,2\right\}\in \mathrm{V}\wedge \left\{2,3\right\}\in \mathrm{V}\right)$$
7		prex	$$⊢\left\{3,4\right\}\in \mathrm{V}$$
8		prex	$$⊢\left\{4,5\right\}\in \mathrm{V}$$
9		prex	$$⊢\left\{0,3\right\}\in \mathrm{V}$$
10		prex	$$⊢\left\{0,5\right\}\in \mathrm{V}$$
11	8 9 10	3pm3.2i	$$⊢\left(\left\{4,5\right\}\in \mathrm{V}\wedge \left\{0,3\right\}\in \mathrm{V}\wedge \left\{0,5\right\}\in \mathrm{V}\right)$$
12	6 7 11	3pm3.2i	$$⊢\left(\left(\left\{0,1\right\}\in \mathrm{V}\wedge \left\{1,2\right\}\in \mathrm{V}\wedge \left\{2,3\right\}\in \mathrm{V}\right)\wedge \left\{3,4\right\}\in \mathrm{V}\wedge \left(\left\{4,5\right\}\in \mathrm{V}\wedge \left\{0,3\right\}\in \mathrm{V}\wedge \left\{0,5\right\}\in \mathrm{V}\right)\right)$$
13		0nn0	$$⊢0\in {\mathbb{N}}_0$$
14		1nn0	$$⊢1\in {\mathbb{N}}_0$$
15	13 14	pm3.2i	$$⊢\left(0\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)$$
16		2nn0	$$⊢2\in {\mathbb{N}}_0$$
17	14 16	pm3.2i	$$⊢\left(1\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)$$
18	15 17	pm3.2i	$$⊢\left(\left(0\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\wedge \left(1\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\right)$$
19		0ne1	$$⊢0\ne 1$$
20		0ne2	$$⊢0\ne 2$$
21	19 20	pm3.2i	$$⊢\left(0\ne 1\wedge 0\ne 2\right)$$
22	21	orci	$$⊢\left(\left(0\ne 1\wedge 0\ne 2\right)\vee \left(1\ne 1\wedge 1\ne 2\right)\right)$$
23		prneimg	$$⊢\left(\left(0\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\wedge \left(1\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(0\ne 1\wedge 0\ne 2\right)\vee \left(1\ne 1\wedge 1\ne 2\right)\right)\to \left\{0,1\right\}\ne \left\{1,2\right\}\right)$$
24	18 22 23	mp2	$$⊢\left\{0,1\right\}\ne \left\{1,2\right\}$$
25		3nn0	$$⊢3\in {\mathbb{N}}_0$$
26	16 25	pm3.2i	$$⊢\left(2\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)$$
27	15 26	pm3.2i	$$⊢\left(\left(0\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\wedge \left(2\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\right)$$
28		0re	$$⊢0\in ℝ$$
29		3pos	$$⊢0<3$$
30	28 29	ltneii	$$⊢0\ne 3$$
31	20 30	pm3.2i	$$⊢\left(0\ne 2\wedge 0\ne 3\right)$$
32	31	orci	$$⊢\left(\left(0\ne 2\wedge 0\ne 3\right)\vee \left(1\ne 2\wedge 1\ne 3\right)\right)$$
33		prneimg	$$⊢\left(\left(0\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\wedge \left(2\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(0\ne 2\wedge 0\ne 3\right)\vee \left(1\ne 2\wedge 1\ne 3\right)\right)\to \left\{0,1\right\}\ne \left\{2,3\right\}\right)$$
34	27 32 33	mp2	$$⊢\left\{0,1\right\}\ne \left\{2,3\right\}$$
35		4nn0	$$⊢4\in {\mathbb{N}}_0$$
36	25 35	pm3.2i	$$⊢\left(3\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\right)$$
37	15 36	pm3.2i	$$⊢\left(\left(0\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\wedge \left(3\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\right)\right)$$
38		4pos	$$⊢0<4$$
39	28 38	ltneii	$$⊢0\ne 4$$
40	30 39	pm3.2i	$$⊢\left(0\ne 3\wedge 0\ne 4\right)$$
41	40	orci	$$⊢\left(\left(0\ne 3\wedge 0\ne 4\right)\vee \left(1\ne 3\wedge 1\ne 4\right)\right)$$
42		prneimg	$$⊢\left(\left(0\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\wedge \left(3\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(0\ne 3\wedge 0\ne 4\right)\vee \left(1\ne 3\wedge 1\ne 4\right)\right)\to \left\{0,1\right\}\ne \left\{3,4\right\}\right)$$
43	37 41 42	mp2	$$⊢\left\{0,1\right\}\ne \left\{3,4\right\}$$
44	24 34 43	3pm3.2i	$$⊢\left(\left\{0,1\right\}\ne \left\{1,2\right\}\wedge \left\{0,1\right\}\ne \left\{2,3\right\}\wedge \left\{0,1\right\}\ne \left\{3,4\right\}\right)$$
45		5nn0	$$⊢5\in {\mathbb{N}}_0$$
46	35 45	pm3.2i	$$⊢\left(4\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)$$
47	15 46	pm3.2i	$$⊢\left(\left(0\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\wedge \left(4\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)$$
48		5pos	$$⊢0<5$$
49	28 48	ltneii	$$⊢0\ne 5$$
50	39 49	pm3.2i	$$⊢\left(0\ne 4\wedge 0\ne 5\right)$$
51	50	orci	$$⊢\left(\left(0\ne 4\wedge 0\ne 5\right)\vee \left(1\ne 4\wedge 1\ne 5\right)\right)$$
52		prneimg	$$⊢\left(\left(0\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\wedge \left(4\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(0\ne 4\wedge 0\ne 5\right)\vee \left(1\ne 4\wedge 1\ne 5\right)\right)\to \left\{0,1\right\}\ne \left\{4,5\right\}\right)$$
53	47 51 52	mp2	$$⊢\left\{0,1\right\}\ne \left\{4,5\right\}$$
54	13 25	pm3.2i	$$⊢\left(0\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)$$
55	15 54	pm3.2i	$$⊢\left(\left(0\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\right)$$
56		ax-1ne0	$$⊢1\ne 0$$
57		1re	$$⊢1\in ℝ$$
58		1lt3	$$⊢1<3$$
59	57 58	ltneii	$$⊢1\ne 3$$
60	56 59	pm3.2i	$$⊢\left(1\ne 0\wedge 1\ne 3\right)$$
61	60	olci	$$⊢\left(\left(0\ne 0\wedge 0\ne 3\right)\vee \left(1\ne 0\wedge 1\ne 3\right)\right)$$
62		prneimg	$$⊢\left(\left(0\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(0\ne 0\wedge 0\ne 3\right)\vee \left(1\ne 0\wedge 1\ne 3\right)\right)\to \left\{0,1\right\}\ne \left\{0,3\right\}\right)$$
63	55 61 62	mp2	$$⊢\left\{0,1\right\}\ne \left\{0,3\right\}$$
64	13 45	pm3.2i	$$⊢\left(0\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)$$
65	15 64	pm3.2i	$$⊢\left(\left(0\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)$$
66		1lt5	$$⊢1<5$$
67	57 66	ltneii	$$⊢1\ne 5$$
68	56 67	pm3.2i	$$⊢\left(1\ne 0\wedge 1\ne 5\right)$$
69	68	olci	$$⊢\left(\left(0\ne 0\wedge 0\ne 5\right)\vee \left(1\ne 0\wedge 1\ne 5\right)\right)$$
70		prneimg	$$⊢\left(\left(0\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(0\ne 0\wedge 0\ne 5\right)\vee \left(1\ne 0\wedge 1\ne 5\right)\right)\to \left\{0,1\right\}\ne \left\{0,5\right\}\right)$$
71	65 69 70	mp2	$$⊢\left\{0,1\right\}\ne \left\{0,5\right\}$$
72	53 63 71	3pm3.2i	$$⊢\left(\left\{0,1\right\}\ne \left\{4,5\right\}\wedge \left\{0,1\right\}\ne \left\{0,3\right\}\wedge \left\{0,1\right\}\ne \left\{0,5\right\}\right)$$
73	44 72	pm3.2i	$$⊢\left(\left(\left\{0,1\right\}\ne \left\{1,2\right\}\wedge \left\{0,1\right\}\ne \left\{2,3\right\}\wedge \left\{0,1\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{0,1\right\}\ne \left\{4,5\right\}\wedge \left\{0,1\right\}\ne \left\{0,3\right\}\wedge \left\{0,1\right\}\ne \left\{0,5\right\}\right)\right)$$
74	17 26	pm3.2i	$$⊢\left(\left(1\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\wedge \left(2\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\right)$$
75		1ne2	$$⊢1\ne 2$$
76	75 59	pm3.2i	$$⊢\left(1\ne 2\wedge 1\ne 3\right)$$
77	76	orci	$$⊢\left(\left(1\ne 2\wedge 1\ne 3\right)\vee \left(2\ne 2\wedge 2\ne 3\right)\right)$$
78		prneimg	$$⊢\left(\left(1\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\wedge \left(2\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(1\ne 2\wedge 1\ne 3\right)\vee \left(2\ne 2\wedge 2\ne 3\right)\right)\to \left\{1,2\right\}\ne \left\{2,3\right\}\right)$$
79	74 77 78	mp2	$$⊢\left\{1,2\right\}\ne \left\{2,3\right\}$$
80	17 36	pm3.2i	$$⊢\left(\left(1\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\wedge \left(3\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\right)\right)$$
81		1lt4	$$⊢1<4$$
82	57 81	ltneii	$$⊢1\ne 4$$
83	59 82	pm3.2i	$$⊢\left(1\ne 3\wedge 1\ne 4\right)$$
84	83	orci	$$⊢\left(\left(1\ne 3\wedge 1\ne 4\right)\vee \left(2\ne 3\wedge 2\ne 4\right)\right)$$
85		prneimg	$$⊢\left(\left(1\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\wedge \left(3\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(1\ne 3\wedge 1\ne 4\right)\vee \left(2\ne 3\wedge 2\ne 4\right)\right)\to \left\{1,2\right\}\ne \left\{3,4\right\}\right)$$
86	80 84 85	mp2	$$⊢\left\{1,2\right\}\ne \left\{3,4\right\}$$
87	79 86	pm3.2i	$$⊢\left(\left\{1,2\right\}\ne \left\{2,3\right\}\wedge \left\{1,2\right\}\ne \left\{3,4\right\}\right)$$
88	17 46	pm3.2i	$$⊢\left(\left(1\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\wedge \left(4\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)$$
89	82 67	pm3.2i	$$⊢\left(1\ne 4\wedge 1\ne 5\right)$$
90	89	orci	$$⊢\left(\left(1\ne 4\wedge 1\ne 5\right)\vee \left(2\ne 4\wedge 2\ne 5\right)\right)$$
91		prneimg	$$⊢\left(\left(1\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\wedge \left(4\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(1\ne 4\wedge 1\ne 5\right)\vee \left(2\ne 4\wedge 2\ne 5\right)\right)\to \left\{1,2\right\}\ne \left\{4,5\right\}\right)$$
92	88 90 91	mp2	$$⊢\left\{1,2\right\}\ne \left\{4,5\right\}$$
93	17 54	pm3.2i	$$⊢\left(\left(1\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\right)$$
94	60	orci	$$⊢\left(\left(1\ne 0\wedge 1\ne 3\right)\vee \left(2\ne 0\wedge 2\ne 3\right)\right)$$
95		prneimg	$$⊢\left(\left(1\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(1\ne 0\wedge 1\ne 3\right)\vee \left(2\ne 0\wedge 2\ne 3\right)\right)\to \left\{1,2\right\}\ne \left\{0,3\right\}\right)$$
96	93 94 95	mp2	$$⊢\left\{1,2\right\}\ne \left\{0,3\right\}$$
97	17 64	pm3.2i	$$⊢\left(\left(1\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)$$
98	68	orci	$$⊢\left(\left(1\ne 0\wedge 1\ne 5\right)\vee \left(2\ne 0\wedge 2\ne 5\right)\right)$$
99		prneimg	$$⊢\left(\left(1\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(1\ne 0\wedge 1\ne 5\right)\vee \left(2\ne 0\wedge 2\ne 5\right)\right)\to \left\{1,2\right\}\ne \left\{0,5\right\}\right)$$
100	97 98 99	mp2	$$⊢\left\{1,2\right\}\ne \left\{0,5\right\}$$
101	92 96 100	3pm3.2i	$$⊢\left(\left\{1,2\right\}\ne \left\{4,5\right\}\wedge \left\{1,2\right\}\ne \left\{0,3\right\}\wedge \left\{1,2\right\}\ne \left\{0,5\right\}\right)$$
102	87 101	pm3.2i	$$⊢\left(\left(\left\{1,2\right\}\ne \left\{2,3\right\}\wedge \left\{1,2\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{1,2\right\}\ne \left\{4,5\right\}\wedge \left\{1,2\right\}\ne \left\{0,3\right\}\wedge \left\{1,2\right\}\ne \left\{0,5\right\}\right)\right)$$
103	26 36	pm3.2i	$$⊢\left(\left(2\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\wedge \left(3\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\right)\right)$$
104		2re	$$⊢2\in ℝ$$
105		2lt3	$$⊢2<3$$
106	104 105	ltneii	$$⊢2\ne 3$$
107		2lt4	$$⊢2<4$$
108	104 107	ltneii	$$⊢2\ne 4$$
109	106 108	pm3.2i	$$⊢\left(2\ne 3\wedge 2\ne 4\right)$$
110	109	orci	$$⊢\left(\left(2\ne 3\wedge 2\ne 4\right)\vee \left(3\ne 3\wedge 3\ne 4\right)\right)$$
111		prneimg	$$⊢\left(\left(2\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\wedge \left(3\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(2\ne 3\wedge 2\ne 4\right)\vee \left(3\ne 3\wedge 3\ne 4\right)\right)\to \left\{2,3\right\}\ne \left\{3,4\right\}\right)$$
112	103 110 111	mp2	$$⊢\left\{2,3\right\}\ne \left\{3,4\right\}$$
113	26 46	pm3.2i	$$⊢\left(\left(2\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\wedge \left(4\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)$$
114		2lt5	$$⊢2<5$$
115	104 114	ltneii	$$⊢2\ne 5$$
116	108 115	pm3.2i	$$⊢\left(2\ne 4\wedge 2\ne 5\right)$$
117	116	orci	$$⊢\left(\left(2\ne 4\wedge 2\ne 5\right)\vee \left(3\ne 4\wedge 3\ne 5\right)\right)$$
118		prneimg	$$⊢\left(\left(2\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\wedge \left(4\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(2\ne 4\wedge 2\ne 5\right)\vee \left(3\ne 4\wedge 3\ne 5\right)\right)\to \left\{2,3\right\}\ne \left\{4,5\right\}\right)$$
119	113 117 118	mp2	$$⊢\left\{2,3\right\}\ne \left\{4,5\right\}$$
120	26 54	pm3.2i	$$⊢\left(\left(2\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\right)$$
121		2ne0	$$⊢2\ne 0$$
122	121 106	pm3.2i	$$⊢\left(2\ne 0\wedge 2\ne 3\right)$$
123	122	orci	$$⊢\left(\left(2\ne 0\wedge 2\ne 3\right)\vee \left(3\ne 0\wedge 3\ne 3\right)\right)$$
124		prneimg	$$⊢\left(\left(2\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(2\ne 0\wedge 2\ne 3\right)\vee \left(3\ne 0\wedge 3\ne 3\right)\right)\to \left\{2,3\right\}\ne \left\{0,3\right\}\right)$$
125	120 123 124	mp2	$$⊢\left\{2,3\right\}\ne \left\{0,3\right\}$$
126	26 64	pm3.2i	$$⊢\left(\left(2\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)$$
127	121 115	pm3.2i	$$⊢\left(2\ne 0\wedge 2\ne 5\right)$$
128	127	orci	$$⊢\left(\left(2\ne 0\wedge 2\ne 5\right)\vee \left(3\ne 0\wedge 3\ne 5\right)\right)$$
129		prneimg	$$⊢\left(\left(2\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(2\ne 0\wedge 2\ne 5\right)\vee \left(3\ne 0\wedge 3\ne 5\right)\right)\to \left\{2,3\right\}\ne \left\{0,5\right\}\right)$$
130	126 128 129	mp2	$$⊢\left\{2,3\right\}\ne \left\{0,5\right\}$$
131	119 125 130	3pm3.2i	$$⊢\left(\left\{2,3\right\}\ne \left\{4,5\right\}\wedge \left\{2,3\right\}\ne \left\{0,3\right\}\wedge \left\{2,3\right\}\ne \left\{0,5\right\}\right)$$
132	112 131	pm3.2i	$$⊢\left(\left\{2,3\right\}\ne \left\{3,4\right\}\wedge \left(\left\{2,3\right\}\ne \left\{4,5\right\}\wedge \left\{2,3\right\}\ne \left\{0,3\right\}\wedge \left\{2,3\right\}\ne \left\{0,5\right\}\right)\right)$$
133	73 102 132	3pm3.2i	$$⊢\left(\left(\left(\left\{0,1\right\}\ne \left\{1,2\right\}\wedge \left\{0,1\right\}\ne \left\{2,3\right\}\wedge \left\{0,1\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{0,1\right\}\ne \left\{4,5\right\}\wedge \left\{0,1\right\}\ne \left\{0,3\right\}\wedge \left\{0,1\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left(\left\{1,2\right\}\ne \left\{2,3\right\}\wedge \left\{1,2\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{1,2\right\}\ne \left\{4,5\right\}\wedge \left\{1,2\right\}\ne \left\{0,3\right\}\wedge \left\{1,2\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left\{2,3\right\}\ne \left\{3,4\right\}\wedge \left(\left\{2,3\right\}\ne \left\{4,5\right\}\wedge \left\{2,3\right\}\ne \left\{0,3\right\}\wedge \left\{2,3\right\}\ne \left\{0,5\right\}\right)\right)\right)$$
134	36 46	pm3.2i	$$⊢\left(\left(3\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\right)\wedge \left(4\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)$$
135		3re	$$⊢3\in ℝ$$
136		3lt4	$$⊢3<4$$
137	135 136	ltneii	$$⊢3\ne 4$$
138		3lt5	$$⊢3<5$$
139	135 138	ltneii	$$⊢3\ne 5$$
140	137 139	pm3.2i	$$⊢\left(3\ne 4\wedge 3\ne 5\right)$$
141	140	orci	$$⊢\left(\left(3\ne 4\wedge 3\ne 5\right)\vee \left(4\ne 4\wedge 4\ne 5\right)\right)$$
142		prneimg	$$⊢\left(\left(3\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\right)\wedge \left(4\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(3\ne 4\wedge 3\ne 5\right)\vee \left(4\ne 4\wedge 4\ne 5\right)\right)\to \left\{3,4\right\}\ne \left\{4,5\right\}\right)$$
143	134 141 142	mp2	$$⊢\left\{3,4\right\}\ne \left\{4,5\right\}$$
144	36 54	pm3.2i	$$⊢\left(\left(3\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\right)$$
145		4ne0	$$⊢4\ne 0$$
146	137	necomi	$$⊢4\ne 3$$
147	145 146	pm3.2i	$$⊢\left(4\ne 0\wedge 4\ne 3\right)$$
148	147	olci	$$⊢\left(\left(3\ne 0\wedge 3\ne 3\right)\vee \left(4\ne 0\wedge 4\ne 3\right)\right)$$
149		prneimg	$$⊢\left(\left(3\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(3\ne 0\wedge 3\ne 3\right)\vee \left(4\ne 0\wedge 4\ne 3\right)\right)\to \left\{3,4\right\}\ne \left\{0,3\right\}\right)$$
150	144 148 149	mp2	$$⊢\left\{3,4\right\}\ne \left\{0,3\right\}$$
151	36 64	pm3.2i	$$⊢\left(\left(3\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)$$
152		3ne0	$$⊢3\ne 0$$
153	152 139	pm3.2i	$$⊢\left(3\ne 0\wedge 3\ne 5\right)$$
154	153	orci	$$⊢\left(\left(3\ne 0\wedge 3\ne 5\right)\vee \left(4\ne 0\wedge 4\ne 5\right)\right)$$
155		prneimg	$$⊢\left(\left(3\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(3\ne 0\wedge 3\ne 5\right)\vee \left(4\ne 0\wedge 4\ne 5\right)\right)\to \left\{3,4\right\}\ne \left\{0,5\right\}\right)$$
156	151 154 155	mp2	$$⊢\left\{3,4\right\}\ne \left\{0,5\right\}$$
157	143 150 156	3pm3.2i	$$⊢\left(\left\{3,4\right\}\ne \left\{4,5\right\}\wedge \left\{3,4\right\}\ne \left\{0,3\right\}\wedge \left\{3,4\right\}\ne \left\{0,5\right\}\right)$$
158	46 54	pm3.2i	$$⊢\left(\left(4\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\right)$$
159	147	orci	$$⊢\left(\left(4\ne 0\wedge 4\ne 3\right)\vee \left(5\ne 0\wedge 5\ne 3\right)\right)$$
160		prneimg	$$⊢\left(\left(4\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(4\ne 0\wedge 4\ne 3\right)\vee \left(5\ne 0\wedge 5\ne 3\right)\right)\to \left\{4,5\right\}\ne \left\{0,3\right\}\right)$$
161	158 159 160	mp2	$$⊢\left\{4,5\right\}\ne \left\{0,3\right\}$$
162	46 64	pm3.2i	$$⊢\left(\left(4\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)$$
163		4re	$$⊢4\in ℝ$$
164		4lt5	$$⊢4<5$$
165	163 164	ltneii	$$⊢4\ne 5$$
166	145 165	pm3.2i	$$⊢\left(4\ne 0\wedge 4\ne 5\right)$$
167	166	orci	$$⊢\left(\left(4\ne 0\wedge 4\ne 5\right)\vee \left(5\ne 0\wedge 5\ne 5\right)\right)$$
168		prneimg	$$⊢\left(\left(4\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(4\ne 0\wedge 4\ne 5\right)\vee \left(5\ne 0\wedge 5\ne 5\right)\right)\to \left\{4,5\right\}\ne \left\{0,5\right\}\right)$$
169	162 167 168	mp2	$$⊢\left\{4,5\right\}\ne \left\{0,5\right\}$$
170	54 64	pm3.2i	$$⊢\left(\left(0\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)$$
171	153	olci	$$⊢\left(\left(0\ne 0\wedge 0\ne 5\right)\vee \left(3\ne 0\wedge 3\ne 5\right)\right)$$
172		prneimg	$$⊢\left(\left(0\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\wedge \left(0\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\right)\right)\to \left(\left(\left(0\ne 0\wedge 0\ne 5\right)\vee \left(3\ne 0\wedge 3\ne 5\right)\right)\to \left\{0,3\right\}\ne \left\{0,5\right\}\right)$$
173	170 171 172	mp2	$$⊢\left\{0,3\right\}\ne \left\{0,5\right\}$$
174	161 169 173	3pm3.2i	$$⊢\left(\left\{4,5\right\}\ne \left\{0,3\right\}\wedge \left\{4,5\right\}\ne \left\{0,5\right\}\wedge \left\{0,3\right\}\ne \left\{0,5\right\}\right)$$
175	157 174	pm3.2i	$$⊢\left(\left(\left\{3,4\right\}\ne \left\{4,5\right\}\wedge \left\{3,4\right\}\ne \left\{0,3\right\}\wedge \left\{3,4\right\}\ne \left\{0,5\right\}\right)\wedge \left(\left\{4,5\right\}\ne \left\{0,3\right\}\wedge \left\{4,5\right\}\ne \left\{0,5\right\}\wedge \left\{0,3\right\}\ne \left\{0,5\right\}\right)\right)$$
176	133 175	pm3.2i	$$⊢\left(\left(\left(\left(\left\{0,1\right\}\ne \left\{1,2\right\}\wedge \left\{0,1\right\}\ne \left\{2,3\right\}\wedge \left\{0,1\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{0,1\right\}\ne \left\{4,5\right\}\wedge \left\{0,1\right\}\ne \left\{0,3\right\}\wedge \left\{0,1\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left(\left\{1,2\right\}\ne \left\{2,3\right\}\wedge \left\{1,2\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{1,2\right\}\ne \left\{4,5\right\}\wedge \left\{1,2\right\}\ne \left\{0,3\right\}\wedge \left\{1,2\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left\{2,3\right\}\ne \left\{3,4\right\}\wedge \left(\left\{2,3\right\}\ne \left\{4,5\right\}\wedge \left\{2,3\right\}\ne \left\{0,3\right\}\wedge \left\{2,3\right\}\ne \left\{0,5\right\}\right)\right)\right)\wedge \left(\left(\left\{3,4\right\}\ne \left\{4,5\right\}\wedge \left\{3,4\right\}\ne \left\{0,3\right\}\wedge \left\{3,4\right\}\ne \left\{0,5\right\}\right)\wedge \left(\left\{4,5\right\}\ne \left\{0,3\right\}\wedge \left\{4,5\right\}\ne \left\{0,5\right\}\wedge \left\{0,3\right\}\ne \left\{0,5\right\}\right)\right)\right)$$
177	12 176	pm3.2i	$$⊢\left(\left(\left(\left\{0,1\right\}\in \mathrm{V}\wedge \left\{1,2\right\}\in \mathrm{V}\wedge \left\{2,3\right\}\in \mathrm{V}\right)\wedge \left\{3,4\right\}\in \mathrm{V}\wedge \left(\left\{4,5\right\}\in \mathrm{V}\wedge \left\{0,3\right\}\in \mathrm{V}\wedge \left\{0,5\right\}\in \mathrm{V}\right)\right)\wedge \left(\left(\left(\left(\left\{0,1\right\}\ne \left\{1,2\right\}\wedge \left\{0,1\right\}\ne \left\{2,3\right\}\wedge \left\{0,1\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{0,1\right\}\ne \left\{4,5\right\}\wedge \left\{0,1\right\}\ne \left\{0,3\right\}\wedge \left\{0,1\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left(\left\{1,2\right\}\ne \left\{2,3\right\}\wedge \left\{1,2\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{1,2\right\}\ne \left\{4,5\right\}\wedge \left\{1,2\right\}\ne \left\{0,3\right\}\wedge \left\{1,2\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left\{2,3\right\}\ne \left\{3,4\right\}\wedge \left(\left\{2,3\right\}\ne \left\{4,5\right\}\wedge \left\{2,3\right\}\ne \left\{0,3\right\}\wedge \left\{2,3\right\}\ne \left\{0,5\right\}\right)\right)\right)\wedge \left(\left(\left\{3,4\right\}\ne \left\{4,5\right\}\wedge \left\{3,4\right\}\ne \left\{0,3\right\}\wedge \left\{3,4\right\}\ne \left\{0,5\right\}\right)\wedge \left(\left\{4,5\right\}\ne \left\{0,3\right\}\wedge \left\{4,5\right\}\ne \left\{0,5\right\}\wedge \left\{0,3\right\}\ne \left\{0,5\right\}\right)\right)\right)\right)$$
178		s7f1o	$$⊢\left(\left(\left(\left\{0,1\right\}\in \mathrm{V}\wedge \left\{1,2\right\}\in \mathrm{V}\wedge \left\{2,3\right\}\in \mathrm{V}\right)\wedge \left\{3,4\right\}\in \mathrm{V}\wedge \left(\left\{4,5\right\}\in \mathrm{V}\wedge \left\{0,3\right\}\in \mathrm{V}\wedge \left\{0,5\right\}\in \mathrm{V}\right)\right)\wedge \left(\left(\left(\left(\left\{0,1\right\}\ne \left\{1,2\right\}\wedge \left\{0,1\right\}\ne \left\{2,3\right\}\wedge \left\{0,1\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{0,1\right\}\ne \left\{4,5\right\}\wedge \left\{0,1\right\}\ne \left\{0,3\right\}\wedge \left\{0,1\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left(\left\{1,2\right\}\ne \left\{2,3\right\}\wedge \left\{1,2\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{1,2\right\}\ne \left\{4,5\right\}\wedge \left\{1,2\right\}\ne \left\{0,3\right\}\wedge \left\{1,2\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left\{2,3\right\}\ne \left\{3,4\right\}\wedge \left(\left\{2,3\right\}\ne \left\{4,5\right\}\wedge \left\{2,3\right\}\ne \left\{0,3\right\}\wedge \left\{2,3\right\}\ne \left\{0,5\right\}\right)\right)\right)\wedge \left(\left(\left\{3,4\right\}\ne \left\{4,5\right\}\wedge \left\{3,4\right\}\ne \left\{0,3\right\}\wedge \left\{3,4\right\}\ne \left\{0,5\right\}\right)\wedge \left(\left\{4,5\right\}\ne \left\{0,3\right\}\wedge \left\{4,5\right\}\ne \left\{0,5\right\}\wedge \left\{0,3\right\}\ne \left\{0,5\right\}\right)\right)\right)\right)\to \left(E=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\to E:\left(0..^7\right)\underset{1-1\; onto}{⟶}\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\right)$$
179	178	imp	$$⊢\left(\left(\left(\left(\left\{0,1\right\}\in \mathrm{V}\wedge \left\{1,2\right\}\in \mathrm{V}\wedge \left\{2,3\right\}\in \mathrm{V}\right)\wedge \left\{3,4\right\}\in \mathrm{V}\wedge \left(\left\{4,5\right\}\in \mathrm{V}\wedge \left\{0,3\right\}\in \mathrm{V}\wedge \left\{0,5\right\}\in \mathrm{V}\right)\right)\wedge \left(\left(\left(\left(\left\{0,1\right\}\ne \left\{1,2\right\}\wedge \left\{0,1\right\}\ne \left\{2,3\right\}\wedge \left\{0,1\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{0,1\right\}\ne \left\{4,5\right\}\wedge \left\{0,1\right\}\ne \left\{0,3\right\}\wedge \left\{0,1\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left(\left\{1,2\right\}\ne \left\{2,3\right\}\wedge \left\{1,2\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{1,2\right\}\ne \left\{4,5\right\}\wedge \left\{1,2\right\}\ne \left\{0,3\right\}\wedge \left\{1,2\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left\{2,3\right\}\ne \left\{3,4\right\}\wedge \left(\left\{2,3\right\}\ne \left\{4,5\right\}\wedge \left\{2,3\right\}\ne \left\{0,3\right\}\wedge \left\{2,3\right\}\ne \left\{0,5\right\}\right)\right)\right)\wedge \left(\left(\left\{3,4\right\}\ne \left\{4,5\right\}\wedge \left\{3,4\right\}\ne \left\{0,3\right\}\wedge \left\{3,4\right\}\ne \left\{0,5\right\}\right)\wedge \left(\left\{4,5\right\}\ne \left\{0,3\right\}\wedge \left\{4,5\right\}\ne \left\{0,5\right\}\wedge \left\{0,3\right\}\ne \left\{0,5\right\}\right)\right)\right)\right)\wedge E=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\right)\to E:\left(0..^7\right)\underset{1-1\; onto}{⟶}\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}$$
180		s7len	$$⊢\left|⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\right|=7$$
181	180	oveq2i	$$⊢\left(0..^\left|⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\right|\right)=\left(0..^7\right)$$
182		f1oeq2	$$⊢\left(0..^\left|⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\right|\right)=\left(0..^7\right)\to \left(E:\left(0..^\left|⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\right|\right)\underset{1-1\; onto}{⟶}\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\leftrightarrow E:\left(0..^7\right)\underset{1-1\; onto}{⟶}\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\right)$$
183	181 182	ax-mp	$$⊢E:\left(0..^\left|⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\right|\right)\underset{1-1\; onto}{⟶}\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\leftrightarrow E:\left(0..^7\right)\underset{1-1\; onto}{⟶}\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}$$
184	179 183	sylibr	$$⊢\left(\left(\left(\left(\left\{0,1\right\}\in \mathrm{V}\wedge \left\{1,2\right\}\in \mathrm{V}\wedge \left\{2,3\right\}\in \mathrm{V}\right)\wedge \left\{3,4\right\}\in \mathrm{V}\wedge \left(\left\{4,5\right\}\in \mathrm{V}\wedge \left\{0,3\right\}\in \mathrm{V}\wedge \left\{0,5\right\}\in \mathrm{V}\right)\right)\wedge \left(\left(\left(\left(\left\{0,1\right\}\ne \left\{1,2\right\}\wedge \left\{0,1\right\}\ne \left\{2,3\right\}\wedge \left\{0,1\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{0,1\right\}\ne \left\{4,5\right\}\wedge \left\{0,1\right\}\ne \left\{0,3\right\}\wedge \left\{0,1\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left(\left\{1,2\right\}\ne \left\{2,3\right\}\wedge \left\{1,2\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{1,2\right\}\ne \left\{4,5\right\}\wedge \left\{1,2\right\}\ne \left\{0,3\right\}\wedge \left\{1,2\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left\{2,3\right\}\ne \left\{3,4\right\}\wedge \left(\left\{2,3\right\}\ne \left\{4,5\right\}\wedge \left\{2,3\right\}\ne \left\{0,3\right\}\wedge \left\{2,3\right\}\ne \left\{0,5\right\}\right)\right)\right)\wedge \left(\left(\left\{3,4\right\}\ne \left\{4,5\right\}\wedge \left\{3,4\right\}\ne \left\{0,3\right\}\wedge \left\{3,4\right\}\ne \left\{0,5\right\}\right)\wedge \left(\left\{4,5\right\}\ne \left\{0,3\right\}\wedge \left\{4,5\right\}\ne \left\{0,5\right\}\wedge \left\{0,3\right\}\ne \left\{0,5\right\}\right)\right)\right)\right)\wedge E=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\right)\to E:\left(0..^\left|⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\right|\right)\underset{1-1\; onto}{⟶}\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}$$
185	2	dmeqi	$$⊢\mathrm{dom}E=\mathrm{dom}⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩$$
186		s7cli	$$⊢⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\in \mathrm{Word}\mathrm{V}$$
187		wrddm	$$⊢⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\in \mathrm{Word}\mathrm{V}\to \mathrm{dom}⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩=\left(0..^\left|⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\right|\right)$$
188	186 187	ax-mp	$$⊢\mathrm{dom}⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩=\left(0..^\left|⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\right|\right)$$
189	185 188	eqtri	$$⊢\mathrm{dom}E=\left(0..^\left|⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\right|\right)$$
190		f1oeq2	$$⊢\mathrm{dom}E=\left(0..^\left|⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\right|\right)\to \left(E:\mathrm{dom}E\underset{1-1\; onto}{⟶}\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\leftrightarrow E:\left(0..^\left|⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\right|\right)\underset{1-1\; onto}{⟶}\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\right)$$
191	189 190	ax-mp	$$⊢E:\mathrm{dom}E\underset{1-1\; onto}{⟶}\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\leftrightarrow E:\left(0..^\left|⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\right|\right)\underset{1-1\; onto}{⟶}\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}$$
192	184 191	sylibr	$$⊢\left(\left(\left(\left(\left\{0,1\right\}\in \mathrm{V}\wedge \left\{1,2\right\}\in \mathrm{V}\wedge \left\{2,3\right\}\in \mathrm{V}\right)\wedge \left\{3,4\right\}\in \mathrm{V}\wedge \left(\left\{4,5\right\}\in \mathrm{V}\wedge \left\{0,3\right\}\in \mathrm{V}\wedge \left\{0,5\right\}\in \mathrm{V}\right)\right)\wedge \left(\left(\left(\left(\left\{0,1\right\}\ne \left\{1,2\right\}\wedge \left\{0,1\right\}\ne \left\{2,3\right\}\wedge \left\{0,1\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{0,1\right\}\ne \left\{4,5\right\}\wedge \left\{0,1\right\}\ne \left\{0,3\right\}\wedge \left\{0,1\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left(\left\{1,2\right\}\ne \left\{2,3\right\}\wedge \left\{1,2\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{1,2\right\}\ne \left\{4,5\right\}\wedge \left\{1,2\right\}\ne \left\{0,3\right\}\wedge \left\{1,2\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left\{2,3\right\}\ne \left\{3,4\right\}\wedge \left(\left\{2,3\right\}\ne \left\{4,5\right\}\wedge \left\{2,3\right\}\ne \left\{0,3\right\}\wedge \left\{2,3\right\}\ne \left\{0,5\right\}\right)\right)\right)\wedge \left(\left(\left\{3,4\right\}\ne \left\{4,5\right\}\wedge \left\{3,4\right\}\ne \left\{0,3\right\}\wedge \left\{3,4\right\}\ne \left\{0,5\right\}\right)\wedge \left(\left\{4,5\right\}\ne \left\{0,3\right\}\wedge \left\{4,5\right\}\ne \left\{0,5\right\}\wedge \left\{0,3\right\}\ne \left\{0,5\right\}\right)\right)\right)\right)\wedge E=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\right)\to E:\mathrm{dom}E\underset{1-1\; onto}{⟶}\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}$$
193		f1of1	$$⊢E:\mathrm{dom}E\underset{1-1\; onto}{⟶}\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\to E:\mathrm{dom}E\underset{1-1}{⟶}\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}$$
194	192 193	syl	$$⊢\left(\left(\left(\left(\left\{0,1\right\}\in \mathrm{V}\wedge \left\{1,2\right\}\in \mathrm{V}\wedge \left\{2,3\right\}\in \mathrm{V}\right)\wedge \left\{3,4\right\}\in \mathrm{V}\wedge \left(\left\{4,5\right\}\in \mathrm{V}\wedge \left\{0,3\right\}\in \mathrm{V}\wedge \left\{0,5\right\}\in \mathrm{V}\right)\right)\wedge \left(\left(\left(\left(\left\{0,1\right\}\ne \left\{1,2\right\}\wedge \left\{0,1\right\}\ne \left\{2,3\right\}\wedge \left\{0,1\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{0,1\right\}\ne \left\{4,5\right\}\wedge \left\{0,1\right\}\ne \left\{0,3\right\}\wedge \left\{0,1\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left(\left\{1,2\right\}\ne \left\{2,3\right\}\wedge \left\{1,2\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{1,2\right\}\ne \left\{4,5\right\}\wedge \left\{1,2\right\}\ne \left\{0,3\right\}\wedge \left\{1,2\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left\{2,3\right\}\ne \left\{3,4\right\}\wedge \left(\left\{2,3\right\}\ne \left\{4,5\right\}\wedge \left\{2,3\right\}\ne \left\{0,3\right\}\wedge \left\{2,3\right\}\ne \left\{0,5\right\}\right)\right)\right)\wedge \left(\left(\left\{3,4\right\}\ne \left\{4,5\right\}\wedge \left\{3,4\right\}\ne \left\{0,3\right\}\wedge \left\{3,4\right\}\ne \left\{0,5\right\}\right)\wedge \left(\left\{4,5\right\}\ne \left\{0,3\right\}\wedge \left\{4,5\right\}\ne \left\{0,5\right\}\wedge \left\{0,3\right\}\ne \left\{0,5\right\}\right)\right)\right)\right)\wedge E=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\right)\to E:\mathrm{dom}E\underset{1-1}{⟶}\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}$$
195		0elfz	$$⊢5\in {\mathbb{N}}_0\to 0\in \left(0\dots 5\right)$$
196	45 195	ax-mp	$$⊢0\in \left(0\dots 5\right)$$
197		5re	$$⊢5\in ℝ$$
198	57 197 66	ltleii	$$⊢1\le 5$$
199		elfz2nn0	$$⊢1\in \left(0\dots 5\right)\leftrightarrow \left(1\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\wedge 1\le 5\right)$$
200	14 45 198 199	mpbir3an	$$⊢1\in \left(0\dots 5\right)$$
201		prssi	$$⊢\left(0\in \left(0\dots 5\right)\wedge 1\in \left(0\dots 5\right)\right)\to \left\{0,1\right\}\subseteq \left(0\dots 5\right)$$
202	196 200 201	mp2an	$$⊢\left\{0,1\right\}\subseteq \left(0\dots 5\right)$$
203	104 197 114	ltleii	$$⊢2\le 5$$
204		elfz2nn0	$$⊢2\in \left(0\dots 5\right)\leftrightarrow \left(2\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\wedge 2\le 5\right)$$
205	16 45 203 204	mpbir3an	$$⊢2\in \left(0\dots 5\right)$$
206		prssi	$$⊢\left(1\in \left(0\dots 5\right)\wedge 2\in \left(0\dots 5\right)\right)\to \left\{1,2\right\}\subseteq \left(0\dots 5\right)$$
207	200 205 206	mp2an	$$⊢\left\{1,2\right\}\subseteq \left(0\dots 5\right)$$
208	135 197 138	ltleii	$$⊢3\le 5$$
209		elfz2nn0	$$⊢3\in \left(0\dots 5\right)\leftrightarrow \left(3\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\wedge 3\le 5\right)$$
210	25 45 208 209	mpbir3an	$$⊢3\in \left(0\dots 5\right)$$
211		prssi	$$⊢\left(2\in \left(0\dots 5\right)\wedge 3\in \left(0\dots 5\right)\right)\to \left\{2,3\right\}\subseteq \left(0\dots 5\right)$$
212	205 210 211	mp2an	$$⊢\left\{2,3\right\}\subseteq \left(0\dots 5\right)$$
213		sseq1	$$⊢e=\left\{0,1\right\}\to \left(e\subseteq \left(0\dots 5\right)\leftrightarrow \left\{0,1\right\}\subseteq \left(0\dots 5\right)\right)$$
214		sseq1	$$⊢e=\left\{1,2\right\}\to \left(e\subseteq \left(0\dots 5\right)\leftrightarrow \left\{1,2\right\}\subseteq \left(0\dots 5\right)\right)$$
215		sseq1	$$⊢e=\left\{2,3\right\}\to \left(e\subseteq \left(0\dots 5\right)\leftrightarrow \left\{2,3\right\}\subseteq \left(0\dots 5\right)\right)$$
216	3 4 5 213 214 215	raltp	$$⊢\forall e\in \left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}e\subseteq \left(0\dots 5\right)\leftrightarrow \left(\left\{0,1\right\}\subseteq \left(0\dots 5\right)\wedge \left\{1,2\right\}\subseteq \left(0\dots 5\right)\wedge \left\{2,3\right\}\subseteq \left(0\dots 5\right)\right)$$
217	202 207 212 216	mpbir3an	$$⊢\forall e\in \left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}e\subseteq \left(0\dots 5\right)$$
218	163 197 164	ltleii	$$⊢4\le 5$$
219		elfz2nn0	$$⊢4\in \left(0\dots 5\right)\leftrightarrow \left(4\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\wedge 4\le 5\right)$$
220	35 45 218 219	mpbir3an	$$⊢4\in \left(0\dots 5\right)$$
221		prssi	$$⊢\left(3\in \left(0\dots 5\right)\wedge 4\in \left(0\dots 5\right)\right)\to \left\{3,4\right\}\subseteq \left(0\dots 5\right)$$
222	210 220 221	mp2an	$$⊢\left\{3,4\right\}\subseteq \left(0\dots 5\right)$$
223		sseq1	$$⊢e=\left\{3,4\right\}\to \left(e\subseteq \left(0\dots 5\right)\leftrightarrow \left\{3,4\right\}\subseteq \left(0\dots 5\right)\right)$$
224	7 223	ralsn	$$⊢\forall e\in \left\{\left\{3,4\right\}\right\}e\subseteq \left(0\dots 5\right)\leftrightarrow \left\{3,4\right\}\subseteq \left(0\dots 5\right)$$
225	222 224	mpbir	$$⊢\forall e\in \left\{\left\{3,4\right\}\right\}e\subseteq \left(0\dots 5\right)$$
226		ralunb	$$⊢\forall e\in \left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)e\subseteq \left(0\dots 5\right)\leftrightarrow \left(\forall e\in \left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}e\subseteq \left(0\dots 5\right)\wedge \forall e\in \left\{\left\{3,4\right\}\right\}e\subseteq \left(0\dots 5\right)\right)$$
227	217 225 226	mpbir2an	$$⊢\forall e\in \left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)e\subseteq \left(0\dots 5\right)$$
228	197	leidi	$$⊢5\le 5$$
229		elfz2nn0	$$⊢5\in \left(0\dots 5\right)\leftrightarrow \left(5\in {\mathbb{N}}_0\wedge 5\in {\mathbb{N}}_0\wedge 5\le 5\right)$$
230	45 45 228 229	mpbir3an	$$⊢5\in \left(0\dots 5\right)$$
231		prssi	$$⊢\left(4\in \left(0\dots 5\right)\wedge 5\in \left(0\dots 5\right)\right)\to \left\{4,5\right\}\subseteq \left(0\dots 5\right)$$
232	220 230 231	mp2an	$$⊢\left\{4,5\right\}\subseteq \left(0\dots 5\right)$$
233		prssi	$$⊢\left(0\in \left(0\dots 5\right)\wedge 3\in \left(0\dots 5\right)\right)\to \left\{0,3\right\}\subseteq \left(0\dots 5\right)$$
234	196 210 233	mp2an	$$⊢\left\{0,3\right\}\subseteq \left(0\dots 5\right)$$
235		prssi	$$⊢\left(0\in \left(0\dots 5\right)\wedge 5\in \left(0\dots 5\right)\right)\to \left\{0,5\right\}\subseteq \left(0\dots 5\right)$$
236	196 230 235	mp2an	$$⊢\left\{0,5\right\}\subseteq \left(0\dots 5\right)$$
237		sseq1	$$⊢e=\left\{4,5\right\}\to \left(e\subseteq \left(0\dots 5\right)\leftrightarrow \left\{4,5\right\}\subseteq \left(0\dots 5\right)\right)$$
238		sseq1	$$⊢e=\left\{0,3\right\}\to \left(e\subseteq \left(0\dots 5\right)\leftrightarrow \left\{0,3\right\}\subseteq \left(0\dots 5\right)\right)$$
239		sseq1	$$⊢e=\left\{0,5\right\}\to \left(e\subseteq \left(0\dots 5\right)\leftrightarrow \left\{0,5\right\}\subseteq \left(0\dots 5\right)\right)$$
240	8 9 10 237 238 239	raltp	$$⊢\forall e\in \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}e\subseteq \left(0\dots 5\right)\leftrightarrow \left(\left\{4,5\right\}\subseteq \left(0\dots 5\right)\wedge \left\{0,3\right\}\subseteq \left(0\dots 5\right)\wedge \left\{0,5\right\}\subseteq \left(0\dots 5\right)\right)$$
241	232 234 236 240	mpbir3an	$$⊢\forall e\in \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}e\subseteq \left(0\dots 5\right)$$
242		ralunb	$$⊢\forall e\in \left(\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\right)e\subseteq \left(0\dots 5\right)\leftrightarrow \left(\forall e\in \left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)e\subseteq \left(0\dots 5\right)\wedge \forall e\in \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}e\subseteq \left(0\dots 5\right)\right)$$
243	227 241 242	mpbir2an	$$⊢\forall e\in \left(\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\right)e\subseteq \left(0\dots 5\right)$$
244		pwssb	$$⊢\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\subseteq 𝒫\left(0\dots 5\right)\leftrightarrow \forall e\in \left(\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\right)e\subseteq \left(0\dots 5\right)$$
245	243 244	mpbir	$$⊢\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\subseteq 𝒫\left(0\dots 5\right)$$
246	1	pweqi	$$⊢𝒫V=𝒫\left(0\dots 5\right)$$
247	245 246	sseqtrri	$$⊢\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\subseteq 𝒫V$$
248		prhash2ex	$$⊢\left|\left\{0,1\right\}\right|=2$$
249		1ex	$$⊢1\in \mathrm{V}$$
250		2ex	$$⊢2\in \mathrm{V}$$
251	249 250 75	3pm3.2i	$$⊢\left(1\in \mathrm{V}\wedge 2\in \mathrm{V}\wedge 1\ne 2\right)$$
252		hashprb	$$⊢\left(1\in \mathrm{V}\wedge 2\in \mathrm{V}\wedge 1\ne 2\right)\leftrightarrow \left|\left\{1,2\right\}\right|=2$$
253	251 252	mpbi	$$⊢\left|\left\{1,2\right\}\right|=2$$
254		3ex	$$⊢3\in \mathrm{V}$$
255	250 254 106	3pm3.2i	$$⊢\left(2\in \mathrm{V}\wedge 3\in \mathrm{V}\wedge 2\ne 3\right)$$
256		hashprb	$$⊢\left(2\in \mathrm{V}\wedge 3\in \mathrm{V}\wedge 2\ne 3\right)\leftrightarrow \left|\left\{2,3\right\}\right|=2$$
257	255 256	mpbi	$$⊢\left|\left\{2,3\right\}\right|=2$$
258		fveqeq2	$$⊢e=\left\{0,1\right\}\to \left(\left|e\right|=2\leftrightarrow \left|\left\{0,1\right\}\right|=2\right)$$
259		fveqeq2	$$⊢e=\left\{1,2\right\}\to \left(\left|e\right|=2\leftrightarrow \left|\left\{1,2\right\}\right|=2\right)$$
260		fveqeq2	$$⊢e=\left\{2,3\right\}\to \left(\left|e\right|=2\leftrightarrow \left|\left\{2,3\right\}\right|=2\right)$$
261	3 4 5 258 259 260	raltp	$$⊢\forall e\in \left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\left|e\right|=2\leftrightarrow \left(\left|\left\{0,1\right\}\right|=2\wedge \left|\left\{1,2\right\}\right|=2\wedge \left|\left\{2,3\right\}\right|=2\right)$$
262	248 253 257 261	mpbir3an	$$⊢\forall e\in \left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\left|e\right|=2$$
263	35	elexi	$$⊢4\in \mathrm{V}$$
264	254 263 137	3pm3.2i	$$⊢\left(3\in \mathrm{V}\wedge 4\in \mathrm{V}\wedge 3\ne 4\right)$$
265		hashprb	$$⊢\left(3\in \mathrm{V}\wedge 4\in \mathrm{V}\wedge 3\ne 4\right)\leftrightarrow \left|\left\{3,4\right\}\right|=2$$
266	264 265	mpbi	$$⊢\left|\left\{3,4\right\}\right|=2$$
267		fveqeq2	$$⊢e=\left\{3,4\right\}\to \left(\left|e\right|=2\leftrightarrow \left|\left\{3,4\right\}\right|=2\right)$$
268	7 267	ralsn	$$⊢\forall e\in \left\{\left\{3,4\right\}\right\}\left|e\right|=2\leftrightarrow \left|\left\{3,4\right\}\right|=2$$
269	266 268	mpbir	$$⊢\forall e\in \left\{\left\{3,4\right\}\right\}\left|e\right|=2$$
270		ralunb	$$⊢\forall e\in \left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\left|e\right|=2\leftrightarrow \left(\forall e\in \left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\left|e\right|=2\wedge \forall e\in \left\{\left\{3,4\right\}\right\}\left|e\right|=2\right)$$
271	262 269 270	mpbir2an	$$⊢\forall e\in \left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\left|e\right|=2$$
272	45	elexi	$$⊢5\in \mathrm{V}$$
273	263 272 165	3pm3.2i	$$⊢\left(4\in \mathrm{V}\wedge 5\in \mathrm{V}\wedge 4\ne 5\right)$$
274		hashprb	$$⊢\left(4\in \mathrm{V}\wedge 5\in \mathrm{V}\wedge 4\ne 5\right)\leftrightarrow \left|\left\{4,5\right\}\right|=2$$
275	273 274	mpbi	$$⊢\left|\left\{4,5\right\}\right|=2$$
276		c0ex	$$⊢0\in \mathrm{V}$$
277	276 254 30	3pm3.2i	$$⊢\left(0\in \mathrm{V}\wedge 3\in \mathrm{V}\wedge 0\ne 3\right)$$
278		hashprb	$$⊢\left(0\in \mathrm{V}\wedge 3\in \mathrm{V}\wedge 0\ne 3\right)\leftrightarrow \left|\left\{0,3\right\}\right|=2$$
279	277 278	mpbi	$$⊢\left|\left\{0,3\right\}\right|=2$$
280	276 272 49	3pm3.2i	$$⊢\left(0\in \mathrm{V}\wedge 5\in \mathrm{V}\wedge 0\ne 5\right)$$
281		hashprb	$$⊢\left(0\in \mathrm{V}\wedge 5\in \mathrm{V}\wedge 0\ne 5\right)\leftrightarrow \left|\left\{0,5\right\}\right|=2$$
282	280 281	mpbi	$$⊢\left|\left\{0,5\right\}\right|=2$$
283		fveqeq2	$$⊢e=\left\{4,5\right\}\to \left(\left|e\right|=2\leftrightarrow \left|\left\{4,5\right\}\right|=2\right)$$
284		fveqeq2	$$⊢e=\left\{0,3\right\}\to \left(\left|e\right|=2\leftrightarrow \left|\left\{0,3\right\}\right|=2\right)$$
285		fveqeq2	$$⊢e=\left\{0,5\right\}\to \left(\left|e\right|=2\leftrightarrow \left|\left\{0,5\right\}\right|=2\right)$$
286	8 9 10 283 284 285	raltp	$$⊢\forall e\in \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\left|e\right|=2\leftrightarrow \left(\left|\left\{4,5\right\}\right|=2\wedge \left|\left\{0,3\right\}\right|=2\wedge \left|\left\{0,5\right\}\right|=2\right)$$
287	275 279 282 286	mpbir3an	$$⊢\forall e\in \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\left|e\right|=2$$
288		ralunb	$$⊢\forall e\in \left(\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\right)\left|e\right|=2\leftrightarrow \left(\forall e\in \left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\left|e\right|=2\wedge \forall e\in \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\left|e\right|=2\right)$$
289	271 287 288	mpbir2an	$$⊢\forall e\in \left(\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\right)\left|e\right|=2$$
290		ssrab	$$⊢\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\subseteq \left\{e\in 𝒫V|\left|e\right|=2\right\}\leftrightarrow \left(\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\subseteq 𝒫V\wedge \forall e\in \left(\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\right)\left|e\right|=2\right)$$
291	247 289 290	mpbir2an	$$⊢\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\subseteq \left\{e\in 𝒫V|\left|e\right|=2\right\}$$
292		f1ss	$$⊢\left(E:\mathrm{dom}E\underset{1-1}{⟶}\left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\wedge \left(\left\{\left\{0,1\right\},\left\{1,2\right\},\left\{2,3\right\}\right\}\cup \left\{\left\{3,4\right\}\right\}\right)\cup \left\{\left\{4,5\right\},\left\{0,3\right\},\left\{0,5\right\}\right\}\subseteq \left\{e\in 𝒫V|\left|e\right|=2\right\}\right)\to E:\mathrm{dom}E\underset{1-1}{⟶}\left\{e\in 𝒫V|\left|e\right|=2\right\}$$
293	194 291 292	sylancl	$$⊢\left(\left(\left(\left(\left\{0,1\right\}\in \mathrm{V}\wedge \left\{1,2\right\}\in \mathrm{V}\wedge \left\{2,3\right\}\in \mathrm{V}\right)\wedge \left\{3,4\right\}\in \mathrm{V}\wedge \left(\left\{4,5\right\}\in \mathrm{V}\wedge \left\{0,3\right\}\in \mathrm{V}\wedge \left\{0,5\right\}\in \mathrm{V}\right)\right)\wedge \left(\left(\left(\left(\left\{0,1\right\}\ne \left\{1,2\right\}\wedge \left\{0,1\right\}\ne \left\{2,3\right\}\wedge \left\{0,1\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{0,1\right\}\ne \left\{4,5\right\}\wedge \left\{0,1\right\}\ne \left\{0,3\right\}\wedge \left\{0,1\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left(\left\{1,2\right\}\ne \left\{2,3\right\}\wedge \left\{1,2\right\}\ne \left\{3,4\right\}\right)\wedge \left(\left\{1,2\right\}\ne \left\{4,5\right\}\wedge \left\{1,2\right\}\ne \left\{0,3\right\}\wedge \left\{1,2\right\}\ne \left\{0,5\right\}\right)\right)\wedge \left(\left\{2,3\right\}\ne \left\{3,4\right\}\wedge \left(\left\{2,3\right\}\ne \left\{4,5\right\}\wedge \left\{2,3\right\}\ne \left\{0,3\right\}\wedge \left\{2,3\right\}\ne \left\{0,5\right\}\right)\right)\right)\wedge \left(\left(\left\{3,4\right\}\ne \left\{4,5\right\}\wedge \left\{3,4\right\}\ne \left\{0,3\right\}\wedge \left\{3,4\right\}\ne \left\{0,5\right\}\right)\wedge \left(\left\{4,5\right\}\ne \left\{0,3\right\}\wedge \left\{4,5\right\}\ne \left\{0,5\right\}\wedge \left\{0,3\right\}\ne \left\{0,5\right\}\right)\right)\right)\right)\wedge E=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩\right)\to E:\mathrm{dom}E\underset{1-1}{⟶}\left\{e\in 𝒫V|\left|e\right|=2\right\}$$
294	177 2 293	mp2an	$$⊢E:\mathrm{dom}E\underset{1-1}{⟶}\left\{e\in 𝒫V|\left|e\right|=2\right\}$$