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 48950

Description: Lemma for usgrexmpl2 48951. (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 5407	. . . . 5 ⊢ {0, 1} ∈ V
2		prex 5407	. . . . 5 ⊢ {1, 2} ∈ V
3		prex 5407	. . . . 5 ⊢ {2, 3} ∈ V
4	1, 2, 3	3pm3.2i 1358	. . . 4 ⊢ ({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V)
5		prex 5407	. . . 4 ⊢ {3, 4} ∈ V
6		prex 5407	. . . . 5 ⊢ {4, 5} ∈ V
7		prex 5407	. . . . 5 ⊢ {0, 3} ∈ V
8		prex 5407	. . . . 5 ⊢ {0, 5} ∈ V
9	6, 7, 8	3pm3.2i 1358	. . . 4 ⊢ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V)
10	4, 5, 9	3pm3.2i 1358	. . 3 ⊢ (({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V) ∧ {3, 4} ∈ V ∧ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V))
11		0nn0 12547	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
12		1nn0 12548	. . . . . . . . . 10 ⊢ 1 ∈ ℕ₀
13	11, 12	pm3.2i 476	. . . . . . . . 9 ⊢ (0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀)
14		2nn0 12549	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
15	12, 14	pm3.2i 476	. . . . . . . . 9 ⊢ (1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀)
16	13, 15	pm3.2i 476	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀))
17		0ne1 12340	. . . . . . . . . 10 ⊢ 0 ≠ 1
18		0ne2 12478	. . . . . . . . . 10 ⊢ 0 ≠ 2
19	17, 18	pm3.2i 476	. . . . . . . . 9 ⊢ (0 ≠ 1 ∧ 0 ≠ 2)
20	19	orci 879	. . . . . . . 8 ⊢ ((0 ≠ 1 ∧ 0 ≠ 2) ∨ (1 ≠ 1 ∧ 1 ≠ 2))
21		prneimg 4817	. . . . . . . 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 12550	. . . . . . . . . 10 ⊢ 3 ∈ ℕ₀
24	14, 23	pm3.2i 476	. . . . . . . . 9 ⊢ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀)
25	13, 24	pm3.2i 476	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀))
26		0re 11238	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
27		3pos 12377	. . . . . . . . . . 11 ⊢ 0 < 3
28	26, 27	ltneii 11351	. . . . . . . . . 10 ⊢ 0 ≠ 3
29	18, 28	pm3.2i 476	. . . . . . . . 9 ⊢ (0 ≠ 2 ∧ 0 ≠ 3)
30	29	orci 879	. . . . . . . 8 ⊢ ((0 ≠ 2 ∧ 0 ≠ 3) ∨ (1 ≠ 2 ∧ 1 ≠ 3))
31		prneimg 4817	. . . . . . . 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 12551	. . . . . . . . . 10 ⊢ 4 ∈ ℕ₀
34	23, 33	pm3.2i 476	. . . . . . . . 9 ⊢ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀)
35	13, 34	pm3.2i 476	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀))
36		4pos 12379	. . . . . . . . . . 11 ⊢ 0 < 4
37	26, 36	ltneii 11351	. . . . . . . . . 10 ⊢ 0 ≠ 4
38	28, 37	pm3.2i 476	. . . . . . . . 9 ⊢ (0 ≠ 3 ∧ 0 ≠ 4)
39	38	orci 879	. . . . . . . 8 ⊢ ((0 ≠ 3 ∧ 0 ≠ 4) ∨ (1 ≠ 3 ∧ 1 ≠ 4))
40		prneimg 4817	. . . . . . . 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 1358	. . . . . 6 ⊢ ({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4})
43		5nn0 12552	. . . . . . . . . 10 ⊢ 5 ∈ ℕ₀
44	33, 43	pm3.2i 476	. . . . . . . . 9 ⊢ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀)
45	13, 44	pm3.2i 476	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
46		5pos 12381	. . . . . . . . . . 11 ⊢ 0 < 5
47	26, 46	ltneii 11351	. . . . . . . . . 10 ⊢ 0 ≠ 5
48	37, 47	pm3.2i 476	. . . . . . . . 9 ⊢ (0 ≠ 4 ∧ 0 ≠ 5)
49	48	orci 879	. . . . . . . 8 ⊢ ((0 ≠ 4 ∧ 0 ≠ 5) ∨ (1 ≠ 4 ∧ 1 ≠ 5))
50		prneimg 4817	. . . . . . . 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 476	. . . . . . . . 9 ⊢ (0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀)
53	13, 52	pm3.2i 476	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀))
54		ax-1ne0 11197	. . . . . . . . . 10 ⊢ 1 ≠ 0
55		1re 11236	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
56		1lt3 12444	. . . . . . . . . . 11 ⊢ 1 < 3
57	55, 56	ltneii 11351	. . . . . . . . . 10 ⊢ 1 ≠ 3
58	54, 57	pm3.2i 476	. . . . . . . . 9 ⊢ (1 ≠ 0 ∧ 1 ≠ 3)
59	58	olci 880	. . . . . . . 8 ⊢ ((0 ≠ 0 ∧ 0 ≠ 3) ∨ (1 ≠ 0 ∧ 1 ≠ 3))
60		prneimg 4817	. . . . . . . 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 476	. . . . . . . . 9 ⊢ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀)
63	13, 62	pm3.2i 476	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
64		1lt5 12451	. . . . . . . . . . 11 ⊢ 1 < 5
65	55, 64	ltneii 11351	. . . . . . . . . 10 ⊢ 1 ≠ 5
66	54, 65	pm3.2i 476	. . . . . . . . 9 ⊢ (1 ≠ 0 ∧ 1 ≠ 5)
67	66	olci 880	. . . . . . . 8 ⊢ ((0 ≠ 0 ∧ 0 ≠ 5) ∨ (1 ≠ 0 ∧ 1 ≠ 5))
68		prneimg 4817	. . . . . . . 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 1358	. . . . . 6 ⊢ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})
71	42, 70	pm3.2i 476	. . . . 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 476	. . . . . . . 8 ⊢ ((1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) ∧ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀))
73		1ne2 12479	. . . . . . . . . 10 ⊢ 1 ≠ 2
74	73, 57	pm3.2i 476	. . . . . . . . 9 ⊢ (1 ≠ 2 ∧ 1 ≠ 3)
75	74	orci 879	. . . . . . . 8 ⊢ ((1 ≠ 2 ∧ 1 ≠ 3) ∨ (2 ≠ 2 ∧ 2 ≠ 3))
76		prneimg 4817	. . . . . . . 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 476	. . . . . . . 8 ⊢ ((1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) ∧ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀))
79		1lt4 12447	. . . . . . . . . . 11 ⊢ 1 < 4
80	55, 79	ltneii 11351	. . . . . . . . . 10 ⊢ 1 ≠ 4
81	57, 80	pm3.2i 476	. . . . . . . . 9 ⊢ (1 ≠ 3 ∧ 1 ≠ 4)
82	81	orci 879	. . . . . . . 8 ⊢ ((1 ≠ 3 ∧ 1 ≠ 4) ∨ (2 ≠ 3 ∧ 2 ≠ 4))
83		prneimg 4817	. . . . . . . 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 476	. . . . . 6 ⊢ ({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4})
86	15, 44	pm3.2i 476	. . . . . . . 8 ⊢ ((1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) ∧ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
87	80, 65	pm3.2i 476	. . . . . . . . 9 ⊢ (1 ≠ 4 ∧ 1 ≠ 5)
88	87	orci 879	. . . . . . . 8 ⊢ ((1 ≠ 4 ∧ 1 ≠ 5) ∨ (2 ≠ 4 ∧ 2 ≠ 5))
89		prneimg 4817	. . . . . . . 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 476	. . . . . . . 8 ⊢ ((1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀))
92	58	orci 879	. . . . . . . 8 ⊢ ((1 ≠ 0 ∧ 1 ≠ 3) ∨ (2 ≠ 0 ∧ 2 ≠ 3))
93		prneimg 4817	. . . . . . . 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 476	. . . . . . . 8 ⊢ ((1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
96	66	orci 879	. . . . . . . 8 ⊢ ((1 ≠ 0 ∧ 1 ≠ 5) ∨ (2 ≠ 0 ∧ 2 ≠ 5))
97		prneimg 4817	. . . . . . . 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 1358	. . . . . 6 ⊢ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})
100	85, 99	pm3.2i 476	. . . . 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 476	. . . . . . 7 ⊢ ((2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) ∧ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀))
102		2re 12343	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
103		2lt3 12442	. . . . . . . . . 10 ⊢ 2 < 3
104	102, 103	ltneii 11351	. . . . . . . . 9 ⊢ 2 ≠ 3
105		2lt4 12446	. . . . . . . . . 10 ⊢ 2 < 4
106	102, 105	ltneii 11351	. . . . . . . . 9 ⊢ 2 ≠ 4
107	104, 106	pm3.2i 476	. . . . . . . 8 ⊢ (2 ≠ 3 ∧ 2 ≠ 4)
108	107	orci 879	. . . . . . 7 ⊢ ((2 ≠ 3 ∧ 2 ≠ 4) ∨ (3 ≠ 3 ∧ 3 ≠ 4))
109		prneimg 4817	. . . . . . 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 476	. . . . . . . 8 ⊢ ((2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) ∧ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
112		2lt5 12450	. . . . . . . . . . 11 ⊢ 2 < 5
113	102, 112	ltneii 11351	. . . . . . . . . 10 ⊢ 2 ≠ 5
114	106, 113	pm3.2i 476	. . . . . . . . 9 ⊢ (2 ≠ 4 ∧ 2 ≠ 5)
115	114	orci 879	. . . . . . . 8 ⊢ ((2 ≠ 4 ∧ 2 ≠ 5) ∨ (3 ≠ 4 ∧ 3 ≠ 5))
116		prneimg 4817	. . . . . . . 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 476	. . . . . . . 8 ⊢ ((2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀))
119		2ne0 12375	. . . . . . . . . 10 ⊢ 2 ≠ 0
120	119, 104	pm3.2i 476	. . . . . . . . 9 ⊢ (2 ≠ 0 ∧ 2 ≠ 3)
121	120	orci 879	. . . . . . . 8 ⊢ ((2 ≠ 0 ∧ 2 ≠ 3) ∨ (3 ≠ 0 ∧ 3 ≠ 3))
122		prneimg 4817	. . . . . . . 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 476	. . . . . . . 8 ⊢ ((2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
125	119, 113	pm3.2i 476	. . . . . . . . 9 ⊢ (2 ≠ 0 ∧ 2 ≠ 5)
126	125	orci 879	. . . . . . . 8 ⊢ ((2 ≠ 0 ∧ 2 ≠ 5) ∨ (3 ≠ 0 ∧ 3 ≠ 5))
127		prneimg 4817	. . . . . . . 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 1358	. . . . . 6 ⊢ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5})
130	110, 129	pm3.2i 476	. . . . 5 ⊢ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))
131	71, 100, 130	3pm3.2i 1358	. . . 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 476	. . . . . . 7 ⊢ ((3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀) ∧ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
133		3re 12349	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
134		3lt4 12445	. . . . . . . . . 10 ⊢ 3 < 4
135	133, 134	ltneii 11351	. . . . . . . . 9 ⊢ 3 ≠ 4
136		3lt5 12449	. . . . . . . . . 10 ⊢ 3 < 5
137	133, 136	ltneii 11351	. . . . . . . . 9 ⊢ 3 ≠ 5
138	135, 137	pm3.2i 476	. . . . . . . 8 ⊢ (3 ≠ 4 ∧ 3 ≠ 5)
139	138	orci 879	. . . . . . 7 ⊢ ((3 ≠ 4 ∧ 3 ≠ 5) ∨ (4 ≠ 4 ∧ 4 ≠ 5))
140		prneimg 4817	. . . . . . 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 476	. . . . . . 7 ⊢ ((3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀))
143		4ne0 12380	. . . . . . . . 9 ⊢ 4 ≠ 0
144	135	necomi 3011	. . . . . . . . 9 ⊢ 4 ≠ 3
145	143, 144	pm3.2i 476	. . . . . . . 8 ⊢ (4 ≠ 0 ∧ 4 ≠ 3)
146	145	olci 880	. . . . . . 7 ⊢ ((3 ≠ 0 ∧ 3 ≠ 3) ∨ (4 ≠ 0 ∧ 4 ≠ 3))
147		prneimg 4817	. . . . . . 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 476	. . . . . . 7 ⊢ ((3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
150		3ne0 12378	. . . . . . . . 9 ⊢ 3 ≠ 0
151	150, 137	pm3.2i 476	. . . . . . . 8 ⊢ (3 ≠ 0 ∧ 3 ≠ 5)
152	151	orci 879	. . . . . . 7 ⊢ ((3 ≠ 0 ∧ 3 ≠ 5) ∨ (4 ≠ 0 ∧ 4 ≠ 5))
153		prneimg 4817	. . . . . . 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 1358	. . . . 5 ⊢ ({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5})
156	44, 52	pm3.2i 476	. . . . . . 7 ⊢ ((4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀))
157	145	orci 879	. . . . . . 7 ⊢ ((4 ≠ 0 ∧ 4 ≠ 3) ∨ (5 ≠ 0 ∧ 5 ≠ 3))
158		prneimg 4817	. . . . . . 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 476	. . . . . . 7 ⊢ ((4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
161		4re 12353	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
162		4lt5 12448	. . . . . . . . . 10 ⊢ 4 < 5
163	161, 162	ltneii 11351	. . . . . . . . 9 ⊢ 4 ≠ 5
164	143, 163	pm3.2i 476	. . . . . . . 8 ⊢ (4 ≠ 0 ∧ 4 ≠ 5)
165	164	orci 879	. . . . . . 7 ⊢ ((4 ≠ 0 ∧ 4 ≠ 5) ∨ (5 ≠ 0 ∧ 5 ≠ 5))
166		prneimg 4817	. . . . . . 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 476	. . . . . . 7 ⊢ ((0 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) ∧ (0 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
169	151	olci 880	. . . . . . 7 ⊢ ((0 ≠ 0 ∧ 0 ≠ 5) ∨ (3 ≠ 0 ∧ 3 ≠ 5))
170		prneimg 4817	. . . . . . 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 1358	. . . . 5 ⊢ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5})
173	155, 172	pm3.2i 476	. . . 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 476	. . 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 476	. 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 15043	. . . . . . 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 412	. . . . . 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 14977	. . . . . . . 8 ⊢ (♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩) = 7
180	179	oveq2i 7428	. . . . . . 7 ⊢ (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩)) = (0..^7)
181		f1oeq2 6810	. . . . . . 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 237	. . . . 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 5892	. . . . . . 7 ⊢ dom 𝐸 = dom ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩
185		s7cli 14960	. . . . . . . 8 ⊢ ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩ ∈ Word V
186		wrddm 14590	. . . . . . . 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 2785	. . . . . 6 ⊢ dom 𝐸 = (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))
189		f1oeq2 6810	. . . . . 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 237	. . . 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 6820	. . . 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 18	. . 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 13683	. . . . . . . . . . 11 ⊢ (5 ∈ ℕ₀ → 0 ∈ (0...5))
195	43, 194	ax-mp 5	. . . . . . . . . 10 ⊢ 0 ∈ (0...5)
196		5re 12356	. . . . . . . . . . . 12 ⊢ 5 ∈ ℝ
197	55, 196, 64	ltleii 11361	. . . . . . . . . . 11 ⊢ 1 ≤ 5
198		elfz2nn0 13677	. . . . . . . . . . 11 ⊢ (1 ∈ (0...5) ↔ (1 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 1 ≤ 5))
199	12, 43, 197, 198	mpbir3an 1360	. . . . . . . . . 10 ⊢ 1 ∈ (0...5)
200		prssi 4785	. . . . . . . . . 10 ⊢ ((0 ∈ (0...5) ∧ 1 ∈ (0...5)) → {0, 1} ⊆ (0...5))
201	195, 199, 200	mp2an 705	. . . . . . . . 9 ⊢ {0, 1} ⊆ (0...5)
202	102, 196, 112	ltleii 11361	. . . . . . . . . . 11 ⊢ 2 ≤ 5
203		elfz2nn0 13677	. . . . . . . . . . 11 ⊢ (2 ∈ (0...5) ↔ (2 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 2 ≤ 5))
204	14, 43, 202, 203	mpbir3an 1360	. . . . . . . . . 10 ⊢ 2 ∈ (0...5)
205		prssi 4785	. . . . . . . . . 10 ⊢ ((1 ∈ (0...5) ∧ 2 ∈ (0...5)) → {1, 2} ⊆ (0...5))
206	199, 204, 205	mp2an 705	. . . . . . . . 9 ⊢ {1, 2} ⊆ (0...5)
207	133, 196, 136	ltleii 11361	. . . . . . . . . . 11 ⊢ 3 ≤ 5
208		elfz2nn0 13677	. . . . . . . . . . 11 ⊢ (3 ∈ (0...5) ↔ (3 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 3 ≤ 5))
209	23, 43, 207, 208	mpbir3an 1360	. . . . . . . . . 10 ⊢ 3 ∈ (0...5)
210		prssi 4785	. . . . . . . . . 10 ⊢ ((2 ∈ (0...5) ∧ 3 ∈ (0...5)) → {2, 3} ⊆ (0...5))
211	204, 209, 210	mp2an 705	. . . . . . . . 9 ⊢ {2, 3} ⊆ (0...5)
212		sseq1 3959	. . . . . . . . . 10 ⊢ (𝑒 = {0, 1} → (𝑒 ⊆ (0...5) ↔ {0, 1} ⊆ (0...5)))
213		sseq1 3959	. . . . . . . . . 10 ⊢ (𝑒 = {1, 2} → (𝑒 ⊆ (0...5) ↔ {1, 2} ⊆ (0...5)))
214		sseq1 3959	. . . . . . . . . 10 ⊢ (𝑒 = {2, 3} → (𝑒 ⊆ (0...5) ↔ {2, 3} ⊆ (0...5)))
215	1, 2, 3, 212, 213, 214	raltp 4669	. . . . . . . . 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 1360	. . . . . . . 8 ⊢ ∀𝑒 ∈ {{0, 1}, {1, 2}, {2, 3}}𝑒 ⊆ (0...5)
217	161, 196, 162	ltleii 11361	. . . . . . . . . . 11 ⊢ 4 ≤ 5
218		elfz2nn0 13677	. . . . . . . . . . 11 ⊢ (4 ∈ (0...5) ↔ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 4 ≤ 5))
219	33, 43, 217, 218	mpbir3an 1360	. . . . . . . . . 10 ⊢ 4 ∈ (0...5)
220		prssi 4785	. . . . . . . . . 10 ⊢ ((3 ∈ (0...5) ∧ 4 ∈ (0...5)) → {3, 4} ⊆ (0...5))
221	209, 219, 220	mp2an 705	. . . . . . . . 9 ⊢ {3, 4} ⊆ (0...5)
222		sseq1 3959	. . . . . . . . . 10 ⊢ (𝑒 = {3, 4} → (𝑒 ⊆ (0...5) ↔ {3, 4} ⊆ (0...5)))
223	5, 222	ralsn 4645	. . . . . . . . 9 ⊢ (∀𝑒 ∈ {{3, 4}}𝑒 ⊆ (0...5) ↔ {3, 4} ⊆ (0...5))
224	221, 223	mpbir 234	. . . . . . . 8 ⊢ ∀𝑒 ∈ {{3, 4}}𝑒 ⊆ (0...5)
225		ralunb 4146	. . . . . . . 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 724	. . . . . . 7 ⊢ ∀𝑒 ∈ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}})𝑒 ⊆ (0...5)
227	196	leidi 11776	. . . . . . . . . 10 ⊢ 5 ≤ 5
228		elfz2nn0 13677	. . . . . . . . . 10 ⊢ (5 ∈ (0...5) ↔ (5 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 5 ≤ 5))
229	43, 43, 227, 228	mpbir3an 1360	. . . . . . . . 9 ⊢ 5 ∈ (0...5)
230		prssi 4785	. . . . . . . . 9 ⊢ ((4 ∈ (0...5) ∧ 5 ∈ (0...5)) → {4, 5} ⊆ (0...5))
231	219, 229, 230	mp2an 705	. . . . . . . 8 ⊢ {4, 5} ⊆ (0...5)
232		prssi 4785	. . . . . . . . 9 ⊢ ((0 ∈ (0...5) ∧ 3 ∈ (0...5)) → {0, 3} ⊆ (0...5))
233	195, 209, 232	mp2an 705	. . . . . . . 8 ⊢ {0, 3} ⊆ (0...5)
234		prssi 4785	. . . . . . . . 9 ⊢ ((0 ∈ (0...5) ∧ 5 ∈ (0...5)) → {0, 5} ⊆ (0...5))
235	195, 229, 234	mp2an 705	. . . . . . . 8 ⊢ {0, 5} ⊆ (0...5)
236		sseq1 3959	. . . . . . . . 9 ⊢ (𝑒 = {4, 5} → (𝑒 ⊆ (0...5) ↔ {4, 5} ⊆ (0...5)))
237		sseq1 3959	. . . . . . . . 9 ⊢ (𝑒 = {0, 3} → (𝑒 ⊆ (0...5) ↔ {0, 3} ⊆ (0...5)))
238		sseq1 3959	. . . . . . . . 9 ⊢ (𝑒 = {0, 5} → (𝑒 ⊆ (0...5) ↔ {0, 5} ⊆ (0...5)))
239	6, 7, 8, 236, 237, 238	raltp 4669	. . . . . . . 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 1360	. . . . . . 7 ⊢ ∀𝑒 ∈ {{4, 5}, {0, 3}, {0, 5}}𝑒 ⊆ (0...5)
241		ralunb 4146	. . . . . . 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 724	. . . . . 6 ⊢ ∀𝑒 ∈ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})𝑒 ⊆ (0...5)
243		pwssb 5065	. . . . . 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 234	. . . . 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 4576	. . . . 5 ⊢ 𝒫 𝑉 = 𝒫 (0...5)
247	244, 246	sseqtrri 3983	. . . 4 ⊢ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ 𝒫 𝑉
248		prhash2ex 14467	. . . . . . 7 ⊢ (♯‘{0, 1}) = 2
249		1ex 11231	. . . . . . . . 9 ⊢ 1 ∈ V
250		2ex 12346	. . . . . . . . 9 ⊢ 2 ∈ V
251	249, 250, 73	3pm3.2i 1358	. . . . . . . 8 ⊢ (1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2)
252		hashprb 14465	. . . . . . . 8 ⊢ ((1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2) ↔ (♯‘{1, 2}) = 2)
253	251, 252	mpbi 233	. . . . . . 7 ⊢ (♯‘{1, 2}) = 2
254		3ex 12351	. . . . . . . . 9 ⊢ 3 ∈ V
255	250, 254, 104	3pm3.2i 1358	. . . . . . . 8 ⊢ (2 ∈ V ∧ 3 ∈ V ∧ 2 ≠ 3)
256		hashprb 14465	. . . . . . . 8 ⊢ ((2 ∈ V ∧ 3 ∈ V ∧ 2 ≠ 3) ↔ (♯‘{2, 3}) = 2)
257	255, 256	mpbi 233	. . . . . . 7 ⊢ (♯‘{2, 3}) = 2
258		fveqeq2 6891	. . . . . . . 8 ⊢ (𝑒 = {0, 1} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 1}) = 2))
259		fveqeq2 6891	. . . . . . . 8 ⊢ (𝑒 = {1, 2} → ((♯‘𝑒) = 2 ↔ (♯‘{1, 2}) = 2))
260		fveqeq2 6891	. . . . . . . 8 ⊢ (𝑒 = {2, 3} → ((♯‘𝑒) = 2 ↔ (♯‘{2, 3}) = 2))
261	1, 2, 3, 258, 259, 260	raltp 4669	. . . . . . 7 ⊢ (∀𝑒 ∈ {{0, 1}, {1, 2}, {2, 3}} (♯‘𝑒) = 2 ↔ ((♯‘{0, 1}) = 2 ∧ (♯‘{1, 2}) = 2 ∧ (♯‘{2, 3}) = 2))
262	248, 253, 257, 261	mpbir3an 1360	. . . . . 6 ⊢ ∀𝑒 ∈ {{0, 1}, {1, 2}, {2, 3}} (♯‘𝑒) = 2
263	33	elexi 3475	. . . . . . . . 9 ⊢ 4 ∈ V
264	254, 263, 135	3pm3.2i 1358	. . . . . . . 8 ⊢ (3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4)
265		hashprb 14465	. . . . . . . 8 ⊢ ((3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4) ↔ (♯‘{3, 4}) = 2)
266	264, 265	mpbi 233	. . . . . . 7 ⊢ (♯‘{3, 4}) = 2
267		fveqeq2 6891	. . . . . . . 8 ⊢ (𝑒 = {3, 4} → ((♯‘𝑒) = 2 ↔ (♯‘{3, 4}) = 2))
268	5, 267	ralsn 4645	. . . . . . 7 ⊢ (∀𝑒 ∈ {{3, 4}} (♯‘𝑒) = 2 ↔ (♯‘{3, 4}) = 2)
269	266, 268	mpbir 234	. . . . . 6 ⊢ ∀𝑒 ∈ {{3, 4}} (♯‘𝑒) = 2
270		ralunb 4146	. . . . . 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 724	. . . . 5 ⊢ ∀𝑒 ∈ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}})(♯‘𝑒) = 2
272	43	elexi 3475	. . . . . . . 8 ⊢ 5 ∈ V
273	263, 272, 163	3pm3.2i 1358	. . . . . . 7 ⊢ (4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5)
274		hashprb 14465	. . . . . . 7 ⊢ ((4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5) ↔ (♯‘{4, 5}) = 2)
275	273, 274	mpbi 233	. . . . . 6 ⊢ (♯‘{4, 5}) = 2
276		c0ex 11228	. . . . . . . 8 ⊢ 0 ∈ V
277	276, 254, 28	3pm3.2i 1358	. . . . . . 7 ⊢ (0 ∈ V ∧ 3 ∈ V ∧ 0 ≠ 3)
278		hashprb 14465	. . . . . . 7 ⊢ ((0 ∈ V ∧ 3 ∈ V ∧ 0 ≠ 3) ↔ (♯‘{0, 3}) = 2)
279	277, 278	mpbi 233	. . . . . 6 ⊢ (♯‘{0, 3}) = 2
280	276, 272, 47	3pm3.2i 1358	. . . . . . 7 ⊢ (0 ∈ V ∧ 5 ∈ V ∧ 0 ≠ 5)
281		hashprb 14465	. . . . . . 7 ⊢ ((0 ∈ V ∧ 5 ∈ V ∧ 0 ≠ 5) ↔ (♯‘{0, 5}) = 2)
282	280, 281	mpbi 233	. . . . . 6 ⊢ (♯‘{0, 5}) = 2
283		fveqeq2 6891	. . . . . . 7 ⊢ (𝑒 = {4, 5} → ((♯‘𝑒) = 2 ↔ (♯‘{4, 5}) = 2))
284		fveqeq2 6891	. . . . . . 7 ⊢ (𝑒 = {0, 3} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 3}) = 2))
285		fveqeq2 6891	. . . . . . 7 ⊢ (𝑒 = {0, 5} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 5}) = 2))
286	6, 7, 8, 283, 284, 285	raltp 4669	. . . . . 6 ⊢ (∀𝑒 ∈ {{4, 5}, {0, 3}, {0, 5}} (♯‘𝑒) = 2 ↔ ((♯‘{4, 5}) = 2 ∧ (♯‘{0, 3}) = 2 ∧ (♯‘{0, 5}) = 2))
287	275, 279, 282, 286	mpbir3an 1360	. . . . 5 ⊢ ∀𝑒 ∈ {{4, 5}, {0, 3}, {0, 5}} (♯‘𝑒) = 2
288		ralunb 4146	. . . . 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 724	. . . 4 ⊢ ∀𝑒 ∈ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})(♯‘𝑒) = 2
290		ssrab 4022	. . . 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 724	. . 3 ⊢ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}
292		f1ss 6782	. . 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 598	. 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 705	1 ⊢ 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}

