uhgr3cyclex

Description: If there are three different vertices in a hypergraph which are mutually connected by edges, there is a 3-cycle in the graph containing one of these vertices. (Contributed by Alexander van der Vekens, 17-Nov-2017) (Revised by AV, 12-Feb-2021)

	Ref	Expression
Hypotheses	uhgr3cyclex.v	$⊢ V = Vtx (G)$
	uhgr3cyclex.e	$⊢ E = Edg (G)$
Assertion	uhgr3cyclex	$⊢ (G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C)) \land (\{A, B\} \in E \land \{B, C\} \in E \land \{C, A\} \in E)) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = A)$

Proof

Step	Hyp	Ref	Expression
1		uhgr3cyclex.v	$⊢ V = Vtx (G)$
2		uhgr3cyclex.e	$⊢ E = Edg (G)$
3	2	eleq2i	$⊢ \{A, B\} \in E \leftrightarrow \{A, B\} \in Edg (G)$
4		eqid	$⊢ iEdg (G) = iEdg (G)$
5	4	uhgredgiedgb	$⊢ G \in UHGraph \to (\{A, B\} \in Edg (G) \leftrightarrow \exists i \in dom iEdg (G) \{A, B\} = iEdg (G) (i))$
6	3 5	bitrid	$⊢ G \in UHGraph \to (\{A, B\} \in E \leftrightarrow \exists i \in dom iEdg (G) \{A, B\} = iEdg (G) (i))$
7	2	eleq2i	$⊢ \{B, C\} \in E \leftrightarrow \{B, C\} \in Edg (G)$
8	4	uhgredgiedgb	$⊢ G \in UHGraph \to (\{B, C\} \in Edg (G) \leftrightarrow \exists j \in dom iEdg (G) \{B, C\} = iEdg (G) (j))$
9	7 8	bitrid	$⊢ G \in UHGraph \to (\{B, C\} \in E \leftrightarrow \exists j \in dom iEdg (G) \{B, C\} = iEdg (G) (j))$
10	2	eleq2i	$⊢ \{C, A\} \in E \leftrightarrow \{C, A\} \in Edg (G)$
11	4	uhgredgiedgb	$⊢ G \in UHGraph \to (\{C, A\} \in Edg (G) \leftrightarrow \exists k \in dom iEdg (G) \{C, A\} = iEdg (G) (k))$
12	10 11	bitrid	$⊢ G \in UHGraph \to (\{C, A\} \in E \leftrightarrow \exists k \in dom iEdg (G) \{C, A\} = iEdg (G) (k))$
13	6 9 12	3anbi123d	$⊢ G \in UHGraph \to ((\{A, B\} \in E \land \{B, C\} \in E \land \{C, A\} \in E) \leftrightarrow (\exists i \in dom iEdg (G) \{A, B\} = iEdg (G) (i) \land \exists j \in dom iEdg (G) \{B, C\} = iEdg (G) (j) \land \exists k \in dom iEdg (G) \{C, A\} = iEdg (G) (k)))$
14	13	adantr	$⊢ (G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \to ((\{A, B\} \in E \land \{B, C\} \in E \land \{C, A\} \in E) \leftrightarrow (\exists i \in dom iEdg (G) \{A, B\} = iEdg (G) (i) \land \exists j \in dom iEdg (G) \{B, C\} = iEdg (G) (j) \land \exists k \in dom iEdg (G) \{C, A\} = iEdg (G) (k)))$
15		eqid	$⊢ ⟨“ A B C A ”⟩ = ⟨“ A B C A ”⟩$
16		eqid	$⊢ ⟨“ i j k ”⟩ = ⟨“ i j k ”⟩$
17		3simpa	$⊢ (A \in V \land B \in V \land C \in V) \to (A \in V \land B \in V)$
18		pm3.22	$⊢ (A \in V \land C \in V) \to (C \in V \land A \in V)$
19	18	3adant2	$⊢ (A \in V \land B \in V \land C \in V) \to (C \in V \land A \in V)$
20	17 19	jca	$⊢ (A \in V \land B \in V \land C \in V) \to ((A \in V \land B \in V) \land (C \in V \land A \in V))$
21	20	adantr	$⊢ ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C)) \to ((A \in V \land B \in V) \land (C \in V \land A \in V))$
22	21	ad2antlr	$⊢ ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \land ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)))) \to ((A \in V \land B \in V) \land (C \in V \land A \in V))$
23		3simpa	$⊢ (A \neq B \land A \neq C \land B \neq C) \to (A \neq B \land A \neq C)$
24		necom	$⊢ A \neq B \leftrightarrow B \neq A$
25	24	biimpi	$⊢ A \neq B \to B \neq A$
26	25	anim1ci	$⊢ (A \neq B \land B \neq C) \to (B \neq C \land B \neq A)$
27	26	3adant2	$⊢ (A \neq B \land A \neq C \land B \neq C) \to (B \neq C \land B \neq A)$
28		necom	$⊢ A \neq C \leftrightarrow C \neq A$
29	28	biimpi	$⊢ A \neq C \to C \neq A$
30	29	3ad2ant2	$⊢ (A \neq B \land A \neq C \land B \neq C) \to C \neq A$
31	23 27 30	3jca	$⊢ (A \neq B \land A \neq C \land B \neq C) \to ((A \neq B \land A \neq C) \land (B \neq C \land B \neq A) \land C \neq A)$
32	31	adantl	$⊢ ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C)) \to ((A \neq B \land A \neq C) \land (B \neq C \land B \neq A) \land C \neq A)$
33	32	ad2antlr	$⊢ ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \land ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)))) \to ((A \neq B \land A \neq C) \land (B \neq C \land B \neq A) \land C \neq A)$
34		eqimss	$⊢ \{A, B\} = iEdg (G) (i) \to \{A, B\} \subseteq iEdg (G) (i)$
35	34	adantl	$⊢ (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)) \to \{A, B\} \subseteq iEdg (G) (i)$
36	35	3ad2ant3	$⊢ ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i))) \to \{A, B\} \subseteq iEdg (G) (i)$
37		eqimss	$⊢ \{B, C\} = iEdg (G) (j) \to \{B, C\} \subseteq iEdg (G) (j)$
38	37	adantl	$⊢ (j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \to \{B, C\} \subseteq iEdg (G) (j)$
39	38	3ad2ant1	$⊢ ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i))) \to \{B, C\} \subseteq iEdg (G) (j)$
40		eqimss	$⊢ \{C, A\} = iEdg (G) (k) \to \{C, A\} \subseteq iEdg (G) (k)$
41	40	adantl	$⊢ (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \to \{C, A\} \subseteq iEdg (G) (k)$
42	41	3ad2ant2	$⊢ ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i))) \to \{C, A\} \subseteq iEdg (G) (k)$
43	36 39 42	3jca	$⊢ ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i))) \to (\{A, B\} \subseteq iEdg (G) (i) \land \{B, C\} \subseteq iEdg (G) (j) \land \{C, A\} \subseteq iEdg (G) (k))$
44	43	adantl	$⊢ ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \land ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)))) \to (\{A, B\} \subseteq iEdg (G) (i) \land \{B, C\} \subseteq iEdg (G) (j) \land \{C, A\} \subseteq iEdg (G) (k))$
45		simp3	$⊢ (A \in V \land B \in V \land C \in V) \to C \in V$
46		simp1	$⊢ (A \in V \land B \in V \land C \in V) \to A \in V$
47	45 46	jca	$⊢ (A \in V \land B \in V \land C \in V) \to (C \in V \land A \in V)$
48	47 30	anim12i	$⊢ ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C)) \to ((C \in V \land A \in V) \land C \neq A)$
49	48	adantl	$⊢ (G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \to ((C \in V \land A \in V) \land C \neq A)$
50		pm3.22	$⊢ ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i))) \to ((i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)) \land (j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)))$
51	50	3adant2	$⊢ ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i))) \to ((i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)) \land (j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)))$
52	1 2 4	uhgr3cyclexlem	$⊢ (((C \in V \land A \in V) \land C \neq A) \land ((i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)) \land (j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)))) \to i \neq j$
53	49 51 52	syl2an	$⊢ ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \land ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)))) \to i \neq j$
54		3simpc	$⊢ (A \in V \land B \in V \land C \in V) \to (B \in V \land C \in V)$
55		simp3	$⊢ (A \neq B \land A \neq C \land B \neq C) \to B \neq C$
56	54 55	anim12i	$⊢ ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C)) \to ((B \in V \land C \in V) \land B \neq C)$
57	56	adantl	$⊢ (G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \to ((B \in V \land C \in V) \land B \neq C)$
58		3simpc	$⊢ ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i))) \to ((k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)))$
59	1 2 4	uhgr3cyclexlem	$⊢ (((B \in V \land C \in V) \land B \neq C) \land ((k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)))) \to k \neq i$
60	59	necomd	$⊢ (((B \in V \land C \in V) \land B \neq C) \land ((k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)))) \to i \neq k$
61	57 58 60	syl2an	$⊢ ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \land ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)))) \to i \neq k$
62	1 2 4	uhgr3cyclexlem	$⊢ (((A \in V \land B \in V) \land A \neq B) \land ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)))) \to j \neq k$
63	62	exp31	$⊢ (A \in V \land B \in V) \to (A \neq B \to (((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k))) \to j \neq k))$
64	63	3adant3	$⊢ (A \in V \land B \in V \land C \in V) \to (A \neq B \to (((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k))) \to j \neq k))$
65	64	com12	$⊢ A \neq B \to ((A \in V \land B \in V \land C \in V) \to (((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k))) \to j \neq k))$
66	65	3ad2ant1	$⊢ (A \neq B \land A \neq C \land B \neq C) \to ((A \in V \land B \in V \land C \in V) \to (((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k))) \to j \neq k))$
67	66	impcom	$⊢ ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C)) \to (((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k))) \to j \neq k)$
68	67	adantl	$⊢ (G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \to (((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k))) \to j \neq k)$
69	68	com12	$⊢ ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k))) \to ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \to j \neq k)$
70	69	3adant3	$⊢ ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i))) \to ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \to j \neq k)$
71	70	impcom	$⊢ ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \land ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)))) \to j \neq k$
72	53 61 71	3jca	$⊢ ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \land ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)))) \to (i \neq j \land i \neq k \land j \neq k)$
73		eqidd	$⊢ ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \land ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)))) \to A = A$
74	15 16 22 33 44 1 4 72 73	3cyclpd	$⊢ ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \land ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)))) \to (⟨“ i j k ”⟩ Cycles (G) ⟨“ A B C A ”⟩ \land \|⟨“ i j k ”⟩\| = 3 \land ⟨“ A B C A ”⟩ (0) = A)$
75		s3cli	$⊢ ⟨“ i j k ”⟩ \in Word V$
76	75	elexi	$⊢ ⟨“ i j k ”⟩ \in V$
77		s4cli	$⊢ ⟨“ A B C A ”⟩ \in Word V$
78	77	elexi	$⊢ ⟨“ A B C A ”⟩ \in V$
79		breq12	$⊢ (f = ⟨“ i j k ”⟩ \land p = ⟨“ A B C A ”⟩) \to (f Cycles (G) p \leftrightarrow ⟨“ i j k ”⟩ Cycles (G) ⟨“ A B C A ”⟩)$
80		fveqeq2	$⊢ f = ⟨“ i j k ”⟩ \to (\|f\| = 3 \leftrightarrow \|⟨“ i j k ”⟩\| = 3)$
81	80	adantr	$⊢ (f = ⟨“ i j k ”⟩ \land p = ⟨“ A B C A ”⟩) \to (\|f\| = 3 \leftrightarrow \|⟨“ i j k ”⟩\| = 3)$
82		fveq1	$⊢ p = ⟨“ A B C A ”⟩ \to p (0) = ⟨“ A B C A ”⟩ (0)$
83	82	eqeq1d	$⊢ p = ⟨“ A B C A ”⟩ \to (p (0) = A \leftrightarrow ⟨“ A B C A ”⟩ (0) = A)$
84	83	adantl	$⊢ (f = ⟨“ i j k ”⟩ \land p = ⟨“ A B C A ”⟩) \to (p (0) = A \leftrightarrow ⟨“ A B C A ”⟩ (0) = A)$
85	79 81 84	3anbi123d	$⊢ (f = ⟨“ i j k ”⟩ \land p = ⟨“ A B C A ”⟩) \to ((f Cycles (G) p \land \|f\| = 3 \land p (0) = A) \leftrightarrow (⟨“ i j k ”⟩ Cycles (G) ⟨“ A B C A ”⟩ \land \|⟨“ i j k ”⟩\| = 3 \land ⟨“ A B C A ”⟩ (0) = A))$
86	76 78 85	spc2ev	$⊢ (⟨“ i j k ”⟩ Cycles (G) ⟨“ A B C A ”⟩ \land \|⟨“ i j k ”⟩\| = 3 \land ⟨“ A B C A ”⟩ (0) = A) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = A)$
87	74 86	syl	$⊢ ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \land ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)))) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = A)$
88	87	expcom	$⊢ ((j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \land (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \land (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i))) \to ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = A))$
89	88	3exp	$⊢ (j \in dom iEdg (G) \land \{B, C\} = iEdg (G) (j)) \to ((k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \to ((i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)) \to ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = A))))$
90	89	rexlimiva	$⊢ \exists j \in dom iEdg (G) \{B, C\} = iEdg (G) (j) \to ((k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \to ((i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)) \to ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = A))))$
91	90	com12	$⊢ (k \in dom iEdg (G) \land \{C, A\} = iEdg (G) (k)) \to (\exists j \in dom iEdg (G) \{B, C\} = iEdg (G) (j) \to ((i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)) \to ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = A))))$
92	91	rexlimiva	$⊢ \exists k \in dom iEdg (G) \{C, A\} = iEdg (G) (k) \to (\exists j \in dom iEdg (G) \{B, C\} = iEdg (G) (j) \to ((i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)) \to ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = A))))$
93	92	com13	$⊢ (i \in dom iEdg (G) \land \{A, B\} = iEdg (G) (i)) \to (\exists j \in dom iEdg (G) \{B, C\} = iEdg (G) (j) \to (\exists k \in dom iEdg (G) \{C, A\} = iEdg (G) (k) \to ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = A))))$
94	93	rexlimiva	$⊢ \exists i \in dom iEdg (G) \{A, B\} = iEdg (G) (i) \to (\exists j \in dom iEdg (G) \{B, C\} = iEdg (G) (j) \to (\exists k \in dom iEdg (G) \{C, A\} = iEdg (G) (k) \to ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = A))))$
95	94	3imp	$⊢ (\exists i \in dom iEdg (G) \{A, B\} = iEdg (G) (i) \land \exists j \in dom iEdg (G) \{B, C\} = iEdg (G) (j) \land \exists k \in dom iEdg (G) \{C, A\} = iEdg (G) (k)) \to ((G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = A))$
96	95	com12	$⊢ (G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \to ((\exists i \in dom iEdg (G) \{A, B\} = iEdg (G) (i) \land \exists j \in dom iEdg (G) \{B, C\} = iEdg (G) (j) \land \exists k \in dom iEdg (G) \{C, A\} = iEdg (G) (k)) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = A))$
97	14 96	sylbid	$⊢ (G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C))) \to ((\{A, B\} \in E \land \{B, C\} \in E \land \{C, A\} \in E) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = A))$
98	97	3impia	$⊢ (G \in UHGraph \land ((A \in V \land B \in V \land C \in V) \land (A \neq B \land A \neq C \land B \neq C)) \land (\{A, B\} \in E \land \{B, C\} \in E \land \{C, A\} \in E)) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 3 \land p (0) = A)$

Metamath Proof Explorer

Theorem uhgr3cyclex

Proof