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 47931

Description: Lemma for usgrexmpl2 47932. (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 5419	. . . . 5 ⊢ {0, 1} ∈ V
2		prex 5419	. . . . 5 ⊢ {1, 2} ∈ V
3		prex 5419	. . . . 5 ⊢ {2, 3} ∈ V
4	1, 2, 3	3pm3.2i 1339	. . . 4 ⊢ ({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V)
5		prex 5419	. . . 4 ⊢ {3, 4} ∈ V
6		prex 5419	. . . . 5 ⊢ {4, 5} ∈ V
7		prex 5419	. . . . 5 ⊢ {0, 3} ∈ V
8		prex 5419	. . . . 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 12525	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
12		1nn0 12526	. . . . . . . . . 10 ⊢ 1 ∈ ℕ₀
13	11, 12	pm3.2i 470	. . . . . . . . 9 ⊢ (0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀)
14		2nn0 12527	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
15	12, 14	pm3.2i 470	. . . . . . . . 9 ⊢ (1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀)
16	13, 15	pm3.2i 470	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀))
17		0ne1 12320	. . . . . . . . . 10 ⊢ 0 ≠ 1
18		0ne2 12456	. . . . . . . . . 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 4836	. . . . . . . 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 12528	. . . . . . . . . 10 ⊢ 3 ∈ ℕ₀
24	14, 23	pm3.2i 470	. . . . . . . . 9 ⊢ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀)
25	13, 24	pm3.2i 470	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀))
26		0re 11246	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
27		3pos 12354	. . . . . . . . . . 11 ⊢ 0 < 3
28	26, 27	ltneii 11357	. . . . . . . . . 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 4836	. . . . . . . 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 12529	. . . . . . . . . 10 ⊢ 4 ∈ ℕ₀
34	23, 33	pm3.2i 470	. . . . . . . . 9 ⊢ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀)
35	13, 34	pm3.2i 470	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀))
36		4pos 12356	. . . . . . . . . . 11 ⊢ 0 < 4
37	26, 36	ltneii 11357	. . . . . . . . . 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 4836	. . . . . . . 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 12530	. . . . . . . . . 10 ⊢ 5 ∈ ℕ₀
44	33, 43	pm3.2i 470	. . . . . . . . 9 ⊢ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀)
45	13, 44	pm3.2i 470	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
46		5pos 12358	. . . . . . . . . . 11 ⊢ 0 < 5
47	26, 46	ltneii 11357	. . . . . . . . . 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 4836	. . . . . . . 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 11207	. . . . . . . . . 10 ⊢ 1 ≠ 0
55		1re 11244	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
56		1lt3 12422	. . . . . . . . . . 11 ⊢ 1 < 3
57	55, 56	ltneii 11357	. . . . . . . . . 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 4836	. . . . . . . 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 12429	. . . . . . . . . . 11 ⊢ 1 < 5
65	55, 64	ltneii 11357	. . . . . . . . . 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 4836	. . . . . . . 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 12457	. . . . . . . . . 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 4836	. . . . . . . 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 12425	. . . . . . . . . . 11 ⊢ 1 < 4
80	55, 79	ltneii 11357	. . . . . . . . . 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 4836	. . . . . . . 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 4836	. . . . . . . 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 4836	. . . . . . . 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 4836	. . . . . . . 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 12323	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
103		2lt3 12421	. . . . . . . . . 10 ⊢ 2 < 3
104	102, 103	ltneii 11357	. . . . . . . . 9 ⊢ 2 ≠ 3
105		2lt4 12424	. . . . . . . . . 10 ⊢ 2 < 4
106	102, 105	ltneii 11357	. . . . . . . . 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 4836	. . . . . . 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 12428	. . . . . . . . . . 11 ⊢ 2 < 5
113	102, 112	ltneii 11357	. . . . . . . . . 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 4836	. . . . . . . 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 12353	. . . . . . . . . 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 4836	. . . . . . . 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 4836	. . . . . . . 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 12329	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
134		3lt4 12423	. . . . . . . . . 10 ⊢ 3 < 4
135	133, 134	ltneii 11357	. . . . . . . . 9 ⊢ 3 ≠ 4
136		3lt5 12427	. . . . . . . . . 10 ⊢ 3 < 5
137	133, 136	ltneii 11357	. . . . . . . . 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 4836	. . . . . . 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 12357	. . . . . . . . 9 ⊢ 4 ≠ 0
144	135	necomi 2985	. . . . . . . . 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 4836	. . . . . . 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 12355	. . . . . . . . 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 4836	. . . . . . 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 4836	. . . . . . 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 12333	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
162		4lt5 12426	. . . . . . . . . 10 ⊢ 4 < 5
163	161, 162	ltneii 11357	. . . . . . . . 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 4836	. . . . . . 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 4836	. . . . . . 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 14988	. . . . . . 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 14924	. . . . . . . 8 ⊢ (♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩) = 7
180	179	oveq2i 7425	. . . . . . 7 ⊢ (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩)) = (0..^7)
181		f1oeq2 6818	. . . . . . 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 5897	. . . . . . 7 ⊢ dom 𝐸 = dom ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩
185		s7cli 14907	. . . . . . . 8 ⊢ ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩ ∈ Word V
186		wrddm 14542	. . . . . . . 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 2757	. . . . . 6 ⊢ dom 𝐸 = (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))
189		f1oeq2 6818	. . . . . 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 6828	. . . 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 13647	. . . . . . . . . . 11 ⊢ (5 ∈ ℕ₀ → 0 ∈ (0...5))
195	43, 194	ax-mp 5	. . . . . . . . . 10 ⊢ 0 ∈ (0...5)
196		5re 12336	. . . . . . . . . . . 12 ⊢ 5 ∈ ℝ
197	55, 196, 64	ltleii 11367	. . . . . . . . . . 11 ⊢ 1 ≤ 5
198		elfz2nn0 13641	. . . . . . . . . . 11 ⊢ (1 ∈ (0...5) ↔ (1 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 1 ≤ 5))
199	12, 43, 197, 198	mpbir3an 1341	. . . . . . . . . 10 ⊢ 1 ∈ (0...5)
200		prssi 4803	. . . . . . . . . 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 11367	. . . . . . . . . . 11 ⊢ 2 ≤ 5
203		elfz2nn0 13641	. . . . . . . . . . 11 ⊢ (2 ∈ (0...5) ↔ (2 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 2 ≤ 5))
204	14, 43, 202, 203	mpbir3an 1341	. . . . . . . . . 10 ⊢ 2 ∈ (0...5)
205		prssi 4803	. . . . . . . . . 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 11367	. . . . . . . . . . 11 ⊢ 3 ≤ 5
208		elfz2nn0 13641	. . . . . . . . . . 11 ⊢ (3 ∈ (0...5) ↔ (3 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 3 ≤ 5))
209	23, 43, 207, 208	mpbir3an 1341	. . . . . . . . . 10 ⊢ 3 ∈ (0...5)
210		prssi 4803	. . . . . . . . . 10 ⊢ ((2 ∈ (0...5) ∧ 3 ∈ (0...5)) → {2, 3} ⊆ (0...5))
211	204, 209, 210	mp2an 692	. . . . . . . . 9 ⊢ {2, 3} ⊆ (0...5)
212		sseq1 3991	. . . . . . . . . 10 ⊢ (𝑒 = {0, 1} → (𝑒 ⊆ (0...5) ↔ {0, 1} ⊆ (0...5)))
213		sseq1 3991	. . . . . . . . . 10 ⊢ (𝑒 = {1, 2} → (𝑒 ⊆ (0...5) ↔ {1, 2} ⊆ (0...5)))
214		sseq1 3991	. . . . . . . . . 10 ⊢ (𝑒 = {2, 3} → (𝑒 ⊆ (0...5) ↔ {2, 3} ⊆ (0...5)))
215	1, 2, 3, 212, 213, 214	raltp 4687	. . . . . . . . 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 11367	. . . . . . . . . . 11 ⊢ 4 ≤ 5
218		elfz2nn0 13641	. . . . . . . . . . 11 ⊢ (4 ∈ (0...5) ↔ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 4 ≤ 5))
219	33, 43, 217, 218	mpbir3an 1341	. . . . . . . . . 10 ⊢ 4 ∈ (0...5)
220		prssi 4803	. . . . . . . . . 10 ⊢ ((3 ∈ (0...5) ∧ 4 ∈ (0...5)) → {3, 4} ⊆ (0...5))
221	209, 219, 220	mp2an 692	. . . . . . . . 9 ⊢ {3, 4} ⊆ (0...5)
222		sseq1 3991	. . . . . . . . . 10 ⊢ (𝑒 = {3, 4} → (𝑒 ⊆ (0...5) ↔ {3, 4} ⊆ (0...5)))
223	5, 222	ralsn 4663	. . . . . . . . 9 ⊢ (∀𝑒 ∈ {{3, 4}}𝑒 ⊆ (0...5) ↔ {3, 4} ⊆ (0...5))
224	221, 223	mpbir 231	. . . . . . . 8 ⊢ ∀𝑒 ∈ {{3, 4}}𝑒 ⊆ (0...5)
225		ralunb 4179	. . . . . . . 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 11780	. . . . . . . . . 10 ⊢ 5 ≤ 5
228		elfz2nn0 13641	. . . . . . . . . 10 ⊢ (5 ∈ (0...5) ↔ (5 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 5 ≤ 5))
229	43, 43, 227, 228	mpbir3an 1341	. . . . . . . . 9 ⊢ 5 ∈ (0...5)
230		prssi 4803	. . . . . . . . 9 ⊢ ((4 ∈ (0...5) ∧ 5 ∈ (0...5)) → {4, 5} ⊆ (0...5))
231	219, 229, 230	mp2an 692	. . . . . . . 8 ⊢ {4, 5} ⊆ (0...5)
232		prssi 4803	. . . . . . . . 9 ⊢ ((0 ∈ (0...5) ∧ 3 ∈ (0...5)) → {0, 3} ⊆ (0...5))
233	195, 209, 232	mp2an 692	. . . . . . . 8 ⊢ {0, 3} ⊆ (0...5)
234		prssi 4803	. . . . . . . . 9 ⊢ ((0 ∈ (0...5) ∧ 5 ∈ (0...5)) → {0, 5} ⊆ (0...5))
235	195, 229, 234	mp2an 692	. . . . . . . 8 ⊢ {0, 5} ⊆ (0...5)
236		sseq1 3991	. . . . . . . . 9 ⊢ (𝑒 = {4, 5} → (𝑒 ⊆ (0...5) ↔ {4, 5} ⊆ (0...5)))
237		sseq1 3991	. . . . . . . . 9 ⊢ (𝑒 = {0, 3} → (𝑒 ⊆ (0...5) ↔ {0, 3} ⊆ (0...5)))
238		sseq1 3991	. . . . . . . . 9 ⊢ (𝑒 = {0, 5} → (𝑒 ⊆ (0...5) ↔ {0, 5} ⊆ (0...5)))
239	6, 7, 8, 236, 237, 238	raltp 4687	. . . . . . . 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 4179	. . . . . . 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 5083	. . . . . 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 4598	. . . . 5 ⊢ 𝒫 𝑉 = 𝒫 (0...5)
247	244, 246	sseqtrri 4015	. . . 4 ⊢ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ 𝒫 𝑉
248		prhash2ex 14421	. . . . . . 7 ⊢ (♯‘{0, 1}) = 2
249		1ex 11240	. . . . . . . . 9 ⊢ 1 ∈ V
250		2ex 12326	. . . . . . . . 9 ⊢ 2 ∈ V
251	249, 250, 73	3pm3.2i 1339	. . . . . . . 8 ⊢ (1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2)
252		hashprb 14419	. . . . . . . 8 ⊢ ((1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2) ↔ (♯‘{1, 2}) = 2)
253	251, 252	mpbi 230	. . . . . . 7 ⊢ (♯‘{1, 2}) = 2
254		3ex 12331	. . . . . . . . 9 ⊢ 3 ∈ V
255	250, 254, 104	3pm3.2i 1339	. . . . . . . 8 ⊢ (2 ∈ V ∧ 3 ∈ V ∧ 2 ≠ 3)
256		hashprb 14419	. . . . . . . 8 ⊢ ((2 ∈ V ∧ 3 ∈ V ∧ 2 ≠ 3) ↔ (♯‘{2, 3}) = 2)
257	255, 256	mpbi 230	. . . . . . 7 ⊢ (♯‘{2, 3}) = 2
258		fveqeq2 6896	. . . . . . . 8 ⊢ (𝑒 = {0, 1} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 1}) = 2))
259		fveqeq2 6896	. . . . . . . 8 ⊢ (𝑒 = {1, 2} → ((♯‘𝑒) = 2 ↔ (♯‘{1, 2}) = 2))
260		fveqeq2 6896	. . . . . . . 8 ⊢ (𝑒 = {2, 3} → ((♯‘𝑒) = 2 ↔ (♯‘{2, 3}) = 2))
261	1, 2, 3, 258, 259, 260	raltp 4687	. . . . . . 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 3487	. . . . . . . . 9 ⊢ 4 ∈ V
264	254, 263, 135	3pm3.2i 1339	. . . . . . . 8 ⊢ (3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4)
265		hashprb 14419	. . . . . . . 8 ⊢ ((3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4) ↔ (♯‘{3, 4}) = 2)
266	264, 265	mpbi 230	. . . . . . 7 ⊢ (♯‘{3, 4}) = 2
267		fveqeq2 6896	. . . . . . . 8 ⊢ (𝑒 = {3, 4} → ((♯‘𝑒) = 2 ↔ (♯‘{3, 4}) = 2))
268	5, 267	ralsn 4663	. . . . . . 7 ⊢ (∀𝑒 ∈ {{3, 4}} (♯‘𝑒) = 2 ↔ (♯‘{3, 4}) = 2)
269	266, 268	mpbir 231	. . . . . 6 ⊢ ∀𝑒 ∈ {{3, 4}} (♯‘𝑒) = 2
270		ralunb 4179	. . . . . 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 3487	. . . . . . . 8 ⊢ 5 ∈ V
273	263, 272, 163	3pm3.2i 1339	. . . . . . 7 ⊢ (4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5)
274		hashprb 14419	. . . . . . 7 ⊢ ((4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5) ↔ (♯‘{4, 5}) = 2)
275	273, 274	mpbi 230	. . . . . 6 ⊢ (♯‘{4, 5}) = 2
276		c0ex 11238	. . . . . . . 8 ⊢ 0 ∈ V
277	276, 254, 28	3pm3.2i 1339	. . . . . . 7 ⊢ (0 ∈ V ∧ 3 ∈ V ∧ 0 ≠ 3)
278		hashprb 14419	. . . . . . 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 14419	. . . . . . 7 ⊢ ((0 ∈ V ∧ 5 ∈ V ∧ 0 ≠ 5) ↔ (♯‘{0, 5}) = 2)
282	280, 281	mpbi 230	. . . . . 6 ⊢ (♯‘{0, 5}) = 2
283		fveqeq2 6896	. . . . . . 7 ⊢ (𝑒 = {4, 5} → ((♯‘𝑒) = 2 ↔ (♯‘{4, 5}) = 2))
284		fveqeq2 6896	. . . . . . 7 ⊢ (𝑒 = {0, 3} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 3}) = 2))
285		fveqeq2 6896	. . . . . . 7 ⊢ (𝑒 = {0, 5} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 5}) = 2))
286	6, 7, 8, 283, 284, 285	raltp 4687	. . . . . 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 4179	. . . . 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 4055	. . . 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 6790	. . 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 1539 ∈ wcel 2107 ≠ wne 2931 ∀wral 3050 {crab 3420 Vcvv 3464 ∪ cun 3931 ⊆ wss 3933 𝒫 cpw 4582 {csn 4608 {cpr 4610 {ctp 4612 class class class wbr 5125 dom cdm 5667 –1-1→wf1 6539 –1-1-onto→wf1o 6541 ‘cfv 6542 (class class class)co 7414 0cc0 11138 1c1 11139 ≤ cle 11279 2c2 12304 3c3 12305 4c4 12306 5c5 12307 7c7 12309 ℕ₀cn0 12510 ...cfz 13530 ..^cfzo 13677 ♯chash 14352 Word cword 14535 ⟨“cs7 14868

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 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 2706 ax-rep 5261 ax-sep 5278 ax-nul 5288 ax-pow 5347 ax-pr 5414 ax-un 7738 ax-cnex 11194 ax-resscn 11195 ax-1cn 11196 ax-icn 11197 ax-addcl 11198 ax-addrcl 11199 ax-mulcl 11200 ax-mulrcl 11201 ax-mulcom 11202 ax-addass 11203 ax-mulass 11204 ax-distr 11205 ax-i2m1 11206 ax-1ne0 11207 ax-1rid 11208 ax-rnegex 11209 ax-rrecex 11210 ax-cnre 11211 ax-pre-lttri 11212 ax-pre-lttrn 11213 ax-pre-ltadd 11214 ax-pre-mulgt0 11215

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3773 df-csb 3882 df-dif 3936 df-un 3938 df-in 3940 df-ss 3950 df-pss 3953 df-nul 4316 df-if 4508 df-pw 4584 df-sn 4609 df-pr 4611 df-tp 4613 df-op 4615 df-uni 4890 df-int 4929 df-iun 4975 df-br 5126 df-opab 5188 df-mpt 5208 df-tr 5242 df-id 5560 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5673 df-rel 5674 df-cnv 5675 df-co 5676 df-dm 5677 df-rn 5678 df-res 5679 df-ima 5680 df-pred 6303 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6495 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7871 df-1st 7997 df-2nd 7998 df-frecs 8289 df-wrecs 8320 df-recs 8394 df-rdg 8433 df-1o 8489 df-2o 8490 df-oadd 8493 df-er 8728 df-en 8969 df-dom 8970 df-sdom 8971 df-fin 8972 df-dju 9924 df-card 9962 df-pnf 11280 df-mnf 11281 df-xr 11282 df-ltxr 11283 df-le 11284 df-sub 11477 df-neg 11478 df-nn 12250 df-2 12312 df-3 12313 df-4 12314 df-5 12315 df-6 12316 df-7 12317 df-n0 12511 df-xnn0 12584 df-z 12598 df-uz 12862 df-fz 13531 df-fzo 13678 df-hash 14353 df-word 14536 df-concat 14592 df-s1 14617 df-s2 14870 df-s3 14871 df-s4 14872 df-s5 14873 df-s6 14874 df-s7 14875

This theorem is referenced by: usgrexmpl2 47932

W3C validator