Colors of variables: wff setvar class

This proof depends on syntax axioms: ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 ∀wral 3078 {crab 3414 Vcvv 3453 ∪ cun 3900 ⊆ wss 3902 𝒫 cpw 4560 {csn 4587 {cpr 4589 {ctp 4591 class class class wbr 5107 dom cdm 5659 –1-1→wf1 6534 –1-1-onto→wf1o 6536 ‘cfv 6537 (class class class)co 7417 0cc0 11128 1c1 11129 ≤ cle 11272 2c2 12323 3c3 12324 4c4 12325 5c5 12326 7c7 12328 ℕ₀cn0 12532 ...cfz 13565 ..^cfzo 13713 ♯chash 14398 Word cword 14582 ⟨“cs7 14921

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-oadd 8463 df-er 8700 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-dju 9910 df-card 9948 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-nn 12262 df-2 12331 df-3 12332 df-4 12333 df-5 12334 df-6 12335 df-7 12336 df-n0 12533 df-xnn0 12606 df-z 12620 df-uz 12892 df-fz 13566 df-fzo 13714 df-hash 14399 df-word 14583 df-concat 14640 df-s1 14667 df-s2 14923 df-s3 14924 df-s4 14925 df-s5 14926 df-s6 14927 df-s7 14928

This theorem is used by: usgrexmpl2 48951

W3C validator