4cycl4dv - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 4cycl4dv		Structured version Visualization version GIF version

Theorem 4cycl4dv 26195

Description: In a simple graph, the vertices of a 4-cycle are mutually different. (Contributed by Alexander van der Vekens, 18-Nov-2017.)

**Assertion**
Ref	Expression
4cycl4dv	⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) → ((((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})) → ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷)))))

**Proof of Theorem 4cycl4dv**
Step	Hyp	Ref	Expression
1		usgrafun 25878	. . . . 5 ⊢ (𝑉 USGrph 𝐸 → Fun 𝐸)
2		4pos 10993	. . . . . . . . . . . . . . 15 ⊢ 0 < 4
3		breq2 4587	. . . . . . . . . . . . . . 15 ⊢ ((#‘𝐹) = 4 → (0 < (#‘𝐹) ↔ 0 < 4))
4	2, 3	mpbiri 247	. . . . . . . . . . . . . 14 ⊢ ((#‘𝐹) = 4 → 0 < (#‘𝐹))
5		0nn0 11184	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℕ₀
6	4, 5	jctil 558	. . . . . . . . . . . . 13 ⊢ ((#‘𝐹) = 4 → (0 ∈ ℕ₀ ∧ 0 < (#‘𝐹)))
7		nvnencycllem 26171	. . . . . . . . . . . . 13 ⊢ (((Fun 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (0 ∈ ℕ₀ ∧ 0 < (#‘𝐹))) → ((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} → {𝐴, 𝐵} ∈ ran 𝐸))
8	6, 7	sylan2 490	. . . . . . . . . . . 12 ⊢ (((Fun 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) = 4) → ((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} → {𝐴, 𝐵} ∈ ran 𝐸))
9		1lt4 11076	. . . . . . . . . . . . . . 15 ⊢ 1 < 4
10		breq2 4587	. . . . . . . . . . . . . . 15 ⊢ ((#‘𝐹) = 4 → (1 < (#‘𝐹) ↔ 1 < 4))
11	9, 10	mpbiri 247	. . . . . . . . . . . . . 14 ⊢ ((#‘𝐹) = 4 → 1 < (#‘𝐹))
12		1nn0 11185	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ₀
13	11, 12	jctil 558	. . . . . . . . . . . . 13 ⊢ ((#‘𝐹) = 4 → (1 ∈ ℕ₀ ∧ 1 < (#‘𝐹)))
14		nvnencycllem 26171	. . . . . . . . . . . . 13 ⊢ (((Fun 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (1 ∈ ℕ₀ ∧ 1 < (#‘𝐹))) → ((𝐸‘(𝐹‘1)) = {𝐵, 𝐶} → {𝐵, 𝐶} ∈ ran 𝐸))
15	13, 14	sylan2 490	. . . . . . . . . . . 12 ⊢ (((Fun 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) = 4) → ((𝐸‘(𝐹‘1)) = {𝐵, 𝐶} → {𝐵, 𝐶} ∈ ran 𝐸))
16	8, 15	anim12d 584	. . . . . . . . . . 11 ⊢ (((Fun 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) = 4) → (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))
17		2lt4 11075	. . . . . . . . . . . . . . 15 ⊢ 2 < 4
18		breq2 4587	. . . . . . . . . . . . . . 15 ⊢ ((#‘𝐹) = 4 → (2 < (#‘𝐹) ↔ 2 < 4))
19	17, 18	mpbiri 247	. . . . . . . . . . . . . 14 ⊢ ((#‘𝐹) = 4 → 2 < (#‘𝐹))
20		2nn0 11186	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ₀
21	19, 20	jctil 558	. . . . . . . . . . . . 13 ⊢ ((#‘𝐹) = 4 → (2 ∈ ℕ₀ ∧ 2 < (#‘𝐹)))
22		nvnencycllem 26171	. . . . . . . . . . . . 13 ⊢ (((Fun 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (2 ∈ ℕ₀ ∧ 2 < (#‘𝐹))) → ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} → {𝐶, 𝐷} ∈ ran 𝐸))
23	21, 22	sylan2 490	. . . . . . . . . . . 12 ⊢ (((Fun 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) = 4) → ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} → {𝐶, 𝐷} ∈ ran 𝐸))
24		3lt4 11074	. . . . . . . . . . . . . . 15 ⊢ 3 < 4
25		breq2 4587	. . . . . . . . . . . . . . 15 ⊢ ((#‘𝐹) = 4 → (3 < (#‘𝐹) ↔ 3 < 4))
26	24, 25	mpbiri 247	. . . . . . . . . . . . . 14 ⊢ ((#‘𝐹) = 4 → 3 < (#‘𝐹))
27		3nn0 11187	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℕ₀
28	26, 27	jctil 558	. . . . . . . . . . . . 13 ⊢ ((#‘𝐹) = 4 → (3 ∈ ℕ₀ ∧ 3 < (#‘𝐹)))
29		nvnencycllem 26171	. . . . . . . . . . . . 13 ⊢ (((Fun 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (3 ∈ ℕ₀ ∧ 3 < (#‘𝐹))) → ((𝐸‘(𝐹‘3)) = {𝐷, 𝐴} → {𝐷, 𝐴} ∈ ran 𝐸))
30	28, 29	sylan2 490	. . . . . . . . . . . 12 ⊢ (((Fun 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) = 4) → ((𝐸‘(𝐹‘3)) = {𝐷, 𝐴} → {𝐷, 𝐴} ∈ ran 𝐸))
31	23, 30	anim12d 584	. . . . . . . . . . 11 ⊢ (((Fun 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) = 4) → (((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}) → ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)))
32	16, 31	anim12d 584	. . . . . . . . . 10 ⊢ (((Fun 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) = 4) → ((((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸))))
33	32	ex 449	. . . . . . . . 9 ⊢ ((Fun 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) → ((#‘𝐹) = 4 → ((((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)))))
34	33	expcom 450	. . . . . . . 8 ⊢ (𝐹 ∈ Word dom 𝐸 → (Fun 𝐸 → ((#‘𝐹) = 4 → ((((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸))))))
35	34	com23 84	. . . . . . 7 ⊢ (𝐹 ∈ Word dom 𝐸 → ((#‘𝐹) = 4 → (Fun 𝐸 → ((((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸))))))
36	35	imp 444	. . . . . 6 ⊢ ((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 4) → (Fun 𝐸 → ((((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)))))
37	36	3adant2 1073	. . . . 5 ⊢ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4) → (Fun 𝐸 → ((((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)))))
38	1, 37	mpan9 485	. . . 4 ⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) → ((((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸))))
39	38	imp 444	. . 3 ⊢ (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)))
40		simpl 472	. . . 4 ⊢ (((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) ∧ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})))) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)))
41		usgraedgrn 25910	. . . . . . . . . . 11 ⊢ ((𝑉 USGrph 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 ≠ 𝐵)
42	41	ex 449	. . . . . . . . . 10 ⊢ (𝑉 USGrph 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 → 𝐴 ≠ 𝐵))
43	42	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → ({𝐴, 𝐵} ∈ ran 𝐸 → 𝐴 ≠ 𝐵))
44	43	com12 32	. . . . . . . 8 ⊢ ({𝐴, 𝐵} ∈ ran 𝐸 → (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → 𝐴 ≠ 𝐵))
45	44	ad2antrr 758	. . . . . . 7 ⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) → (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → 𝐴 ≠ 𝐵))
46	45	imp 444	. . . . . 6 ⊢ (((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) ∧ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})))) → 𝐴 ≠ 𝐵)
47		preq1 4212	. . . . . . . . . . . . . 14 ⊢ (𝐴 = 𝐶 → {𝐴, 𝐵} = {𝐶, 𝐵})
48	47	eqeq2d 2620	. . . . . . . . . . . . 13 ⊢ (𝐴 = 𝐶 → ((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ↔ (𝐸‘(𝐹‘0)) = {𝐶, 𝐵}))
49		prcom 4211	. . . . . . . . . . . . . . 15 ⊢ {𝐵, 𝐶} = {𝐶, 𝐵}
50	49	eqeq2i 2622	. . . . . . . . . . . . . 14 ⊢ ((𝐸‘(𝐹‘1)) = {𝐵, 𝐶} ↔ (𝐸‘(𝐹‘1)) = {𝐶, 𝐵})
51	50	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝐴 = 𝐶 → ((𝐸‘(𝐹‘1)) = {𝐵, 𝐶} ↔ (𝐸‘(𝐹‘1)) = {𝐶, 𝐵}))
52	48, 51	anbi12d 743	. . . . . . . . . . . 12 ⊢ (𝐴 = 𝐶 → (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ↔ ((𝐸‘(𝐹‘0)) = {𝐶, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐶, 𝐵})))
53	52	adantr 480	. . . . . . . . . . 11 ⊢ ((𝐴 = 𝐶 ∧ (𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4))) → (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ↔ ((𝐸‘(𝐹‘0)) = {𝐶, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐶, 𝐵})))
54		eqtr3 2631	. . . . . . . . . . . . 13 ⊢ (((𝐸‘(𝐹‘0)) = {𝐶, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐶, 𝐵}) → (𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1)))
55		usgraf1 25889	. . . . . . . . . . . . . . 15 ⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→ran 𝐸)
56		wrdf 13165	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Word dom 𝐸 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸)
57		oveq2 6557	. . . . . . . . . . . . . . . . . . 19 ⊢ ((#‘𝐹) = 4 → (0..^(#‘𝐹)) = (0..^4))
58	57	feq2d 5944	. . . . . . . . . . . . . . . . . 18 ⊢ ((#‘𝐹) = 4 → (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ↔ 𝐹:(0..^4)⟶dom 𝐸))
59		4nn 11064	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 4 ∈ ℕ
60		lbfzo0 12375	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ (0..^4) ↔ 4 ∈ ℕ)
61	59, 60	mpbir 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ (0..^4)
62		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹:(0..^4)⟶dom 𝐸 ∧ 0 ∈ (0..^4)) → (𝐹‘0) ∈ dom 𝐸)
63	61, 62	mpan2 703	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹:(0..^4)⟶dom 𝐸 → (𝐹‘0) ∈ dom 𝐸)
64		elfzo0 12376	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ (0..^4) ↔ (1 ∈ ℕ₀ ∧ 4 ∈ ℕ ∧ 1 < 4))
65	12, 59, 9, 64	mpbir3an 1237	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ (0..^4)
66		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹:(0..^4)⟶dom 𝐸 ∧ 1 ∈ (0..^4)) → (𝐹‘1) ∈ dom 𝐸)
67	65, 66	mpan2 703	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹:(0..^4)⟶dom 𝐸 → (𝐹‘1) ∈ dom 𝐸)
68	63, 67	jca 553	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:(0..^4)⟶dom 𝐸 → ((𝐹‘0) ∈ dom 𝐸 ∧ (𝐹‘1) ∈ dom 𝐸))
69	58, 68	syl6bi 242	. . . . . . . . . . . . . . . . 17 ⊢ ((#‘𝐹) = 4 → (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → ((𝐹‘0) ∈ dom 𝐸 ∧ (𝐹‘1) ∈ dom 𝐸)))
70	56, 69	mpan9 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 4) → ((𝐹‘0) ∈ dom 𝐸 ∧ (𝐹‘1) ∈ dom 𝐸))
71	70	3adant2 1073	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4) → ((𝐹‘0) ∈ dom 𝐸 ∧ (𝐹‘1) ∈ dom 𝐸))
72		f1veqaeq 6418	. . . . . . . . . . . . . . 15 ⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ ((𝐹‘0) ∈ dom 𝐸 ∧ (𝐹‘1) ∈ dom 𝐸)) → ((𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1)) → (𝐹‘0) = (𝐹‘1)))
73	55, 71, 72	syl2an 493	. . . . . . . . . . . . . 14 ⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) → ((𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1)) → (𝐹‘0) = (𝐹‘1)))
74		df-f1 5809	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ↔ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ Fun ^◡𝐹))
75		f1eq2 6010	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0..^(#‘𝐹)) = (0..^4) → (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ↔ 𝐹:(0..^4)–1-1→dom 𝐸))
76	57, 75	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((#‘𝐹) = 4 → (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ↔ 𝐹:(0..^4)–1-1→dom 𝐸))
77		f1veqaeq 6418	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹:(0..^4)–1-1→dom 𝐸 ∧ (0 ∈ (0..^4) ∧ 1 ∈ (0..^4))) → ((𝐹‘0) = (𝐹‘1) → 0 = 1))
78	61, 65, 77	mpanr12 717	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹:(0..^4)–1-1→dom 𝐸 → ((𝐹‘0) = (𝐹‘1) → 0 = 1))
79		ax-1ne0 9884	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ≠ 0
80	79	nesymi 2839	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ¬ 0 = 1
81	80	pm2.21i 115	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0 = 1 → 𝐴 ≠ 𝐶)
82	78, 81	syl6 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:(0..^4)–1-1→dom 𝐸 → ((𝐹‘0) = (𝐹‘1) → 𝐴 ≠ 𝐶))
83	76, 82	syl6bi 242	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((#‘𝐹) = 4 → (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 → ((𝐹‘0) = (𝐹‘1) → 𝐴 ≠ 𝐶)))
84	83	com12 32	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 → ((#‘𝐹) = 4 → ((𝐹‘0) = (𝐹‘1) → 𝐴 ≠ 𝐶)))
85	74, 84	sylbir 224	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ Fun ^◡𝐹) → ((#‘𝐹) = 4 → ((𝐹‘0) = (𝐹‘1) → 𝐴 ≠ 𝐶)))
86	85	ex 449	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → (Fun ^◡𝐹 → ((#‘𝐹) = 4 → ((𝐹‘0) = (𝐹‘1) → 𝐴 ≠ 𝐶))))
87	56, 86	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Word dom 𝐸 → (Fun ^◡𝐹 → ((#‘𝐹) = 4 → ((𝐹‘0) = (𝐹‘1) → 𝐴 ≠ 𝐶))))
88	87	3imp 1249	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4) → ((𝐹‘0) = (𝐹‘1) → 𝐴 ≠ 𝐶))
89	88	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) → ((𝐹‘0) = (𝐹‘1) → 𝐴 ≠ 𝐶))
90	73, 89	syld 46	. . . . . . . . . . . . 13 ⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) → ((𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1)) → 𝐴 ≠ 𝐶))
91	54, 90	syl5 33	. . . . . . . . . . . 12 ⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) → (((𝐸‘(𝐹‘0)) = {𝐶, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐶, 𝐵}) → 𝐴 ≠ 𝐶))
92	91	adantl 481	. . . . . . . . . . 11 ⊢ ((𝐴 = 𝐶 ∧ (𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4))) → (((𝐸‘(𝐹‘0)) = {𝐶, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐶, 𝐵}) → 𝐴 ≠ 𝐶))
93	53, 92	sylbid 229	. . . . . . . . . 10 ⊢ ((𝐴 = 𝐶 ∧ (𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4))) → (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) → 𝐴 ≠ 𝐶))
94	93	adantrd 483	. . . . . . . . 9 ⊢ ((𝐴 = 𝐶 ∧ (𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4))) → ((((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})) → 𝐴 ≠ 𝐶))
95	94	expimpd 627	. . . . . . . 8 ⊢ (𝐴 = 𝐶 → (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → 𝐴 ≠ 𝐶))
96		ax-1 6	. . . . . . . 8 ⊢ (𝐴 ≠ 𝐶 → (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → 𝐴 ≠ 𝐶))
97	95, 96	pm2.61ine 2865	. . . . . . 7 ⊢ (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → 𝐴 ≠ 𝐶)
98	97	adantl 481	. . . . . 6 ⊢ (((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) ∧ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})))) → 𝐴 ≠ 𝐶)
99		usgraedgrn 25910	. . . . . . . . . . . . 13 ⊢ ((𝑉 USGrph 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸) → 𝐷 ≠ 𝐴)
100	99	necomd 2837	. . . . . . . . . . . 12 ⊢ ((𝑉 USGrph 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸) → 𝐴 ≠ 𝐷)
101	100	ex 449	. . . . . . . . . . 11 ⊢ (𝑉 USGrph 𝐸 → ({𝐷, 𝐴} ∈ ran 𝐸 → 𝐴 ≠ 𝐷))
102	101	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → ({𝐷, 𝐴} ∈ ran 𝐸 → 𝐴 ≠ 𝐷))
103	102	com12 32	. . . . . . . . 9 ⊢ ({𝐷, 𝐴} ∈ ran 𝐸 → (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → 𝐴 ≠ 𝐷))
104	103	adantl 481	. . . . . . . 8 ⊢ (({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸) → (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → 𝐴 ≠ 𝐷))
105	104	adantl 481	. . . . . . 7 ⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) → (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → 𝐴 ≠ 𝐷))
106	105	imp 444	. . . . . 6 ⊢ (((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) ∧ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})))) → 𝐴 ≠ 𝐷)
107	46, 98, 106	3jca 1235	. . . . 5 ⊢ (((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) ∧ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})))) → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷))
108		usgraedgrn 25910	. . . . . . . . . . . 12 ⊢ ((𝑉 USGrph 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → 𝐵 ≠ 𝐶)
109	108	ex 449	. . . . . . . . . . 11 ⊢ (𝑉 USGrph 𝐸 → ({𝐵, 𝐶} ∈ ran 𝐸 → 𝐵 ≠ 𝐶))
110	109	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → ({𝐵, 𝐶} ∈ ran 𝐸 → 𝐵 ≠ 𝐶))
111	110	com12 32	. . . . . . . . 9 ⊢ ({𝐵, 𝐶} ∈ ran 𝐸 → (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → 𝐵 ≠ 𝐶))
112	111	adantl 481	. . . . . . . 8 ⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → 𝐵 ≠ 𝐶))
113	112	adantr 480	. . . . . . 7 ⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) → (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → 𝐵 ≠ 𝐶))
114	113	imp 444	. . . . . 6 ⊢ (((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) ∧ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})))) → 𝐵 ≠ 𝐶)
115		prcom 4211	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝐷, 𝐴} = {𝐴, 𝐷}
116	115	eqeq2i 2622	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸‘(𝐹‘3)) = {𝐷, 𝐴} ↔ (𝐸‘(𝐹‘3)) = {𝐴, 𝐷})
117	116	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 = 𝐷 → ((𝐸‘(𝐹‘3)) = {𝐷, 𝐴} ↔ (𝐸‘(𝐹‘3)) = {𝐴, 𝐷}))
118		preq2 4213	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 = 𝐷 → {𝐴, 𝐵} = {𝐴, 𝐷})
119	118	eqeq2d 2620	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 = 𝐷 → ((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ↔ (𝐸‘(𝐹‘0)) = {𝐴, 𝐷}))
120	117, 119	anbi12d 743	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 = 𝐷 → (((𝐸‘(𝐹‘3)) = {𝐷, 𝐴} ∧ (𝐸‘(𝐹‘0)) = {𝐴, 𝐵}) ↔ ((𝐸‘(𝐹‘3)) = {𝐴, 𝐷} ∧ (𝐸‘(𝐹‘0)) = {𝐴, 𝐷})))
121	120	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 = 𝐷 ∧ (𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4))) → (((𝐸‘(𝐹‘3)) = {𝐷, 𝐴} ∧ (𝐸‘(𝐹‘0)) = {𝐴, 𝐵}) ↔ ((𝐸‘(𝐹‘3)) = {𝐴, 𝐷} ∧ (𝐸‘(𝐹‘0)) = {𝐴, 𝐷})))
122		eqtr3 2631	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐸‘(𝐹‘3)) = {𝐴, 𝐷} ∧ (𝐸‘(𝐹‘0)) = {𝐴, 𝐷}) → (𝐸‘(𝐹‘3)) = (𝐸‘(𝐹‘0)))
123		elfzo0 12376	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (3 ∈ (0..^4) ↔ (3 ∈ ℕ₀ ∧ 4 ∈ ℕ ∧ 3 < 4))
124	27, 59, 24, 123	mpbir3an 1237	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 3 ∈ (0..^4)
125		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹:(0..^4)⟶dom 𝐸 ∧ 3 ∈ (0..^4)) → (𝐹‘3) ∈ dom 𝐸)
126	124, 125	mpan2 703	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹:(0..^4)⟶dom 𝐸 → (𝐹‘3) ∈ dom 𝐸)
127	126, 63	jca 553	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:(0..^4)⟶dom 𝐸 → ((𝐹‘3) ∈ dom 𝐸 ∧ (𝐹‘0) ∈ dom 𝐸))
128	58, 127	syl6bi 242	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((#‘𝐹) = 4 → (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → ((𝐹‘3) ∈ dom 𝐸 ∧ (𝐹‘0) ∈ dom 𝐸)))
129	56, 128	mpan9 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 4) → ((𝐹‘3) ∈ dom 𝐸 ∧ (𝐹‘0) ∈ dom 𝐸))
130	129	3adant2 1073	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4) → ((𝐹‘3) ∈ dom 𝐸 ∧ (𝐹‘0) ∈ dom 𝐸))
131		f1veqaeq 6418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ ((𝐹‘3) ∈ dom 𝐸 ∧ (𝐹‘0) ∈ dom 𝐸)) → ((𝐸‘(𝐹‘3)) = (𝐸‘(𝐹‘0)) → (𝐹‘3) = (𝐹‘0)))
132	55, 130, 131	syl2an 493	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) → ((𝐸‘(𝐹‘3)) = (𝐸‘(𝐹‘0)) → (𝐹‘3) = (𝐹‘0)))
133		f1veqaeq 6418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹:(0..^4)–1-1→dom 𝐸 ∧ (3 ∈ (0..^4) ∧ 0 ∈ (0..^4))) → ((𝐹‘3) = (𝐹‘0) → 3 = 0))
134	124, 61, 133	mpanr12 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐹:(0..^4)–1-1→dom 𝐸 → ((𝐹‘3) = (𝐹‘0) → 3 = 0))
135		3ne0 10992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 3 ≠ 0
136	135	neii 2784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ¬ 3 = 0
137	136	pm2.21i 115	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (3 = 0 → 𝐵 ≠ 𝐷)
138	134, 137	syl6 34	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹:(0..^4)–1-1→dom 𝐸 → ((𝐹‘3) = (𝐹‘0) → 𝐵 ≠ 𝐷))
139	76, 138	syl6bi 242	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((#‘𝐹) = 4 → (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 → ((𝐹‘3) = (𝐹‘0) → 𝐵 ≠ 𝐷)))
140	139	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 → ((#‘𝐹) = 4 → ((𝐹‘3) = (𝐹‘0) → 𝐵 ≠ 𝐷)))
141	74, 140	sylbir 224	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ Fun ^◡𝐹) → ((#‘𝐹) = 4 → ((𝐹‘3) = (𝐹‘0) → 𝐵 ≠ 𝐷)))
142	141	ex 449	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → (Fun ^◡𝐹 → ((#‘𝐹) = 4 → ((𝐹‘3) = (𝐹‘0) → 𝐵 ≠ 𝐷))))
143	56, 142	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ Word dom 𝐸 → (Fun ^◡𝐹 → ((#‘𝐹) = 4 → ((𝐹‘3) = (𝐹‘0) → 𝐵 ≠ 𝐷))))
144	143	3imp 1249	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4) → ((𝐹‘3) = (𝐹‘0) → 𝐵 ≠ 𝐷))
145	144	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) → ((𝐹‘3) = (𝐹‘0) → 𝐵 ≠ 𝐷))
146	132, 145	syld 46	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) → ((𝐸‘(𝐹‘3)) = (𝐸‘(𝐹‘0)) → 𝐵 ≠ 𝐷))
147	122, 146	syl5 33	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) → (((𝐸‘(𝐹‘3)) = {𝐴, 𝐷} ∧ (𝐸‘(𝐹‘0)) = {𝐴, 𝐷}) → 𝐵 ≠ 𝐷))
148	147	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 = 𝐷 ∧ (𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4))) → (((𝐸‘(𝐹‘3)) = {𝐴, 𝐷} ∧ (𝐸‘(𝐹‘0)) = {𝐴, 𝐷}) → 𝐵 ≠ 𝐷))
149	121, 148	sylbid 229	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 = 𝐷 ∧ (𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4))) → (((𝐸‘(𝐹‘3)) = {𝐷, 𝐴} ∧ (𝐸‘(𝐹‘0)) = {𝐴, 𝐵}) → 𝐵 ≠ 𝐷))
150	149	com12 32	. . . . . . . . . . . . . . 15 ⊢ (((𝐸‘(𝐹‘3)) = {𝐷, 𝐴} ∧ (𝐸‘(𝐹‘0)) = {𝐴, 𝐵}) → ((𝐵 = 𝐷 ∧ (𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4))) → 𝐵 ≠ 𝐷))
151	150	ex 449	. . . . . . . . . . . . . 14 ⊢ ((𝐸‘(𝐹‘3)) = {𝐷, 𝐴} → ((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} → ((𝐵 = 𝐷 ∧ (𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4))) → 𝐵 ≠ 𝐷)))
152	151	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}) → ((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} → ((𝐵 = 𝐷 ∧ (𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4))) → 𝐵 ≠ 𝐷)))
153	152	com12 32	. . . . . . . . . . . 12 ⊢ ((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} → (((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}) → ((𝐵 = 𝐷 ∧ (𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4))) → 𝐵 ≠ 𝐷)))
154	153	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) → (((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}) → ((𝐵 = 𝐷 ∧ (𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4))) → 𝐵 ≠ 𝐷)))
155	154	imp 444	. . . . . . . . . 10 ⊢ ((((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})) → ((𝐵 = 𝐷 ∧ (𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4))) → 𝐵 ≠ 𝐷))
156	155	com12 32	. . . . . . . . 9 ⊢ ((𝐵 = 𝐷 ∧ (𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4))) → ((((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})) → 𝐵 ≠ 𝐷))
157	156	expimpd 627	. . . . . . . 8 ⊢ (𝐵 = 𝐷 → (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → 𝐵 ≠ 𝐷))
158		ax-1 6	. . . . . . . 8 ⊢ (𝐵 ≠ 𝐷 → (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → 𝐵 ≠ 𝐷))
159	157, 158	pm2.61ine 2865	. . . . . . 7 ⊢ (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → 𝐵 ≠ 𝐷)
160	159	adantl 481	. . . . . 6 ⊢ (((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) ∧ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})))) → 𝐵 ≠ 𝐷)
161		usgraedgrn 25910	. . . . . . . . . . . 12 ⊢ ((𝑉 USGrph 𝐸 ∧ {𝐶, 𝐷} ∈ ran 𝐸) → 𝐶 ≠ 𝐷)
162	161	ex 449	. . . . . . . . . . 11 ⊢ (𝑉 USGrph 𝐸 → ({𝐶, 𝐷} ∈ ran 𝐸 → 𝐶 ≠ 𝐷))
163	162	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → ({𝐶, 𝐷} ∈ ran 𝐸 → 𝐶 ≠ 𝐷))
164	163	com12 32	. . . . . . . . 9 ⊢ ({𝐶, 𝐷} ∈ ran 𝐸 → (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → 𝐶 ≠ 𝐷))
165	164	adantr 480	. . . . . . . 8 ⊢ (({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸) → (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → 𝐶 ≠ 𝐷))
166	165	adantl 481	. . . . . . 7 ⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) → (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → 𝐶 ≠ 𝐷))
167	166	imp 444	. . . . . 6 ⊢ (((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) ∧ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})))) → 𝐶 ≠ 𝐷)
168	114, 160, 167	3jca 1235	. . . . 5 ⊢ (((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) ∧ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})))) → (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))
169	107, 168	jca 553	. . . 4 ⊢ (((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) ∧ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})))) → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷)))
170	40, 169	jca 553	. . 3 ⊢ (((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) ∧ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})))) → ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))))
171	39, 170	mpancom 700	. 2 ⊢ (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) ∧ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴}))) → ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))))
172	171	ex 449	1 ⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ Fun ^◡𝐹 ∧ (#‘𝐹) = 4)) → ((((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶}) ∧ ((𝐸‘(𝐹‘2)) = {𝐶, 𝐷} ∧ (𝐸‘(𝐹‘3)) = {𝐷, 𝐴})) → ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 {cpr 4127 class class class wbr 4583 ^◡ccnv 5037 dom cdm 5038 ran crn 5039 Fun wfun 5798 ⟶wf 5800 –1-1→wf1 5801 ‘cfv 5804 (class class class)co 6549 0cc0 9815 1c1 9816 < clt 9953 ℕcn 10897 2c2 10947 3c3 10948 4c4 10949 ℕ₀cn0 11169 ..^cfzo 12334 #chash 12979 Word cword 13146 USGrph cusg 25859

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-2 10956 df-3 10957 df-4 10958 df-n0 11170 df-z 11255 df-uz 11564 df-fz 12198 df-fzo 12335 df-hash 12980 df-word 13154 df-usgra 25862

This theorem is referenced by: 4cycl4dv4e 26196

W3C validator