Theorem usgrexmpl1lem

Description: Lemma for usgrexmpl1 . (Contributed by AV, 2-Aug-2025)

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

Proof

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