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 49217

Description: Lemma for usgrexmpl2 49218. (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 5395	. . . . 5 ⊢ {0, 1} ∈ V
2		prex 5395	. . . . 5 ⊢ {1, 2} ∈ V
3		prex 5395	. . . . 5 ⊢ {2, 3} ∈ V
4	1, 2, 3	3pm3.2i 1358	. . . 4 ⊢ ({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V)
5		prex 5395	. . . 4 ⊢ {3, 4} ∈ V
6		prex 5395	. . . . 5 ⊢ {4, 5} ∈ V
7		prex 5395	. . . . 5 ⊢ {0, 3} ∈ V
8		prex 5395	. . . . 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 12624	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
12		1nn0 12625	. . . . . . . . . 10 ⊢ 1 ∈ ℕ₀
13	11, 12	pm3.2i 476	. . . . . . . . 9 ⊢ (0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀)
14		2nn0 12626	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
15	12, 14	pm3.2i 476	. . . . . . . . 9 ⊢ (1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀)
16	13, 15	pm3.2i 476	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀))
17		0ne1 12417	. . . . . . . . . 10 ⊢ 0 ≠ 1
18		0ne2 12555	. . . . . . . . . 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 4808	. . . . . . . 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 12627	. . . . . . . . . 10 ⊢ 3 ∈ ℕ₀
24	14, 23	pm3.2i 476	. . . . . . . . 9 ⊢ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀)
25	13, 24	pm3.2i 476	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀))
26		0re 11313	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
27		3pos 12454	. . . . . . . . . . 11 ⊢ 0 < 3
28	26, 27	ltneii 11426	. . . . . . . . . 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 4808	. . . . . . . 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 12628	. . . . . . . . . 10 ⊢ 4 ∈ ℕ₀
34	23, 33	pm3.2i 476	. . . . . . . . 9 ⊢ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀)
35	13, 34	pm3.2i 476	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ₀))
36		4pos 12456	. . . . . . . . . . 11 ⊢ 0 < 4
37	26, 36	ltneii 11426	. . . . . . . . . 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 4808	. . . . . . . 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 12629	. . . . . . . . . 10 ⊢ 5 ∈ ℕ₀
44	33, 43	pm3.2i 476	. . . . . . . . 9 ⊢ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀)
45	13, 44	pm3.2i 476	. . . . . . . 8 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) ∧ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀))
46		5pos 12458	. . . . . . . . . . 11 ⊢ 0 < 5
47	26, 46	ltneii 11426	. . . . . . . . . 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 4808	. . . . . . . 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 11272	. . . . . . . . . 10 ⊢ 1 ≠ 0
55		1re 11311	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
56		1lt3 12521	. . . . . . . . . . 11 ⊢ 1 < 3
57	55, 56	ltneii 11426	. . . . . . . . . 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 4808	. . . . . . . 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 12528	. . . . . . . . . . 11 ⊢ 1 < 5
65	55, 64	ltneii 11426	. . . . . . . . . 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 4808	. . . . . . . 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 12556	. . . . . . . . . 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 4808	. . . . . . . 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 12524	. . . . . . . . . . 11 ⊢ 1 < 4
80	55, 79	ltneii 11426	. . . . . . . . . 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 4808	. . . . . . . 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 4808	. . . . . . . 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 4808	. . . . . . . 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 4808	. . . . . . . 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 12420	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
103		2lt3 12519	. . . . . . . . . 10 ⊢ 2 < 3
104	102, 103	ltneii 11426	. . . . . . . . 9 ⊢ 2 ≠ 3
105		2lt4 12523	. . . . . . . . . 10 ⊢ 2 < 4
106	102, 105	ltneii 11426	. . . . . . . . 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 4808	. . . . . . 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 12527	. . . . . . . . . . 11 ⊢ 2 < 5
113	102, 112	ltneii 11426	. . . . . . . . . 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 4808	. . . . . . . 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 12452	. . . . . . . . . 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 4808	. . . . . . . 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 4808	. . . . . . . 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 12426	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
134		3lt4 12522	. . . . . . . . . 10 ⊢ 3 < 4
135	133, 134	ltneii 11426	. . . . . . . . 9 ⊢ 3 ≠ 4
136		3lt5 12526	. . . . . . . . . 10 ⊢ 3 < 5
137	133, 136	ltneii 11426	. . . . . . . . 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 4808	. . . . . . 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 12457	. . . . . . . . 9 ⊢ 4 ≠ 0
144	135	necomi 3009	. . . . . . . . 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 4808	. . . . . . 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 12455	. . . . . . . . 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 4808	. . . . . . 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 4808	. . . . . . 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 12430	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
162		4lt5 12525	. . . . . . . . . 10 ⊢ 4 < 5
163	161, 162	ltneii 11426	. . . . . . . . 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 4808	. . . . . . 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 4808	. . . . . . 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 15124	. . . . . . 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 15058	. . . . . . . 8 ⊢ (♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩) = 7
180	179	oveq2i 7431	. . . . . . 7 ⊢ (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩)) = (0..^7)
181		f1oeq2 6813	. . . . . . 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 5885	. . . . . . 7 ⊢ dom 𝐸 = dom ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩
185		s7cli 15040	. . . . . . . 8 ⊢ ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩ ∈ Word V
186		wrddm 14669	. . . . . . . 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 2783	. . . . . 6 ⊢ dom 𝐸 = (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))
189		f1oeq2 6813	. . . . . 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 6823	. . . 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 13761	. . . . . . . . . . 11 ⊢ (5 ∈ ℕ₀ → 0 ∈ (0...5))
195	43, 194	ax-mp 5	. . . . . . . . . 10 ⊢ 0 ∈ (0...5)
196		5re 12433	. . . . . . . . . . . 12 ⊢ 5 ∈ ℝ
197	55, 196, 64	ltleii 11436	. . . . . . . . . . 11 ⊢ 1 ≤ 5
198		elfz2nn0 13755	. . . . . . . . . . 11 ⊢ (1 ∈ (0...5) ↔ (1 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 1 ≤ 5))
199	12, 43, 197, 198	mpbir3an 1360	. . . . . . . . . 10 ⊢ 1 ∈ (0...5)
200		prssi 4776	. . . . . . . . . 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 11436	. . . . . . . . . . 11 ⊢ 2 ≤ 5
203		elfz2nn0 13755	. . . . . . . . . . 11 ⊢ (2 ∈ (0...5) ↔ (2 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 2 ≤ 5))
204	14, 43, 202, 203	mpbir3an 1360	. . . . . . . . . 10 ⊢ 2 ∈ (0...5)
205		prssi 4776	. . . . . . . . . 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 11436	. . . . . . . . . . 11 ⊢ 3 ≤ 5
208		elfz2nn0 13755	. . . . . . . . . . 11 ⊢ (3 ∈ (0...5) ↔ (3 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 3 ≤ 5))
209	23, 43, 207, 208	mpbir3an 1360	. . . . . . . . . 10 ⊢ 3 ∈ (0...5)
210		prssi 4776	. . . . . . . . . 10 ⊢ ((2 ∈ (0...5) ∧ 3 ∈ (0...5)) → {2, 3} ⊆ (0...5))
211	204, 209, 210	mp2an 705	. . . . . . . . 9 ⊢ {2, 3} ⊆ (0...5)
212		sseq1 3933	. . . . . . . . . 10 ⊢ (𝑒 = {0, 1} → (𝑒 ⊆ (0...5) ↔ {0, 1} ⊆ (0...5)))
213		sseq1 3933	. . . . . . . . . 10 ⊢ (𝑒 = {1, 2} → (𝑒 ⊆ (0...5) ↔ {1, 2} ⊆ (0...5)))
214		sseq1 3933	. . . . . . . . . 10 ⊢ (𝑒 = {2, 3} → (𝑒 ⊆ (0...5) ↔ {2, 3} ⊆ (0...5)))
215	1, 2, 3, 212, 213, 214	raltp 4662	. . . . . . . . 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 11436	. . . . . . . . . . 11 ⊢ 4 ≤ 5
218		elfz2nn0 13755	. . . . . . . . . . 11 ⊢ (4 ∈ (0...5) ↔ (4 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 4 ≤ 5))
219	33, 43, 217, 218	mpbir3an 1360	. . . . . . . . . 10 ⊢ 4 ∈ (0...5)
220		prssi 4776	. . . . . . . . . 10 ⊢ ((3 ∈ (0...5) ∧ 4 ∈ (0...5)) → {3, 4} ⊆ (0...5))
221	209, 219, 220	mp2an 705	. . . . . . . . 9 ⊢ {3, 4} ⊆ (0...5)
222		sseq1 3933	. . . . . . . . . 10 ⊢ (𝑒 = {3, 4} → (𝑒 ⊆ (0...5) ↔ {3, 4} ⊆ (0...5)))
223	5, 222	ralsn 4638	. . . . . . . . 9 ⊢ (∀𝑒 ∈ {{3, 4}}𝑒 ⊆ (0...5) ↔ {3, 4} ⊆ (0...5))
224	221, 223	mpbir 234	. . . . . . . 8 ⊢ ∀𝑒 ∈ {{3, 4}}𝑒 ⊆ (0...5)
225		ralunb 4195	. . . . . . . 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 11853	. . . . . . . . . 10 ⊢ 5 ≤ 5
228		elfz2nn0 13755	. . . . . . . . . 10 ⊢ (5 ∈ (0...5) ↔ (5 ∈ ℕ₀ ∧ 5 ∈ ℕ₀ ∧ 5 ≤ 5))
229	43, 43, 227, 228	mpbir3an 1360	. . . . . . . . 9 ⊢ 5 ∈ (0...5)
230		prssi 4776	. . . . . . . . 9 ⊢ ((4 ∈ (0...5) ∧ 5 ∈ (0...5)) → {4, 5} ⊆ (0...5))
231	219, 229, 230	mp2an 705	. . . . . . . 8 ⊢ {4, 5} ⊆ (0...5)
232		prssi 4776	. . . . . . . . 9 ⊢ ((0 ∈ (0...5) ∧ 3 ∈ (0...5)) → {0, 3} ⊆ (0...5))
233	195, 209, 232	mp2an 705	. . . . . . . 8 ⊢ {0, 3} ⊆ (0...5)
234		prssi 4776	. . . . . . . . 9 ⊢ ((0 ∈ (0...5) ∧ 5 ∈ (0...5)) → {0, 5} ⊆ (0...5))
235	195, 229, 234	mp2an 705	. . . . . . . 8 ⊢ {0, 5} ⊆ (0...5)
236		sseq1 3933	. . . . . . . . 9 ⊢ (𝑒 = {4, 5} → (𝑒 ⊆ (0...5) ↔ {4, 5} ⊆ (0...5)))
237		sseq1 3933	. . . . . . . . 9 ⊢ (𝑒 = {0, 3} → (𝑒 ⊆ (0...5) ↔ {0, 3} ⊆ (0...5)))
238		sseq1 3933	. . . . . . . . 9 ⊢ (𝑒 = {0, 5} → (𝑒 ⊆ (0...5) ↔ {0, 5} ⊆ (0...5)))
239	6, 7, 8, 236, 237, 238	raltp 4662	. . . . . . . 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 4195	. . . . . . 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 5060	. . . . . 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 4572	. . . . 5 ⊢ 𝒫 𝑉 = 𝒫 (0...5)
247	244, 246	sseqtrri 3957	. . . 4 ⊢ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ 𝒫 𝑉
248		prhash2ex 14546	. . . . . . 7 ⊢ (♯‘{0, 1}) = 2
249		1ex 11306	. . . . . . . . 9 ⊢ 1 ∈ V
250		2ex 12423	. . . . . . . . 9 ⊢ 2 ∈ V
251	249, 250, 73	3pm3.2i 1358	. . . . . . . 8 ⊢ (1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2)
252		hashprb 14544	. . . . . . . 8 ⊢ ((1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2) ↔ (♯‘{1, 2}) = 2)
253	251, 252	mpbi 233	. . . . . . 7 ⊢ (♯‘{1, 2}) = 2
254		3ex 12428	. . . . . . . . 9 ⊢ 3 ∈ V
255	250, 254, 104	3pm3.2i 1358	. . . . . . . 8 ⊢ (2 ∈ V ∧ 3 ∈ V ∧ 2 ≠ 3)
256		hashprb 14544	. . . . . . . 8 ⊢ ((2 ∈ V ∧ 3 ∈ V ∧ 2 ≠ 3) ↔ (♯‘{2, 3}) = 2)
257	255, 256	mpbi 233	. . . . . . 7 ⊢ (♯‘{2, 3}) = 2
258		fveqeq2 6894	. . . . . . . 8 ⊢ (𝑒 = {0, 1} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 1}) = 2))
259		fveqeq2 6894	. . . . . . . 8 ⊢ (𝑒 = {1, 2} → ((♯‘𝑒) = 2 ↔ (♯‘{1, 2}) = 2))
260		fveqeq2 6894	. . . . . . . 8 ⊢ (𝑒 = {2, 3} → ((♯‘𝑒) = 2 ↔ (♯‘{2, 3}) = 2))
261	1, 2, 3, 258, 259, 260	raltp 4662	. . . . . . 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 3472	. . . . . . . . 9 ⊢ 4 ∈ V
264	254, 263, 135	3pm3.2i 1358	. . . . . . . 8 ⊢ (3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4)
265		hashprb 14544	. . . . . . . 8 ⊢ ((3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4) ↔ (♯‘{3, 4}) = 2)
266	264, 265	mpbi 233	. . . . . . 7 ⊢ (♯‘{3, 4}) = 2
267		fveqeq2 6894	. . . . . . . 8 ⊢ (𝑒 = {3, 4} → ((♯‘𝑒) = 2 ↔ (♯‘{3, 4}) = 2))
268	5, 267	ralsn 4638	. . . . . . 7 ⊢ (∀𝑒 ∈ {{3, 4}} (♯‘𝑒) = 2 ↔ (♯‘{3, 4}) = 2)
269	266, 268	mpbir 234	. . . . . 6 ⊢ ∀𝑒 ∈ {{3, 4}} (♯‘𝑒) = 2
270		ralunb 4195	. . . . . 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 3472	. . . . . . . 8 ⊢ 5 ∈ V
273	263, 272, 163	3pm3.2i 1358	. . . . . . 7 ⊢ (4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5)
274		hashprb 14544	. . . . . . 7 ⊢ ((4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5) ↔ (♯‘{4, 5}) = 2)
275	273, 274	mpbi 233	. . . . . 6 ⊢ (♯‘{4, 5}) = 2
276		c0ex 11303	. . . . . . . 8 ⊢ 0 ∈ V
277	276, 254, 28	3pm3.2i 1358	. . . . . . 7 ⊢ (0 ∈ V ∧ 3 ∈ V ∧ 0 ≠ 3)
278		hashprb 14544	. . . . . . 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 14544	. . . . . . 7 ⊢ ((0 ∈ V ∧ 5 ∈ V ∧ 0 ≠ 5) ↔ (♯‘{0, 5}) = 2)
282	280, 281	mpbi 233	. . . . . 6 ⊢ (♯‘{0, 5}) = 2
283		fveqeq2 6894	. . . . . . 7 ⊢ (𝑒 = {4, 5} → ((♯‘𝑒) = 2 ↔ (♯‘{4, 5}) = 2))
284		fveqeq2 6894	. . . . . . 7 ⊢ (𝑒 = {0, 3} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 3}) = 2))
285		fveqeq2 6894	. . . . . . 7 ⊢ (𝑒 = {0, 5} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 5}) = 2))
286	6, 7, 8, 283, 284, 285	raltp 4662	. . . . . 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 4195	. . . . 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 3996	. . . 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 6785	. . 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 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 {crab 3412 Vcvv 3450 ⊆ wss 3895 ∪ cun 4149 𝒫 cpw 4556 {csn 4584 {cpr 4586 {ctp 4588 class class class wbr 5102 dom cdm 5650 –1-1→wf1 6535 –1-1-onto→wf1o 6537 ‘cfv 6538 (class class class)co 7420 0cc0 11203 1c1 11204 ≤ cle 11347 2c2 12400 3c3 12401 4c4 12402 5c5 12403 7c7 12405 ℕ₀cn0 12609 ...cfz 13642 ..^cfzo 13791 ♯chash 14477 Word cword 14661 ⟨“cs7 15001

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11259 ax-resscn 11260 ax-1cn 11261 ax-icn 11262 ax-addcl 11263 ax-addrcl 11264 ax-mulcl 11265 ax-mulrcl 11266 ax-mulcom 11267 ax-addass 11268 ax-mulass 11269 ax-distr 11270 ax-i2m1 11271 ax-1ne0 11272 ax-1rid 11273 ax-rnegex 11274 ax-rrecex 11275 ax-cnre 11276 ax-pre-lttri 11277 ax-pre-lttrn 11278 ax-pre-ltadd 11279 ax-pre-mulgt0 11280

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-1o 8479 df-2o 8480 df-oadd 8483 df-er 8720 df-en 8977 df-dom 8978 df-sdom 8979 df-fin 8980 df-dju 9985 df-card 10023 df-pnf 11348 df-mnf 11349 df-xr 11350 df-ltxr 11351 df-le 11352 df-sub 11546 df-neg 11547 df-nn 12339 df-2 12408 df-3 12409 df-4 12410 df-5 12411 df-6 12412 df-7 12413 df-n0 12610 df-xnn0 12683 df-z 12697 df-uz 12969 df-fz 13643 df-fzo 13792 df-hash 14478 df-word 14662 df-concat 14719 df-s1 14746 df-s2 15003 df-s3 15004 df-s4 15005 df-s5 15006 df-s6 15007 df-s7 15008

This theorem is used by: usgrexmpl2 49218

W3C validator