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 47761

Description: Lemma for usgrexmpl2 47762. (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 5455	. . . . 5 ⊢ {0, 1} ∈ V
2		prex 5455	. . . . 5 ⊢ {1, 2} ∈ V
3		prex 5455	. . . . 5 ⊢ {2, 3} ∈ V
4	1, 2, 3	3pm3.2i 1339	. . . 4 ⊢ ({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V)
5		prex 5455	. . . 4 ⊢ {3, 4} ∈ V
6		prex 5455	. . . . 5 ⊢ {4, 5} ∈ V
7		prex 5455	. . . . 5 ⊢ {0, 3} ∈ V
8		prex 5455	. . . . 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 12564	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
12		1nn0 12565	. . . . . . . . . 10 ⊢ 1 ∈ ℕ₀
13	11, 12	pm3.2i 470	. . . . . . . . 9 ⊢ (0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀)
14		2nn0 12566	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
15	12, 14	pm3.2i 470	. . . . . . . . 9 ⊢ (1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀)
16	13, 15	pm3.2i 470	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀))
17		0ne1 12360	. . . . . . . . . 10 ⊢ 0 ≠ 1
18		0ne2 12496	. . . . . . . . . 10 ⊢ 0 ≠ 2
19	17, 18	pm3.2i 470	. . . . . . . . 9 ⊢ (0 ≠ 1 ∧ 0 ≠ 2)
20	19	orci 864	. . . . . . . 8 ⊢ ((0 ≠ 1 ∧ 0 ≠ 2) ∨ (1 ≠ 1 ∧ 1 ≠ 2))
21		prneimg 4879	. . . . . . . 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 12567	. . . . . . . . . 10 ⊢ 3 ∈ ℕ₀
24	14, 23	pm3.2i 470	. . . . . . . . 9 ⊢ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀)
25	13, 24	pm3.2i 470	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀))
26		0re 11288	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
27		3pos 12394	. . . . . . . . . . 11 ⊢ 0 < 3
28	26, 27	ltneii 11399	. . . . . . . . . 10 ⊢ 0 ≠ 3
29	18, 28	pm3.2i 470	. . . . . . . . 9 ⊢ (0 ≠ 2 ∧ 0 ≠ 3)
30	29	orci 864	. . . . . . . 8 ⊢ ((0 ≠ 2 ∧ 0 ≠ 3) ∨ (1 ≠ 2 ∧ 1 ≠ 3))
31		prneimg 4879	. . . . . . . 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 12568	. . . . . . . . . 10 ⊢ 4 ∈ ℕ₀
34	23, 33	pm3.2i 470	. . . . . . . . 9 ⊢ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀)
35	13, 34	pm3.2i 470	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀))
36		4pos 12396	. . . . . . . . . . 11 ⊢ 0 < 4
37	26, 36	ltneii 11399	. . . . . . . . . 10 ⊢ 0 ≠ 4
38	28, 37	pm3.2i 470	. . . . . . . . 9 ⊢ (0 ≠ 3 ∧ 0 ≠ 4)
39	38	orci 864	. . . . . . . 8 ⊢ ((0 ≠ 3 ∧ 0 ≠ 4) ∨ (1 ≠ 3 ∧ 1 ≠ 4))
40		prneimg 4879	. . . . . . . 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 12569	. . . . . . . . . 10 ⊢ 5 ∈ ℕ₀
44	33, 43	pm3.2i 470	. . . . . . . . 9 ⊢ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀)
45	13, 44	pm3.2i 470	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
46		5pos 12398	. . . . . . . . . . 11 ⊢ 0 < 5
47	26, 46	ltneii 11399	. . . . . . . . . 10 ⊢ 0 ≠ 5
48	37, 47	pm3.2i 470	. . . . . . . . 9 ⊢ (0 ≠ 4 ∧ 0 ≠ 5)
49	48	orci 864	. . . . . . . 8 ⊢ ((0 ≠ 4 ∧ 0 ≠ 5) ∨ (1 ≠ 4 ∧ 1 ≠ 5))
50		prneimg 4879	. . . . . . . 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 11249	. . . . . . . . . 10 ⊢ 1 ≠ 0
55		1re 11286	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
56		1lt3 12462	. . . . . . . . . . 11 ⊢ 1 < 3
57	55, 56	ltneii 11399	. . . . . . . . . 10 ⊢ 1 ≠ 3
58	54, 57	pm3.2i 470	. . . . . . . . 9 ⊢ (1 ≠ 0 ∧ 1 ≠ 3)
59	58	olci 865	. . . . . . . 8 ⊢ ((0 ≠ 0 ∧ 0 ≠ 3) ∨ (1 ≠ 0 ∧ 1 ≠ 3))
60		prneimg 4879	. . . . . . . 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 12469	. . . . . . . . . . 11 ⊢ 1 < 5
65	55, 64	ltneii 11399	. . . . . . . . . 10 ⊢ 1 ≠ 5
66	54, 65	pm3.2i 470	. . . . . . . . 9 ⊢ (1 ≠ 0 ∧ 1 ≠ 5)
67	66	olci 865	. . . . . . . 8 ⊢ ((0 ≠ 0 ∧ 0 ≠ 5) ∨ (1 ≠ 0 ∧ 1 ≠ 5))
68		prneimg 4879	. . . . . . . 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 12497	. . . . . . . . . 10 ⊢ 1 ≠ 2
74	73, 57	pm3.2i 470	. . . . . . . . 9 ⊢ (1 ≠ 2 ∧ 1 ≠ 3)
75	74	orci 864	. . . . . . . 8 ⊢ ((1 ≠ 2 ∧ 1 ≠ 3) ∨ (2 ≠ 2 ∧ 2 ≠ 3))
76		prneimg 4879	. . . . . . . 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 12465	. . . . . . . . . . 11 ⊢ 1 < 4
80	55, 79	ltneii 11399	. . . . . . . . . 10 ⊢ 1 ≠ 4
81	57, 80	pm3.2i 470	. . . . . . . . 9 ⊢ (1 ≠ 3 ∧ 1 ≠ 4)
82	81	orci 864	. . . . . . . 8 ⊢ ((1 ≠ 3 ∧ 1 ≠ 4) ∨ (2 ≠ 3 ∧ 2 ≠ 4))
83		prneimg 4879	. . . . . . . 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 864	. . . . . . . 8 ⊢ ((1 ≠ 4 ∧ 1 ≠ 5) ∨ (2 ≠ 4 ∧ 2 ≠ 5))
89		prneimg 4879	. . . . . . . 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 864	. . . . . . . 8 ⊢ ((1 ≠ 0 ∧ 1 ≠ 3) ∨ (2 ≠ 0 ∧ 2 ≠ 3))
93		prneimg 4879	. . . . . . . 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 864	. . . . . . . 8 ⊢ ((1 ≠ 0 ∧ 1 ≠ 5) ∨ (2 ≠ 0 ∧ 2 ≠ 5))
97		prneimg 4879	. . . . . . . 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 12363	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
103		2lt3 12461	. . . . . . . . . 10 ⊢ 2 < 3
104	102, 103	ltneii 11399	. . . . . . . . 9 ⊢ 2 ≠ 3
105		2lt4 12464	. . . . . . . . . 10 ⊢ 2 < 4
106	102, 105	ltneii 11399	. . . . . . . . 9 ⊢ 2 ≠ 4
107	104, 106	pm3.2i 470	. . . . . . . 8 ⊢ (2 ≠ 3 ∧ 2 ≠ 4)
108	107	orci 864	. . . . . . 7 ⊢ ((2 ≠ 3 ∧ 2 ≠ 4) ∨ (3 ≠ 3 ∧ 3 ≠ 4))
109		prneimg 4879	. . . . . . 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 12468	. . . . . . . . . . 11 ⊢ 2 < 5
113	102, 112	ltneii 11399	. . . . . . . . . 10 ⊢ 2 ≠ 5
114	106, 113	pm3.2i 470	. . . . . . . . 9 ⊢ (2 ≠ 4 ∧ 2 ≠ 5)
115	114	orci 864	. . . . . . . 8 ⊢ ((2 ≠ 4 ∧ 2 ≠ 5) ∨ (3 ≠ 4 ∧ 3 ≠ 5))
116		prneimg 4879	. . . . . . . 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 12393	. . . . . . . . . 10 ⊢ 2 ≠ 0
120	119, 104	pm3.2i 470	. . . . . . . . 9 ⊢ (2 ≠ 0 ∧ 2 ≠ 3)
121	120	orci 864	. . . . . . . 8 ⊢ ((2 ≠ 0 ∧ 2 ≠ 3) ∨ (3 ≠ 0 ∧ 3 ≠ 3))
122		prneimg 4879	. . . . . . . 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 864	. . . . . . . 8 ⊢ ((2 ≠ 0 ∧ 2 ≠ 5) ∨ (3 ≠ 0 ∧ 3 ≠ 5))
127		prneimg 4879	. . . . . . . 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 12369	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
134		3lt4 12463	. . . . . . . . . 10 ⊢ 3 < 4
135	133, 134	ltneii 11399	. . . . . . . . 9 ⊢ 3 ≠ 4
136		3lt5 12467	. . . . . . . . . 10 ⊢ 3 < 5
137	133, 136	ltneii 11399	. . . . . . . . 9 ⊢ 3 ≠ 5
138	135, 137	pm3.2i 470	. . . . . . . 8 ⊢ (3 ≠ 4 ∧ 3 ≠ 5)
139	138	orci 864	. . . . . . 7 ⊢ ((3 ≠ 4 ∧ 3 ≠ 5) ∨ (4 ≠ 4 ∧ 4 ≠ 5))
140		prneimg 4879	. . . . . . 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 12397	. . . . . . . . 9 ⊢ 4 ≠ 0
144	135	necomi 2997	. . . . . . . . 9 ⊢ 4 ≠ 3
145	143, 144	pm3.2i 470	. . . . . . . 8 ⊢ (4 ≠ 0 ∧ 4 ≠ 3)
146	145	olci 865	. . . . . . 7 ⊢ ((3 ≠ 0 ∧ 3 ≠ 3) ∨ (4 ≠ 0 ∧ 4 ≠ 3))
147		prneimg 4879	. . . . . . 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 12395	. . . . . . . . 9 ⊢ 3 ≠ 0
151	150, 137	pm3.2i 470	. . . . . . . 8 ⊢ (3 ≠ 0 ∧ 3 ≠ 5)
152	151	orci 864	. . . . . . 7 ⊢ ((3 ≠ 0 ∧ 3 ≠ 5) ∨ (4 ≠ 0 ∧ 4 ≠ 5))
153		prneimg 4879	. . . . . . 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 864	. . . . . . 7 ⊢ ((4 ≠ 0 ∧ 4 ≠ 3) ∨ (5 ≠ 0 ∧ 5 ≠ 3))
158		prneimg 4879	. . . . . . 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 12373	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
162		4lt5 12466	. . . . . . . . . 10 ⊢ 4 < 5
163	161, 162	ltneii 11399	. . . . . . . . 9 ⊢ 4 ≠ 5
164	143, 163	pm3.2i 470	. . . . . . . 8 ⊢ (4 ≠ 0 ∧ 4 ≠ 5)
165	164	orci 864	. . . . . . 7 ⊢ ((4 ≠ 0 ∧ 4 ≠ 5) ∨ (5 ≠ 0 ∧ 5 ≠ 5))
166		prneimg 4879	. . . . . . 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 865	. . . . . . 7 ⊢ ((0 ≠ 0 ∧ 0 ≠ 5) ∨ (3 ≠ 0 ∧ 3 ≠ 5))
170		prneimg 4879	. . . . . . 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 15011	. . . . . . 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 14947	. . . . . . . 8 ⊢ (♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩) = 7
180	179	oveq2i 7456	. . . . . . 7 ⊢ (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩)) = (0..^7)
181		f1oeq2 6850	. . . . . . 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 5928	. . . . . . 7 ⊢ dom 𝐸 = dom ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩
185		s7cli 14930	. . . . . . . 8 ⊢ ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩ ∈ Word V
186		wrddm 14565	. . . . . . . 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 2762	. . . . . 6 ⊢ dom 𝐸 = (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))
189		f1oeq2 6850	. . . . . 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 6860	. . . 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 13677	. . . . . . . . . . 11 ⊢ (5 ∈ ℕ₀ → 0 ∈ (0...5))
195	43, 194	ax-mp 5	. . . . . . . . . 10 ⊢ 0 ∈ (0...5)
196		5re 12376	. . . . . . . . . . . 12 ⊢ 5 ∈ ℝ
197	55, 196, 64	ltleii 11409	. . . . . . . . . . 11 ⊢ 1 ≤ 5
198		elfz2nn0 13671	. . . . . . . . . . 11 ⊢ (1 ∈ (0...5) ↔ (1 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 1 ≤ 5))
199	12, 43, 197, 198	mpbir3an 1341	. . . . . . . . . 10 ⊢ 1 ∈ (0...5)
200		prssi 4846	. . . . . . . . . 10 ⊢ ((0 ∈ (0...5) ∧ 1 ∈ (0...5)) → {0, 1} ⊆ (0...5))
201	195, 199, 200	mp2an 691	. . . . . . . . 9 ⊢ {0, 1} ⊆ (0...5)
202	102, 196, 112	ltleii 11409	. . . . . . . . . . 11 ⊢ 2 ≤ 5
203		elfz2nn0 13671	. . . . . . . . . . 11 ⊢ (2 ∈ (0...5) ↔ (2 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 2 ≤ 5))
204	14, 43, 202, 203	mpbir3an 1341	. . . . . . . . . 10 ⊢ 2 ∈ (0...5)
205		prssi 4846	. . . . . . . . . 10 ⊢ ((1 ∈ (0...5) ∧ 2 ∈ (0...5)) → {1, 2} ⊆ (0...5))
206	199, 204, 205	mp2an 691	. . . . . . . . 9 ⊢ {1, 2} ⊆ (0...5)
207	133, 196, 136	ltleii 11409	. . . . . . . . . . 11 ⊢ 3 ≤ 5
208		elfz2nn0 13671	. . . . . . . . . . 11 ⊢ (3 ∈ (0...5) ↔ (3 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 3 ≤ 5))
209	23, 43, 207, 208	mpbir3an 1341	. . . . . . . . . 10 ⊢ 3 ∈ (0...5)
210		prssi 4846	. . . . . . . . . 10 ⊢ ((2 ∈ (0...5) ∧ 3 ∈ (0...5)) → {2, 3} ⊆ (0...5))
211	204, 209, 210	mp2an 691	. . . . . . . . 9 ⊢ {2, 3} ⊆ (0...5)
212		sseq1 4028	. . . . . . . . . 10 ⊢ (𝑒 = {0, 1} → (𝑒 ⊆ (0...5) ↔ {0, 1} ⊆ (0...5)))
213		sseq1 4028	. . . . . . . . . 10 ⊢ (𝑒 = {1, 2} → (𝑒 ⊆ (0...5) ↔ {1, 2} ⊆ (0...5)))
214		sseq1 4028	. . . . . . . . . 10 ⊢ (𝑒 = {2, 3} → (𝑒 ⊆ (0...5) ↔ {2, 3} ⊆ (0...5)))
215	1, 2, 3, 212, 213, 214	raltp 4730	. . . . . . . . 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 11409	. . . . . . . . . . 11 ⊢ 4 ≤ 5
218		elfz2nn0 13671	. . . . . . . . . . 11 ⊢ (4 ∈ (0...5) ↔ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 4 ≤ 5))
219	33, 43, 217, 218	mpbir3an 1341	. . . . . . . . . 10 ⊢ 4 ∈ (0...5)
220		prssi 4846	. . . . . . . . . 10 ⊢ ((3 ∈ (0...5) ∧ 4 ∈ (0...5)) → {3, 4} ⊆ (0...5))
221	209, 219, 220	mp2an 691	. . . . . . . . 9 ⊢ {3, 4} ⊆ (0...5)
222		sseq1 4028	. . . . . . . . . 10 ⊢ (𝑒 = {3, 4} → (𝑒 ⊆ (0...5) ↔ {3, 4} ⊆ (0...5)))
223	5, 222	ralsn 4705	. . . . . . . . 9 ⊢ (∀𝑒 ∈ {{3, 4}}𝑒 ⊆ (0...5) ↔ {3, 4} ⊆ (0...5))
224	221, 223	mpbir 231	. . . . . . . 8 ⊢ ∀𝑒 ∈ {{3, 4}}𝑒 ⊆ (0...5)
225		ralunb 4214	. . . . . . . 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 710	. . . . . . 7 ⊢ ∀𝑒 ∈ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}})𝑒 ⊆ (0...5)
227	196	leidi 11820	. . . . . . . . . 10 ⊢ 5 ≤ 5
228		elfz2nn0 13671	. . . . . . . . . 10 ⊢ (5 ∈ (0...5) ↔ (5 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 5 ≤ 5))
229	43, 43, 227, 228	mpbir3an 1341	. . . . . . . . 9 ⊢ 5 ∈ (0...5)
230		prssi 4846	. . . . . . . . 9 ⊢ ((4 ∈ (0...5) ∧ 5 ∈ (0...5)) → {4, 5} ⊆ (0...5))
231	219, 229, 230	mp2an 691	. . . . . . . 8 ⊢ {4, 5} ⊆ (0...5)
232		prssi 4846	. . . . . . . . 9 ⊢ ((0 ∈ (0...5) ∧ 3 ∈ (0...5)) → {0, 3} ⊆ (0...5))
233	195, 209, 232	mp2an 691	. . . . . . . 8 ⊢ {0, 3} ⊆ (0...5)
234		prssi 4846	. . . . . . . . 9 ⊢ ((0 ∈ (0...5) ∧ 5 ∈ (0...5)) → {0, 5} ⊆ (0...5))
235	195, 229, 234	mp2an 691	. . . . . . . 8 ⊢ {0, 5} ⊆ (0...5)
236		sseq1 4028	. . . . . . . . 9 ⊢ (𝑒 = {4, 5} → (𝑒 ⊆ (0...5) ↔ {4, 5} ⊆ (0...5)))
237		sseq1 4028	. . . . . . . . 9 ⊢ (𝑒 = {0, 3} → (𝑒 ⊆ (0...5) ↔ {0, 3} ⊆ (0...5)))
238		sseq1 4028	. . . . . . . . 9 ⊢ (𝑒 = {0, 5} → (𝑒 ⊆ (0...5) ↔ {0, 5} ⊆ (0...5)))
239	6, 7, 8, 236, 237, 238	raltp 4730	. . . . . . . 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 4214	. . . . . . 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 710	. . . . . 6 ⊢ ∀𝑒 ∈ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})𝑒 ⊆ (0...5)
243		pwssb 5127	. . . . . 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 4638	. . . . 5 ⊢ 𝒫 𝑉 = 𝒫 (0...5)
247	244, 246	sseqtrri 4040	. . . 4 ⊢ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ 𝒫 𝑉
248		prhash2ex 14444	. . . . . . 7 ⊢ (♯‘{0, 1}) = 2
249		1ex 11282	. . . . . . . . 9 ⊢ 1 ∈ V
250		2ex 12366	. . . . . . . . 9 ⊢ 2 ∈ V
251	249, 250, 73	3pm3.2i 1339	. . . . . . . 8 ⊢ (1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2)
252		hashprb 14442	. . . . . . . 8 ⊢ ((1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2) ↔ (♯‘{1, 2}) = 2)
253	251, 252	mpbi 230	. . . . . . 7 ⊢ (♯‘{1, 2}) = 2
254		3ex 12371	. . . . . . . . 9 ⊢ 3 ∈ V
255	250, 254, 104	3pm3.2i 1339	. . . . . . . 8 ⊢ (2 ∈ V ∧ 3 ∈ V ∧ 2 ≠ 3)
256		hashprb 14442	. . . . . . . 8 ⊢ ((2 ∈ V ∧ 3 ∈ V ∧ 2 ≠ 3) ↔ (♯‘{2, 3}) = 2)
257	255, 256	mpbi 230	. . . . . . 7 ⊢ (♯‘{2, 3}) = 2
258		fveqeq2 6928	. . . . . . . 8 ⊢ (𝑒 = {0, 1} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 1}) = 2))
259		fveqeq2 6928	. . . . . . . 8 ⊢ (𝑒 = {1, 2} → ((♯‘𝑒) = 2 ↔ (♯‘{1, 2}) = 2))
260		fveqeq2 6928	. . . . . . . 8 ⊢ (𝑒 = {2, 3} → ((♯‘𝑒) = 2 ↔ (♯‘{2, 3}) = 2))
261	1, 2, 3, 258, 259, 260	raltp 4730	. . . . . . 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 3506	. . . . . . . . 9 ⊢ 4 ∈ V
264	254, 263, 135	3pm3.2i 1339	. . . . . . . 8 ⊢ (3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4)
265		hashprb 14442	. . . . . . . 8 ⊢ ((3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4) ↔ (♯‘{3, 4}) = 2)
266	264, 265	mpbi 230	. . . . . . 7 ⊢ (♯‘{3, 4}) = 2
267		fveqeq2 6928	. . . . . . . 8 ⊢ (𝑒 = {3, 4} → ((♯‘𝑒) = 2 ↔ (♯‘{3, 4}) = 2))
268	5, 267	ralsn 4705	. . . . . . 7 ⊢ (∀𝑒 ∈ {{3, 4}} (♯‘𝑒) = 2 ↔ (♯‘{3, 4}) = 2)
269	266, 268	mpbir 231	. . . . . 6 ⊢ ∀𝑒 ∈ {{3, 4}} (♯‘𝑒) = 2
270		ralunb 4214	. . . . . 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 710	. . . . 5 ⊢ ∀𝑒 ∈ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}})(♯‘𝑒) = 2
272	43	elexi 3506	. . . . . . . 8 ⊢ 5 ∈ V
273	263, 272, 163	3pm3.2i 1339	. . . . . . 7 ⊢ (4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5)
274		hashprb 14442	. . . . . . 7 ⊢ ((4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5) ↔ (♯‘{4, 5}) = 2)
275	273, 274	mpbi 230	. . . . . 6 ⊢ (♯‘{4, 5}) = 2
276		c0ex 11280	. . . . . . . 8 ⊢ 0 ∈ V
277	276, 254, 28	3pm3.2i 1339	. . . . . . 7 ⊢ (0 ∈ V ∧ 3 ∈ V ∧ 0 ≠ 3)
278		hashprb 14442	. . . . . . 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 14442	. . . . . . 7 ⊢ ((0 ∈ V ∧ 5 ∈ V ∧ 0 ≠ 5) ↔ (♯‘{0, 5}) = 2)
282	280, 281	mpbi 230	. . . . . 6 ⊢ (♯‘{0, 5}) = 2
283		fveqeq2 6928	. . . . . . 7 ⊢ (𝑒 = {4, 5} → ((♯‘𝑒) = 2 ↔ (♯‘{4, 5}) = 2))
284		fveqeq2 6928	. . . . . . 7 ⊢ (𝑒 = {0, 3} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 3}) = 2))
285		fveqeq2 6928	. . . . . . 7 ⊢ (𝑒 = {0, 5} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 5}) = 2))
286	6, 7, 8, 283, 284, 285	raltp 4730	. . . . . 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 4214	. . . . 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 710	. . . 4 ⊢ ∀𝑒 ∈ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})(♯‘𝑒) = 2
290		ssrab 4090	. . . 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 710	. . 3 ⊢ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}
292		f1ss 6821	. . 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 585	. 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 691	1 ⊢ 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 ∧ wa 395 ∨ wo 846 ∧ w3a 1087 = wceq 1537 ∈ wcel 2103 ≠ wne 2942 ∀wral 3063 {crab 3438 Vcvv 3482 ∪ cun 3968 ⊆ wss 3970 𝒫 cpw 4622 {csn 4648 {cpr 4650 {ctp 4652 class class class wbr 5169 dom cdm 5699 –1-1→wf1 6569 –1-1-onto→wf1o 6571 ‘cfv 6572 (class class class)co 7445 0cc0 11180 1c1 11181 ≤ cle 11321 2c2 12344 3c3 12345 4c4 12346 5c5 12347 7c7 12349 ℕ₀cn0 12549 ...cfz 13563 ..^cfzo 13707 ♯chash 14375 Word cword 14558 ⟨“cs7 14891

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 1967 ax-7 2007 ax-8 2105 ax-9 2113 ax-10 2136 ax-11 2153 ax-12 2173 ax-ext 2705 ax-rep 5306 ax-sep 5320 ax-nul 5327 ax-pow 5386 ax-pr 5450 ax-un 7766 ax-cnex 11236 ax-resscn 11237 ax-1cn 11238 ax-icn 11239 ax-addcl 11240 ax-addrcl 11241 ax-mulcl 11242 ax-mulrcl 11243 ax-mulcom 11244 ax-addass 11245 ax-mulass 11246 ax-distr 11247 ax-i2m1 11248 ax-1ne0 11249 ax-1rid 11250 ax-rnegex 11251 ax-rrecex 11252 ax-cnre 11253 ax-pre-lttri 11254 ax-pre-lttrn 11255 ax-pre-ltadd 11256 ax-pre-mulgt0 11257

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2890 df-ne 2943 df-nel 3049 df-ral 3064 df-rex 3073 df-reu 3384 df-rab 3439 df-v 3484 df-sbc 3799 df-csb 3916 df-dif 3973 df-un 3975 df-in 3977 df-ss 3987 df-pss 3990 df-nul 4348 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-int 4973 df-iun 5021 df-br 5170 df-opab 5232 df-mpt 5253 df-tr 5287 df-id 5597 df-eprel 5603 df-po 5611 df-so 5612 df-fr 5654 df-we 5656 df-xp 5705 df-rel 5706 df-cnv 5707 df-co 5708 df-dm 5709 df-rn 5710 df-res 5711 df-ima 5712 df-pred 6331 df-ord 6397 df-on 6398 df-lim 6399 df-suc 6400 df-iota 6524 df-fun 6574 df-fn 6575 df-f 6576 df-f1 6577 df-fo 6578 df-f1o 6579 df-fv 6580 df-riota 7401 df-ov 7448 df-oprab 7449 df-mpo 7450 df-om 7900 df-1st 8026 df-2nd 8027 df-frecs 8318 df-wrecs 8349 df-recs 8423 df-rdg 8462 df-1o 8518 df-2o 8519 df-oadd 8522 df-er 8759 df-en 9000 df-dom 9001 df-sdom 9002 df-fin 9003 df-dju 9966 df-card 10004 df-pnf 11322 df-mnf 11323 df-xr 11324 df-ltxr 11325 df-le 11326 df-sub 11518 df-neg 11519 df-nn 12290 df-2 12352 df-3 12353 df-4 12354 df-5 12355 df-6 12356 df-7 12357 df-n0 12550 df-xnn0 12622 df-z 12636 df-uz 12900 df-fz 13564 df-fzo 13708 df-hash 14376 df-word 14559 df-concat 14615 df-s1 14640 df-s2 14893 df-s3 14894 df-s4 14895 df-s5 14896 df-s6 14897 df-s7 14898

This theorem is referenced by: usgrexmpl2 47762

W3C validator