usgrexmpl2lem - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > usgrexmpl2lem		Structured version Visualization version GIF version

Theorem usgrexmpl2lem 47934

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

**Hypotheses**
Ref	Expression
usgrexmpl2.v	⊢ 𝑉 = (0...5)
usgrexmpl2.e	⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩

**Assertion**
Ref	Expression
usgrexmpl2lem	⊢ 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}

Distinct variable group: 𝑒,𝑉 Allowed substitution hint: 𝐸(𝑒)

**Proof of Theorem usgrexmpl2lem**
Step	Hyp	Ref	Expression
1		prex 5444	. . . . 5 ⊢ {0, 1} ∈ V
2		prex 5444	. . . . 5 ⊢ {1, 2} ∈ V
3		prex 5444	. . . . 5 ⊢ {2, 3} ∈ V
4	1, 2, 3	3pm3.2i 1339	. . . 4 ⊢ ({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V)
5		prex 5444	. . . 4 ⊢ {3, 4} ∈ V
6		prex 5444	. . . . 5 ⊢ {4, 5} ∈ V
7		prex 5444	. . . . 5 ⊢ {0, 3} ∈ V
8		prex 5444	. . . . 5 ⊢ {0, 5} ∈ V
9	6, 7, 8	3pm3.2i 1339	. . . 4 ⊢ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V)
10	4, 5, 9	3pm3.2i 1339	. . 3 ⊢ (({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V) ∧ {3, 4} ∈ V ∧ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V))
11		0nn0 12545	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
12		1nn0 12546	. . . . . . . . . 10 ⊢ 1 ∈ ℕ₀
13	11, 12	pm3.2i 470	. . . . . . . . 9 ⊢ (0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀)
14		2nn0 12547	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
15	12, 14	pm3.2i 470	. . . . . . . . 9 ⊢ (1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀)
16	13, 15	pm3.2i 470	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀))
17		0ne1 12341	. . . . . . . . . 10 ⊢ 0 ≠ 1
18		0ne2 12477	. . . . . . . . . 10 ⊢ 0 ≠ 2
19	17, 18	pm3.2i 470	. . . . . . . . 9 ⊢ (0 ≠ 1 ∧ 0 ≠ 2)
20	19	orci 865	. . . . . . . 8 ⊢ ((0 ≠ 1 ∧ 0 ≠ 2) ∨ (1 ≠ 1 ∧ 1 ≠ 2))
21		prneimg 4860	. . . . . . . 8 ⊢ (((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀)) → (((0 ≠ 1 ∧ 0 ≠ 2) ∨ (1 ≠ 1 ∧ 1 ≠ 2)) → {0, 1} ≠ {1, 2}))
22	16, 20, 21	mp2 9	. . . . . . 7 ⊢ {0, 1} ≠ {1, 2}
23		3nn0 12548	. . . . . . . . . 10 ⊢ 3 ∈ ℕ₀
24	14, 23	pm3.2i 470	. . . . . . . . 9 ⊢ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀)
25	13, 24	pm3.2i 470	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀))
26		0re 11267	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
27		3pos 12375	. . . . . . . . . . 11 ⊢ 0 < 3
28	26, 27	ltneii 11378	. . . . . . . . . 10 ⊢ 0 ≠ 3
29	18, 28	pm3.2i 470	. . . . . . . . 9 ⊢ (0 ≠ 2 ∧ 0 ≠ 3)
30	29	orci 865	. . . . . . . 8 ⊢ ((0 ≠ 2 ∧ 0 ≠ 3) ∨ (1 ≠ 2 ∧ 1 ≠ 3))
31		prneimg 4860	. . . . . . . 8 ⊢ (((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀)) → (((0 ≠ 2 ∧ 0 ≠ 3) ∨ (1 ≠ 2 ∧ 1 ≠ 3)) → {0, 1} ≠ {2, 3}))
32	25, 30, 31	mp2 9	. . . . . . 7 ⊢ {0, 1} ≠ {2, 3}
33		4nn0 12549	. . . . . . . . . 10 ⊢ 4 ∈ ℕ₀
34	23, 33	pm3.2i 470	. . . . . . . . 9 ⊢ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀)
35	13, 34	pm3.2i 470	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀))
36		4pos 12377	. . . . . . . . . . 11 ⊢ 0 < 4
37	26, 36	ltneii 11378	. . . . . . . . . 10 ⊢ 0 ≠ 4
38	28, 37	pm3.2i 470	. . . . . . . . 9 ⊢ (0 ≠ 3 ∧ 0 ≠ 4)
39	38	orci 865	. . . . . . . 8 ⊢ ((0 ≠ 3 ∧ 0 ≠ 4) ∨ (1 ≠ 3 ∧ 1 ≠ 4))
40		prneimg 4860	. . . . . . . 8 ⊢ (((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀)) → (((0 ≠ 3 ∧ 0 ≠ 4) ∨ (1 ≠ 3 ∧ 1 ≠ 4)) → {0, 1} ≠ {3, 4}))
41	35, 39, 40	mp2 9	. . . . . . 7 ⊢ {0, 1} ≠ {3, 4}
42	22, 32, 41	3pm3.2i 1339	. . . . . 6 ⊢ ({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4})
43		5nn0 12550	. . . . . . . . . 10 ⊢ 5 ∈ ℕ₀
44	33, 43	pm3.2i 470	. . . . . . . . 9 ⊢ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀)
45	13, 44	pm3.2i 470	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
46		5pos 12379	. . . . . . . . . . 11 ⊢ 0 < 5
47	26, 46	ltneii 11378	. . . . . . . . . 10 ⊢ 0 ≠ 5
48	37, 47	pm3.2i 470	. . . . . . . . 9 ⊢ (0 ≠ 4 ∧ 0 ≠ 5)
49	48	orci 865	. . . . . . . 8 ⊢ ((0 ≠ 4 ∧ 0 ≠ 5) ∨ (1 ≠ 4 ∧ 1 ≠ 5))
50		prneimg 4860	. . . . . . . 8 ⊢ (((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀)) → (((0 ≠ 4 ∧ 0 ≠ 5) ∨ (1 ≠ 4 ∧ 1 ≠ 5)) → {0, 1} ≠ {4, 5}))
51	45, 49, 50	mp2 9	. . . . . . 7 ⊢ {0, 1} ≠ {4, 5}
52	11, 23	pm3.2i 470	. . . . . . . . 9 ⊢ (0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀)
53	13, 52	pm3.2i 470	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀))
54		ax-1ne0 11228	. . . . . . . . . 10 ⊢ 1 ≠ 0
55		1re 11265	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
56		1lt3 12443	. . . . . . . . . . 11 ⊢ 1 < 3
57	55, 56	ltneii 11378	. . . . . . . . . 10 ⊢ 1 ≠ 3
58	54, 57	pm3.2i 470	. . . . . . . . 9 ⊢ (1 ≠ 0 ∧ 1 ≠ 3)
59	58	olci 866	. . . . . . . 8 ⊢ ((0 ≠ 0 ∧ 0 ≠ 3) ∨ (1 ≠ 0 ∧ 1 ≠ 3))
60		prneimg 4860	. . . . . . . 8 ⊢ (((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀)) → (((0 ≠ 0 ∧ 0 ≠ 3) ∨ (1 ≠ 0 ∧ 1 ≠ 3)) → {0, 1} ≠ {0, 3}))
61	53, 59, 60	mp2 9	. . . . . . 7 ⊢ {0, 1} ≠ {0, 3}
62	11, 43	pm3.2i 470	. . . . . . . . 9 ⊢ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀)
63	13, 62	pm3.2i 470	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
64		1lt5 12450	. . . . . . . . . . 11 ⊢ 1 < 5
65	55, 64	ltneii 11378	. . . . . . . . . 10 ⊢ 1 ≠ 5
66	54, 65	pm3.2i 470	. . . . . . . . 9 ⊢ (1 ≠ 0 ∧ 1 ≠ 5)
67	66	olci 866	. . . . . . . 8 ⊢ ((0 ≠ 0 ∧ 0 ≠ 5) ∨ (1 ≠ 0 ∧ 1 ≠ 5))
68		prneimg 4860	. . . . . . . 8 ⊢ (((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀)) → (((0 ≠ 0 ∧ 0 ≠ 5) ∨ (1 ≠ 0 ∧ 1 ≠ 5)) → {0, 1} ≠ {0, 5}))
69	63, 67, 68	mp2 9	. . . . . . 7 ⊢ {0, 1} ≠ {0, 5}
70	51, 61, 69	3pm3.2i 1339	. . . . . 6 ⊢ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})
71	42, 70	pm3.2i 470	. . . . 5 ⊢ (({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5}))
72	15, 24	pm3.2i 470	. . . . . . . 8 ⊢ ((1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) ∧ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀))
73		1ne2 12478	. . . . . . . . . 10 ⊢ 1 ≠ 2
74	73, 57	pm3.2i 470	. . . . . . . . 9 ⊢ (1 ≠ 2 ∧ 1 ≠ 3)
75	74	orci 865	. . . . . . . 8 ⊢ ((1 ≠ 2 ∧ 1 ≠ 3) ∨ (2 ≠ 2 ∧ 2 ≠ 3))
76		prneimg 4860	. . . . . . . 8 ⊢ (((1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) ∧ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀)) → (((1 ≠ 2 ∧ 1 ≠ 3) ∨ (2 ≠ 2 ∧ 2 ≠ 3)) → {1, 2} ≠ {2, 3}))
77	72, 75, 76	mp2 9	. . . . . . 7 ⊢ {1, 2} ≠ {2, 3}
78	15, 34	pm3.2i 470	. . . . . . . 8 ⊢ ((1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) ∧ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀))
79		1lt4 12446	. . . . . . . . . . 11 ⊢ 1 < 4
80	55, 79	ltneii 11378	. . . . . . . . . 10 ⊢ 1 ≠ 4
81	57, 80	pm3.2i 470	. . . . . . . . 9 ⊢ (1 ≠ 3 ∧ 1 ≠ 4)
82	81	orci 865	. . . . . . . 8 ⊢ ((1 ≠ 3 ∧ 1 ≠ 4) ∨ (2 ≠ 3 ∧ 2 ≠ 4))
83		prneimg 4860	. . . . . . . 8 ⊢ (((1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) ∧ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀)) → (((1 ≠ 3 ∧ 1 ≠ 4) ∨ (2 ≠ 3 ∧ 2 ≠ 4)) → {1, 2} ≠ {3, 4}))
84	78, 82, 83	mp2 9	. . . . . . 7 ⊢ {1, 2} ≠ {3, 4}
85	77, 84	pm3.2i 470	. . . . . 6 ⊢ ({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4})
86	15, 44	pm3.2i 470	. . . . . . . 8 ⊢ ((1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) ∧ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
87	80, 65	pm3.2i 470	. . . . . . . . 9 ⊢ (1 ≠ 4 ∧ 1 ≠ 5)
88	87	orci 865	. . . . . . . 8 ⊢ ((1 ≠ 4 ∧ 1 ≠ 5) ∨ (2 ≠ 4 ∧ 2 ≠ 5))
89		prneimg 4860	. . . . . . . 8 ⊢ (((1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) ∧ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀)) → (((1 ≠ 4 ∧ 1 ≠ 5) ∨ (2 ≠ 4 ∧ 2 ≠ 5)) → {1, 2} ≠ {4, 5}))
90	86, 88, 89	mp2 9	. . . . . . 7 ⊢ {1, 2} ≠ {4, 5}
91	15, 52	pm3.2i 470	. . . . . . . 8 ⊢ ((1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀))
92	58	orci 865	. . . . . . . 8 ⊢ ((1 ≠ 0 ∧ 1 ≠ 3) ∨ (2 ≠ 0 ∧ 2 ≠ 3))
93		prneimg 4860	. . . . . . . 8 ⊢ (((1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀)) → (((1 ≠ 0 ∧ 1 ≠ 3) ∨ (2 ≠ 0 ∧ 2 ≠ 3)) → {1, 2} ≠ {0, 3}))
94	91, 92, 93	mp2 9	. . . . . . 7 ⊢ {1, 2} ≠ {0, 3}
95	15, 62	pm3.2i 470	. . . . . . . 8 ⊢ ((1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
96	66	orci 865	. . . . . . . 8 ⊢ ((1 ≠ 0 ∧ 1 ≠ 5) ∨ (2 ≠ 0 ∧ 2 ≠ 5))
97		prneimg 4860	. . . . . . . 8 ⊢ (((1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀)) → (((1 ≠ 0 ∧ 1 ≠ 5) ∨ (2 ≠ 0 ∧ 2 ≠ 5)) → {1, 2} ≠ {0, 5}))
98	95, 96, 97	mp2 9	. . . . . . 7 ⊢ {1, 2} ≠ {0, 5}
99	90, 94, 98	3pm3.2i 1339	. . . . . 6 ⊢ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})
100	85, 99	pm3.2i 470	. . . . 5 ⊢ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5}))
101	24, 34	pm3.2i 470	. . . . . . 7 ⊢ ((2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) ∧ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀))
102		2re 12344	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
103		2lt3 12442	. . . . . . . . . 10 ⊢ 2 < 3
104	102, 103	ltneii 11378	. . . . . . . . 9 ⊢ 2 ≠ 3
105		2lt4 12445	. . . . . . . . . 10 ⊢ 2 < 4
106	102, 105	ltneii 11378	. . . . . . . . 9 ⊢ 2 ≠ 4
107	104, 106	pm3.2i 470	. . . . . . . 8 ⊢ (2 ≠ 3 ∧ 2 ≠ 4)
108	107	orci 865	. . . . . . 7 ⊢ ((2 ≠ 3 ∧ 2 ≠ 4) ∨ (3 ≠ 3 ∧ 3 ≠ 4))
109		prneimg 4860	. . . . . . 7 ⊢ (((2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) ∧ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀)) → (((2 ≠ 3 ∧ 2 ≠ 4) ∨ (3 ≠ 3 ∧ 3 ≠ 4)) → {2, 3} ≠ {3, 4}))
110	101, 108, 109	mp2 9	. . . . . 6 ⊢ {2, 3} ≠ {3, 4}
111	24, 44	pm3.2i 470	. . . . . . . 8 ⊢ ((2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) ∧ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
112		2lt5 12449	. . . . . . . . . . 11 ⊢ 2 < 5
113	102, 112	ltneii 11378	. . . . . . . . . 10 ⊢ 2 ≠ 5
114	106, 113	pm3.2i 470	. . . . . . . . 9 ⊢ (2 ≠ 4 ∧ 2 ≠ 5)
115	114	orci 865	. . . . . . . 8 ⊢ ((2 ≠ 4 ∧ 2 ≠ 5) ∨ (3 ≠ 4 ∧ 3 ≠ 5))
116		prneimg 4860	. . . . . . . 8 ⊢ (((2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) ∧ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀)) → (((2 ≠ 4 ∧ 2 ≠ 5) ∨ (3 ≠ 4 ∧ 3 ≠ 5)) → {2, 3} ≠ {4, 5}))
117	111, 115, 116	mp2 9	. . . . . . 7 ⊢ {2, 3} ≠ {4, 5}
118	24, 52	pm3.2i 470	. . . . . . . 8 ⊢ ((2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀))
119		2ne0 12374	. . . . . . . . . 10 ⊢ 2 ≠ 0
120	119, 104	pm3.2i 470	. . . . . . . . 9 ⊢ (2 ≠ 0 ∧ 2 ≠ 3)
121	120	orci 865	. . . . . . . 8 ⊢ ((2 ≠ 0 ∧ 2 ≠ 3) ∨ (3 ≠ 0 ∧ 3 ≠ 3))
122		prneimg 4860	. . . . . . . 8 ⊢ (((2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀)) → (((2 ≠ 0 ∧ 2 ≠ 3) ∨ (3 ≠ 0 ∧ 3 ≠ 3)) → {2, 3} ≠ {0, 3}))
123	118, 121, 122	mp2 9	. . . . . . 7 ⊢ {2, 3} ≠ {0, 3}
124	24, 62	pm3.2i 470	. . . . . . . 8 ⊢ ((2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
125	119, 113	pm3.2i 470	. . . . . . . . 9 ⊢ (2 ≠ 0 ∧ 2 ≠ 5)
126	125	orci 865	. . . . . . . 8 ⊢ ((2 ≠ 0 ∧ 2 ≠ 5) ∨ (3 ≠ 0 ∧ 3 ≠ 5))
127		prneimg 4860	. . . . . . . 8 ⊢ (((2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀)) → (((2 ≠ 0 ∧ 2 ≠ 5) ∨ (3 ≠ 0 ∧ 3 ≠ 5)) → {2, 3} ≠ {0, 5}))
128	124, 126, 127	mp2 9	. . . . . . 7 ⊢ {2, 3} ≠ {0, 5}
129	117, 123, 128	3pm3.2i 1339	. . . . . 6 ⊢ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5})
130	110, 129	pm3.2i 470	. . . . 5 ⊢ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))
131	71, 100, 130	3pm3.2i 1339	. . . 4 ⊢ ((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5})))
132	34, 44	pm3.2i 470	. . . . . . 7 ⊢ ((3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀) ∧ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
133		3re 12350	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
134		3lt4 12444	. . . . . . . . . 10 ⊢ 3 < 4
135	133, 134	ltneii 11378	. . . . . . . . 9 ⊢ 3 ≠ 4
136		3lt5 12448	. . . . . . . . . 10 ⊢ 3 < 5
137	133, 136	ltneii 11378	. . . . . . . . 9 ⊢ 3 ≠ 5
138	135, 137	pm3.2i 470	. . . . . . . 8 ⊢ (3 ≠ 4 ∧ 3 ≠ 5)
139	138	orci 865	. . . . . . 7 ⊢ ((3 ≠ 4 ∧ 3 ≠ 5) ∨ (4 ≠ 4 ∧ 4 ≠ 5))
140		prneimg 4860	. . . . . . 7 ⊢ (((3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀) ∧ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀)) → (((3 ≠ 4 ∧ 3 ≠ 5) ∨ (4 ≠ 4 ∧ 4 ≠ 5)) → {3, 4} ≠ {4, 5}))
141	132, 139, 140	mp2 9	. . . . . 6 ⊢ {3, 4} ≠ {4, 5}
142	34, 52	pm3.2i 470	. . . . . . 7 ⊢ ((3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀))
143		4ne0 12378	. . . . . . . . 9 ⊢ 4 ≠ 0
144	135	necomi 2994	. . . . . . . . 9 ⊢ 4 ≠ 3
145	143, 144	pm3.2i 470	. . . . . . . 8 ⊢ (4 ≠ 0 ∧ 4 ≠ 3)
146	145	olci 866	. . . . . . 7 ⊢ ((3 ≠ 0 ∧ 3 ≠ 3) ∨ (4 ≠ 0 ∧ 4 ≠ 3))
147		prneimg 4860	. . . . . . 7 ⊢ (((3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀)) → (((3 ≠ 0 ∧ 3 ≠ 3) ∨ (4 ≠ 0 ∧ 4 ≠ 3)) → {3, 4} ≠ {0, 3}))
148	142, 146, 147	mp2 9	. . . . . 6 ⊢ {3, 4} ≠ {0, 3}
149	34, 62	pm3.2i 470	. . . . . . 7 ⊢ ((3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
150		3ne0 12376	. . . . . . . . 9 ⊢ 3 ≠ 0
151	150, 137	pm3.2i 470	. . . . . . . 8 ⊢ (3 ≠ 0 ∧ 3 ≠ 5)
152	151	orci 865	. . . . . . 7 ⊢ ((3 ≠ 0 ∧ 3 ≠ 5) ∨ (4 ≠ 0 ∧ 4 ≠ 5))
153		prneimg 4860	. . . . . . 7 ⊢ (((3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀)) → (((3 ≠ 0 ∧ 3 ≠ 5) ∨ (4 ≠ 0 ∧ 4 ≠ 5)) → {3, 4} ≠ {0, 5}))
154	149, 152, 153	mp2 9	. . . . . 6 ⊢ {3, 4} ≠ {0, 5}
155	141, 148, 154	3pm3.2i 1339	. . . . 5 ⊢ ({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5})
156	44, 52	pm3.2i 470	. . . . . . 7 ⊢ ((4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀))
157	145	orci 865	. . . . . . 7 ⊢ ((4 ≠ 0 ∧ 4 ≠ 3) ∨ (5 ≠ 0 ∧ 5 ≠ 3))
158		prneimg 4860	. . . . . . 7 ⊢ (((4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀)) → (((4 ≠ 0 ∧ 4 ≠ 3) ∨ (5 ≠ 0 ∧ 5 ≠ 3)) → {4, 5} ≠ {0, 3}))
159	156, 157, 158	mp2 9	. . . . . 6 ⊢ {4, 5} ≠ {0, 3}
160	44, 62	pm3.2i 470	. . . . . . 7 ⊢ ((4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
161		4re 12354	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
162		4lt5 12447	. . . . . . . . . 10 ⊢ 4 < 5
163	161, 162	ltneii 11378	. . . . . . . . 9 ⊢ 4 ≠ 5
164	143, 163	pm3.2i 470	. . . . . . . 8 ⊢ (4 ≠ 0 ∧ 4 ≠ 5)
165	164	orci 865	. . . . . . 7 ⊢ ((4 ≠ 0 ∧ 4 ≠ 5) ∨ (5 ≠ 0 ∧ 5 ≠ 5))
166		prneimg 4860	. . . . . . 7 ⊢ (((4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀)) → (((4 ≠ 0 ∧ 4 ≠ 5) ∨ (5 ≠ 0 ∧ 5 ≠ 5)) → {4, 5} ≠ {0, 5}))
167	160, 165, 166	mp2 9	. . . . . 6 ⊢ {4, 5} ≠ {0, 5}
168	52, 62	pm3.2i 470	. . . . . . 7 ⊢ ((0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
169	151	olci 866	. . . . . . 7 ⊢ ((0 ≠ 0 ∧ 0 ≠ 5) ∨ (3 ≠ 0 ∧ 3 ≠ 5))
170		prneimg 4860	. . . . . . 7 ⊢ (((0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀)) → (((0 ≠ 0 ∧ 0 ≠ 5) ∨ (3 ≠ 0 ∧ 3 ≠ 5)) → {0, 3} ≠ {0, 5}))
171	168, 169, 170	mp2 9	. . . . . 6 ⊢ {0, 3} ≠ {0, 5}
172	159, 167, 171	3pm3.2i 1339	. . . . 5 ⊢ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5})
173	155, 172	pm3.2i 470	. . . 4 ⊢ (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5}))
174	131, 173	pm3.2i 470	. . 3 ⊢ (((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))) ∧ (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5})))
175	10, 174	pm3.2i 470	. 2 ⊢ ((({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V) ∧ {3, 4} ∈ V ∧ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V)) ∧ (((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))) ∧ (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5}))))
176		usgrexmpl2.e	. 2 ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩
177		s7f1o 15008	. . . . . . 7 ⊢ (((({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V) ∧ {3, 4} ∈ V ∧ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V)) ∧ (((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))) ∧ (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5})))) → (𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩ → 𝐸:(0..^7)–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})))
178	177	imp 406	. . . . . 6 ⊢ ((((({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V) ∧ {3, 4} ∈ V ∧ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V)) ∧ (((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))) ∧ (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5})))) ∧ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩) → 𝐸:(0..^7)–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}))
179		s7len 14944	. . . . . . . 8 ⊢ (♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩) = 7
180	179	oveq2i 7446	. . . . . . 7 ⊢ (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩)) = (0..^7)
181		f1oeq2 6842	. . . . . . 7 ⊢ ((0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩)) = (0..^7) → (𝐸:(0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ↔ 𝐸:(0..^7)–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})))
182	180, 181	ax-mp 5	. . . . . 6 ⊢ (𝐸:(0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ↔ 𝐸:(0..^7)–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}))
183	178, 182	sylibr 234	. . . . 5 ⊢ ((((({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V) ∧ {3, 4} ∈ V ∧ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V)) ∧ (((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))) ∧ (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5})))) ∧ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩) → 𝐸:(0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}))
184	176	dmeqi 5919	. . . . . . 7 ⊢ dom 𝐸 = dom ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩
185		s7cli 14927	. . . . . . . 8 ⊢ ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩ ∈ Word V
186		wrddm 14562	. . . . . . . 8 ⊢ (⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩ ∈ Word V → dom ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩ = (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩)))
187	185, 186	ax-mp 5	. . . . . . 7 ⊢ dom ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩ = (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))
188	184, 187	eqtri 2764	. . . . . 6 ⊢ dom 𝐸 = (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))
189		f1oeq2 6842	. . . . . 6 ⊢ (dom 𝐸 = (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩)) → (𝐸:dom 𝐸–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ↔ 𝐸:(0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})))
190	188, 189	ax-mp 5	. . . . 5 ⊢ (𝐸:dom 𝐸–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ↔ 𝐸:(0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}))
191	183, 190	sylibr 234	. . . 4 ⊢ ((((({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V) ∧ {3, 4} ∈ V ∧ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V)) ∧ (((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))) ∧ (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5})))) ∧ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩) → 𝐸:dom 𝐸–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}))
192		f1of1 6852	. . . 4 ⊢ (𝐸:dom 𝐸–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) → 𝐸:dom 𝐸–1-1→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}))
193	191, 192	syl 17	. . 3 ⊢ ((((({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V) ∧ {3, 4} ∈ V ∧ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V)) ∧ (((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))) ∧ (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5})))) ∧ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩) → 𝐸:dom 𝐸–1-1→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}))
194		0elfz 13667	. . . . . . . . . . 11 ⊢ (5 ∈ ℕ₀ → 0 ∈ (0...5))
195	43, 194	ax-mp 5	. . . . . . . . . 10 ⊢ 0 ∈ (0...5)
196		5re 12357	. . . . . . . . . . . 12 ⊢ 5 ∈ ℝ
197	55, 196, 64	ltleii 11388	. . . . . . . . . . 11 ⊢ 1 ≤ 5
198		elfz2nn0 13661	. . . . . . . . . . 11 ⊢ (1 ∈ (0...5) ↔ (1 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 1 ≤ 5))
199	12, 43, 197, 198	mpbir3an 1341	. . . . . . . . . 10 ⊢ 1 ∈ (0...5)
200		prssi 4827	. . . . . . . . . 10 ⊢ ((0 ∈ (0...5) ∧ 1 ∈ (0...5)) → {0, 1} ⊆ (0...5))
201	195, 199, 200	mp2an 692	. . . . . . . . 9 ⊢ {0, 1} ⊆ (0...5)
202	102, 196, 112	ltleii 11388	. . . . . . . . . . 11 ⊢ 2 ≤ 5
203		elfz2nn0 13661	. . . . . . . . . . 11 ⊢ (2 ∈ (0...5) ↔ (2 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 2 ≤ 5))
204	14, 43, 202, 203	mpbir3an 1341	. . . . . . . . . 10 ⊢ 2 ∈ (0...5)
205		prssi 4827	. . . . . . . . . 10 ⊢ ((1 ∈ (0...5) ∧ 2 ∈ (0...5)) → {1, 2} ⊆ (0...5))
206	199, 204, 205	mp2an 692	. . . . . . . . 9 ⊢ {1, 2} ⊆ (0...5)
207	133, 196, 136	ltleii 11388	. . . . . . . . . . 11 ⊢ 3 ≤ 5
208		elfz2nn0 13661	. . . . . . . . . . 11 ⊢ (3 ∈ (0...5) ↔ (3 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 3 ≤ 5))
209	23, 43, 207, 208	mpbir3an 1341	. . . . . . . . . 10 ⊢ 3 ∈ (0...5)
210		prssi 4827	. . . . . . . . . 10 ⊢ ((2 ∈ (0...5) ∧ 3 ∈ (0...5)) → {2, 3} ⊆ (0...5))
211	204, 209, 210	mp2an 692	. . . . . . . . 9 ⊢ {2, 3} ⊆ (0...5)
212		sseq1 4022	. . . . . . . . . 10 ⊢ (𝑒 = {0, 1} → (𝑒 ⊆ (0...5) ↔ {0, 1} ⊆ (0...5)))
213		sseq1 4022	. . . . . . . . . 10 ⊢ (𝑒 = {1, 2} → (𝑒 ⊆ (0...5) ↔ {1, 2} ⊆ (0...5)))
214		sseq1 4022	. . . . . . . . . 10 ⊢ (𝑒 = {2, 3} → (𝑒 ⊆ (0...5) ↔ {2, 3} ⊆ (0...5)))
215	1, 2, 3, 212, 213, 214	raltp 4711	. . . . . . . . 9 ⊢ (∀𝑒 ∈ {{0, 1}, {1, 2}, {2, 3}}𝑒 ⊆ (0...5) ↔ ({0, 1} ⊆ (0...5) ∧ {1, 2} ⊆ (0...5) ∧ {2, 3} ⊆ (0...5)))
216	201, 206, 211, 215	mpbir3an 1341	. . . . . . . 8 ⊢ ∀𝑒 ∈ {{0, 1}, {1, 2}, {2, 3}}𝑒 ⊆ (0...5)
217	161, 196, 162	ltleii 11388	. . . . . . . . . . 11 ⊢ 4 ≤ 5
218		elfz2nn0 13661	. . . . . . . . . . 11 ⊢ (4 ∈ (0...5) ↔ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 4 ≤ 5))
219	33, 43, 217, 218	mpbir3an 1341	. . . . . . . . . 10 ⊢ 4 ∈ (0...5)
220		prssi 4827	. . . . . . . . . 10 ⊢ ((3 ∈ (0...5) ∧ 4 ∈ (0...5)) → {3, 4} ⊆ (0...5))
221	209, 219, 220	mp2an 692	. . . . . . . . 9 ⊢ {3, 4} ⊆ (0...5)
222		sseq1 4022	. . . . . . . . . 10 ⊢ (𝑒 = {3, 4} → (𝑒 ⊆ (0...5) ↔ {3, 4} ⊆ (0...5)))
223	5, 222	ralsn 4687	. . . . . . . . 9 ⊢ (∀𝑒 ∈ {{3, 4}}𝑒 ⊆ (0...5) ↔ {3, 4} ⊆ (0...5))
224	221, 223	mpbir 231	. . . . . . . 8 ⊢ ∀𝑒 ∈ {{3, 4}}𝑒 ⊆ (0...5)
225		ralunb 4208	. . . . . . . 8 ⊢ (∀𝑒 ∈ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}})𝑒 ⊆ (0...5) ↔ (∀𝑒 ∈ {{0, 1}, {1, 2}, {2, 3}}𝑒 ⊆ (0...5) ∧ ∀𝑒 ∈ {{3, 4}}𝑒 ⊆ (0...5)))
226	216, 224, 225	mpbir2an 711	. . . . . . 7 ⊢ ∀𝑒 ∈ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}})𝑒 ⊆ (0...5)
227	196	leidi 11801	. . . . . . . . . 10 ⊢ 5 ≤ 5
228		elfz2nn0 13661	. . . . . . . . . 10 ⊢ (5 ∈ (0...5) ↔ (5 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 5 ≤ 5))
229	43, 43, 227, 228	mpbir3an 1341	. . . . . . . . 9 ⊢ 5 ∈ (0...5)
230		prssi 4827	. . . . . . . . 9 ⊢ ((4 ∈ (0...5) ∧ 5 ∈ (0...5)) → {4, 5} ⊆ (0...5))
231	219, 229, 230	mp2an 692	. . . . . . . 8 ⊢ {4, 5} ⊆ (0...5)
232		prssi 4827	. . . . . . . . 9 ⊢ ((0 ∈ (0...5) ∧ 3 ∈ (0...5)) → {0, 3} ⊆ (0...5))
233	195, 209, 232	mp2an 692	. . . . . . . 8 ⊢ {0, 3} ⊆ (0...5)
234		prssi 4827	. . . . . . . . 9 ⊢ ((0 ∈ (0...5) ∧ 5 ∈ (0...5)) → {0, 5} ⊆ (0...5))
235	195, 229, 234	mp2an 692	. . . . . . . 8 ⊢ {0, 5} ⊆ (0...5)
236		sseq1 4022	. . . . . . . . 9 ⊢ (𝑒 = {4, 5} → (𝑒 ⊆ (0...5) ↔ {4, 5} ⊆ (0...5)))
237		sseq1 4022	. . . . . . . . 9 ⊢ (𝑒 = {0, 3} → (𝑒 ⊆ (0...5) ↔ {0, 3} ⊆ (0...5)))
238		sseq1 4022	. . . . . . . . 9 ⊢ (𝑒 = {0, 5} → (𝑒 ⊆ (0...5) ↔ {0, 5} ⊆ (0...5)))
239	6, 7, 8, 236, 237, 238	raltp 4711	. . . . . . . 8 ⊢ (∀𝑒 ∈ {{4, 5}, {0, 3}, {0, 5}}𝑒 ⊆ (0...5) ↔ ({4, 5} ⊆ (0...5) ∧ {0, 3} ⊆ (0...5) ∧ {0, 5} ⊆ (0...5)))
240	231, 233, 235, 239	mpbir3an 1341	. . . . . . 7 ⊢ ∀𝑒 ∈ {{4, 5}, {0, 3}, {0, 5}}𝑒 ⊆ (0...5)
241		ralunb 4208	. . . . . . 7 ⊢ (∀𝑒 ∈ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})𝑒 ⊆ (0...5) ↔ (∀𝑒 ∈ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}})𝑒 ⊆ (0...5) ∧ ∀𝑒 ∈ {{4, 5}, {0, 3}, {0, 5}}𝑒 ⊆ (0...5)))
242	226, 240, 241	mpbir2an 711	. . . . . 6 ⊢ ∀𝑒 ∈ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})𝑒 ⊆ (0...5)
243		pwssb 5107	. . . . . 6 ⊢ ((({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ 𝒫 (0...5) ↔ ∀𝑒 ∈ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})𝑒 ⊆ (0...5))
244	242, 243	mpbir 231	. . . . 5 ⊢ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ 𝒫 (0...5)
245		usgrexmpl2.v	. . . . . 6 ⊢ 𝑉 = (0...5)
246	245	pweqi 4622	. . . . 5 ⊢ 𝒫 𝑉 = 𝒫 (0...5)
247	244, 246	sseqtrri 4034	. . . 4 ⊢ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ 𝒫 𝑉
248		prhash2ex 14441	. . . . . . 7 ⊢ (♯‘{0, 1}) = 2
249		1ex 11261	. . . . . . . . 9 ⊢ 1 ∈ V
250		2ex 12347	. . . . . . . . 9 ⊢ 2 ∈ V
251	249, 250, 73	3pm3.2i 1339	. . . . . . . 8 ⊢ (1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2)
252		hashprb 14439	. . . . . . . 8 ⊢ ((1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2) ↔ (♯‘{1, 2}) = 2)
253	251, 252	mpbi 230	. . . . . . 7 ⊢ (♯‘{1, 2}) = 2
254		3ex 12352	. . . . . . . . 9 ⊢ 3 ∈ V
255	250, 254, 104	3pm3.2i 1339	. . . . . . . 8 ⊢ (2 ∈ V ∧ 3 ∈ V ∧ 2 ≠ 3)
256		hashprb 14439	. . . . . . . 8 ⊢ ((2 ∈ V ∧ 3 ∈ V ∧ 2 ≠ 3) ↔ (♯‘{2, 3}) = 2)
257	255, 256	mpbi 230	. . . . . . 7 ⊢ (♯‘{2, 3}) = 2
258		fveqeq2 6920	. . . . . . . 8 ⊢ (𝑒 = {0, 1} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 1}) = 2))
259		fveqeq2 6920	. . . . . . . 8 ⊢ (𝑒 = {1, 2} → ((♯‘𝑒) = 2 ↔ (♯‘{1, 2}) = 2))
260		fveqeq2 6920	. . . . . . . 8 ⊢ (𝑒 = {2, 3} → ((♯‘𝑒) = 2 ↔ (♯‘{2, 3}) = 2))
261	1, 2, 3, 258, 259, 260	raltp 4711	. . . . . . 7 ⊢ (∀𝑒 ∈ {{0, 1}, {1, 2}, {2, 3}} (♯‘𝑒) = 2 ↔ ((♯‘{0, 1}) = 2 ∧ (♯‘{1, 2}) = 2 ∧ (♯‘{2, 3}) = 2))
262	248, 253, 257, 261	mpbir3an 1341	. . . . . 6 ⊢ ∀𝑒 ∈ {{0, 1}, {1, 2}, {2, 3}} (♯‘𝑒) = 2
263	33	elexi 3502	. . . . . . . . 9 ⊢ 4 ∈ V
264	254, 263, 135	3pm3.2i 1339	. . . . . . . 8 ⊢ (3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4)
265		hashprb 14439	. . . . . . . 8 ⊢ ((3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4) ↔ (♯‘{3, 4}) = 2)
266	264, 265	mpbi 230	. . . . . . 7 ⊢ (♯‘{3, 4}) = 2
267		fveqeq2 6920	. . . . . . . 8 ⊢ (𝑒 = {3, 4} → ((♯‘𝑒) = 2 ↔ (♯‘{3, 4}) = 2))
268	5, 267	ralsn 4687	. . . . . . 7 ⊢ (∀𝑒 ∈ {{3, 4}} (♯‘𝑒) = 2 ↔ (♯‘{3, 4}) = 2)
269	266, 268	mpbir 231	. . . . . 6 ⊢ ∀𝑒 ∈ {{3, 4}} (♯‘𝑒) = 2
270		ralunb 4208	. . . . . 6 ⊢ (∀𝑒 ∈ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}})(♯‘𝑒) = 2 ↔ (∀𝑒 ∈ {{0, 1}, {1, 2}, {2, 3}} (♯‘𝑒) = 2 ∧ ∀𝑒 ∈ {{3, 4}} (♯‘𝑒) = 2))
271	262, 269, 270	mpbir2an 711	. . . . 5 ⊢ ∀𝑒 ∈ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}})(♯‘𝑒) = 2
272	43	elexi 3502	. . . . . . . 8 ⊢ 5 ∈ V
273	263, 272, 163	3pm3.2i 1339	. . . . . . 7 ⊢ (4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5)
274		hashprb 14439	. . . . . . 7 ⊢ ((4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5) ↔ (♯‘{4, 5}) = 2)
275	273, 274	mpbi 230	. . . . . 6 ⊢ (♯‘{4, 5}) = 2
276		c0ex 11259	. . . . . . . 8 ⊢ 0 ∈ V
277	276, 254, 28	3pm3.2i 1339	. . . . . . 7 ⊢ (0 ∈ V ∧ 3 ∈ V ∧ 0 ≠ 3)
278		hashprb 14439	. . . . . . 7 ⊢ ((0 ∈ V ∧ 3 ∈ V ∧ 0 ≠ 3) ↔ (♯‘{0, 3}) = 2)
279	277, 278	mpbi 230	. . . . . 6 ⊢ (♯‘{0, 3}) = 2
280	276, 272, 47	3pm3.2i 1339	. . . . . . 7 ⊢ (0 ∈ V ∧ 5 ∈ V ∧ 0 ≠ 5)
281		hashprb 14439	. . . . . . 7 ⊢ ((0 ∈ V ∧ 5 ∈ V ∧ 0 ≠ 5) ↔ (♯‘{0, 5}) = 2)
282	280, 281	mpbi 230	. . . . . 6 ⊢ (♯‘{0, 5}) = 2
283		fveqeq2 6920	. . . . . . 7 ⊢ (𝑒 = {4, 5} → ((♯‘𝑒) = 2 ↔ (♯‘{4, 5}) = 2))
284		fveqeq2 6920	. . . . . . 7 ⊢ (𝑒 = {0, 3} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 3}) = 2))
285		fveqeq2 6920	. . . . . . 7 ⊢ (𝑒 = {0, 5} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 5}) = 2))
286	6, 7, 8, 283, 284, 285	raltp 4711	. . . . . 6 ⊢ (∀𝑒 ∈ {{4, 5}, {0, 3}, {0, 5}} (♯‘𝑒) = 2 ↔ ((♯‘{4, 5}) = 2 ∧ (♯‘{0, 3}) = 2 ∧ (♯‘{0, 5}) = 2))
287	275, 279, 282, 286	mpbir3an 1341	. . . . 5 ⊢ ∀𝑒 ∈ {{4, 5}, {0, 3}, {0, 5}} (♯‘𝑒) = 2
288		ralunb 4208	. . . . 5 ⊢ (∀𝑒 ∈ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})(♯‘𝑒) = 2 ↔ (∀𝑒 ∈ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}})(♯‘𝑒) = 2 ∧ ∀𝑒 ∈ {{4, 5}, {0, 3}, {0, 5}} (♯‘𝑒) = 2))
289	271, 287, 288	mpbir2an 711	. . . 4 ⊢ ∀𝑒 ∈ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})(♯‘𝑒) = 2
290		ssrab 4084	. . . 4 ⊢ ((({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} ↔ ((({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ 𝒫 𝑉 ∧ ∀𝑒 ∈ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})(♯‘𝑒) = 2))
291	247, 289, 290	mpbir2an 711	. . 3 ⊢ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}
292		f1ss 6814	. . 3 ⊢ ((𝐸:dom 𝐸–1-1→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ∧ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}) → 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2})
293	193, 291, 292	sylancl 586	. 2 ⊢ ((((({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V) ∧ {3, 4} ∈ V ∧ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V)) ∧ (((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))) ∧ (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5})))) ∧ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩) → 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2})
294	175, 176, 293	mp2an 692	1 ⊢ 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1538 ∈ wcel 2107 ≠ wne 2939 ∀wral 3060 {crab 3434 Vcvv 3479 ∪ cun 3962 ⊆ wss 3964 𝒫 cpw 4606 {csn 4632 {cpr 4634 {ctp 4636 class class class wbr 5149 dom cdm 5690 –1-1→wf1 6563 –1-1-onto→wf1o 6565 ‘cfv 6566 (class class class)co 7435 0cc0 11159 1c1 11160 ≤ cle 11300 2c2 12325 3c3 12326 4c4 12327 5c5 12328 7c7 12330 ℕ₀cn0 12530 ...cfz 13550 ..^cfzo 13697 ♯chash 14372 Word cword 14555 ⟨“cs7 14888

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-rep 5286 ax-sep 5303 ax-nul 5313 ax-pow 5372 ax-pr 5439 ax-un 7758 ax-cnex 11215 ax-resscn 11216 ax-1cn 11217 ax-icn 11218 ax-addcl 11219 ax-addrcl 11220 ax-mulcl 11221 ax-mulrcl 11222 ax-mulcom 11223 ax-addass 11224 ax-mulass 11225 ax-distr 11226 ax-i2m1 11227 ax-1ne0 11228 ax-1rid 11229 ax-rnegex 11230 ax-rrecex 11231 ax-cnre 11232 ax-pre-lttri 11233 ax-pre-lttrn 11234 ax-pre-ltadd 11235 ax-pre-mulgt0 11236

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1541 df-fal 1551 df-ex 1778 df-nf 1782 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-reu 3380 df-rab 3435 df-v 3481 df-sbc 3793 df-csb 3910 df-dif 3967 df-un 3969 df-in 3971 df-ss 3981 df-pss 3984 df-nul 4341 df-if 4533 df-pw 4608 df-sn 4633 df-pr 4635 df-tp 4637 df-op 4639 df-uni 4914 df-int 4953 df-iun 4999 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5584 df-eprel 5590 df-po 5598 df-so 5599 df-fr 5642 df-we 5644 df-xp 5696 df-rel 5697 df-cnv 5698 df-co 5699 df-dm 5700 df-rn 5701 df-res 5702 df-ima 5703 df-pred 6326 df-ord 6392 df-on 6393 df-lim 6394 df-suc 6395 df-iota 6519 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-riota 7392 df-ov 7438 df-oprab 7439 df-mpo 7440 df-om 7892 df-1st 8019 df-2nd 8020 df-frecs 8311 df-wrecs 8342 df-recs 8416 df-rdg 8455 df-1o 8511 df-2o 8512 df-oadd 8515 df-er 8750 df-en 8991 df-dom 8992 df-sdom 8993 df-fin 8994 df-dju 9945 df-card 9983 df-pnf 11301 df-mnf 11302 df-xr 11303 df-ltxr 11304 df-le 11305 df-sub 11498 df-neg 11499 df-nn 12271 df-2 12333 df-3 12334 df-4 12335 df-5 12336 df-6 12337 df-7 12338 df-n0 12531 df-xnn0 12604 df-z 12618 df-uz 12883 df-fz 13551 df-fzo 13698 df-hash 14373 df-word 14556 df-concat 14612 df-s1 14637 df-s2 14890 df-s3 14891 df-s4 14892 df-s5 14893 df-s6 14894 df-s7 14895

This theorem is referenced by: usgrexmpl2 47935

W3C validator