umgr2cycllem

	Ref	Expression
Hypotheses	umgr2cycllem.1	$⊢ F = ⟨“ J K ”⟩$
	umgr2cycllem.2	$⊢ I = iEdg (G)$
	umgr2cycllem.3	$⊢ φ \to G \in UMGraph$
	umgr2cycllem.4	$⊢ φ \to J \in dom I$
	umgr2cycllem.5	$⊢ φ \to J \neq K$
	umgr2cycllem.6	$⊢ φ \to I (J) = I (K)$
Assertion	umgr2cycllem	$⊢ φ \to \exists p F Cycles (G) p$

Proof

Step	Hyp	Ref	Expression
1		umgr2cycllem.1	$⊢ F = ⟨“ J K ”⟩$
2		umgr2cycllem.2	$⊢ I = iEdg (G)$
3		umgr2cycllem.3	$⊢ φ \to G \in UMGraph$
4		umgr2cycllem.4	$⊢ φ \to J \in dom I$
5		umgr2cycllem.5	$⊢ φ \to J \neq K$
6		umgr2cycllem.6	$⊢ φ \to I (J) = I (K)$
7		umgruhgr	$⊢ G \in UMGraph \to G \in UHGraph$
8	2	uhgrfun	$⊢ G \in UHGraph \to Fun I$
9	3 7 8	3syl	$⊢ φ \to Fun I$
10	2	iedgedg	$⊢ (Fun I \land J \in dom I) \to I (J) \in Edg (G)$
11	9 4 10	syl2anc	$⊢ φ \to I (J) \in Edg (G)$
12		eqid	$⊢ Vtx (G) = Vtx (G)$
13		eqid	$⊢ Edg (G) = Edg (G)$
14	12 13	umgredg	$⊢ (G \in UMGraph \land I (J) \in Edg (G)) \to \exists a \in Vtx (G) \exists b \in Vtx (G) (a \neq b \land I (J) = \{a, b\})$
15	3 11 14	syl2anc	$⊢ φ \to \exists a \in Vtx (G) \exists b \in Vtx (G) (a \neq b \land I (J) = \{a, b\})$
16		ax-5	$⊢ a \in Vtx (G) \to \forall b a \in Vtx (G)$
17		alral	$⊢ \forall b a \in Vtx (G) \to \forall b \in Vtx (G) a \in Vtx (G)$
18	16 17	syl	$⊢ a \in Vtx (G) \to \forall b \in Vtx (G) a \in Vtx (G)$
19		r19.29	$⊢ (\forall b \in Vtx (G) a \in Vtx (G) \land \exists b \in Vtx (G) (a \neq b \land I (J) = \{a, b\})) \to \exists b \in Vtx (G) (a \in Vtx (G) \land (a \neq b \land I (J) = \{a, b\}))$
20	18 19	sylan	$⊢ (a \in Vtx (G) \land \exists b \in Vtx (G) (a \neq b \land I (J) = \{a, b\})) \to \exists b \in Vtx (G) (a \in Vtx (G) \land (a \neq b \land I (J) = \{a, b\}))$
21		eqid	$⊢ ⟨“ a b a ”⟩ = ⟨“ a b a ”⟩$
22		simp2l	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to a \in Vtx (G)$
23		simp2r	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to b \in Vtx (G)$
24	22 23 22	3jca	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to (a \in Vtx (G) \land b \in Vtx (G) \land a \in Vtx (G))$
25		simp3l	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to a \neq b$
26	25	necomd	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to b \neq a$
27	25 26	jca	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to (a \neq b \land b \neq a)$
28		simp3r	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to I (J) = \{a, b\}$
29	28	eqimsscd	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to \{a, b\} \subseteq I (J)$
30	6	3ad2ant1	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to I (J) = I (K)$
31	30 28	eqtr3d	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to I (K) = \{a, b\}$
32		prcom	$⊢ \{a, b\} = \{b, a\}$
33	32	a1i	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to \{a, b\} = \{b, a\}$
34	31 33	eqtrd	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to I (K) = \{b, a\}$
35		eqimss2	$⊢ I (K) = \{b, a\} \to \{b, a\} \subseteq I (K)$
36	34 35	syl	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to \{b, a\} \subseteq I (K)$
37	29 36	jca	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to (\{a, b\} \subseteq I (J) \land \{b, a\} \subseteq I (K))$
38	5	3ad2ant1	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to J \neq K$
39		eqidd	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to a = a$
40	21 1 24 27 37 12 2 38 39	2cycld	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to F Cycles (G) ⟨“ a b a ”⟩$
41	40	3expib	$⊢ φ \to (((a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to F Cycles (G) ⟨“ a b a ”⟩)$
42	41	exp4c	$⊢ φ \to (a \in Vtx (G) \to (b \in Vtx (G) \to ((a \neq b \land I (J) = \{a, b\}) \to F Cycles (G) ⟨“ a b a ”⟩)))$
43	42	com23	$⊢ φ \to (b \in Vtx (G) \to (a \in Vtx (G) \to ((a \neq b \land I (J) = \{a, b\}) \to F Cycles (G) ⟨“ a b a ”⟩)))$
44	43	imp4a	$⊢ φ \to (b \in Vtx (G) \to ((a \in Vtx (G) \land (a \neq b \land I (J) = \{a, b\})) \to F Cycles (G) ⟨“ a b a ”⟩))$
45		s3cli	$⊢ ⟨“ a b a ”⟩ \in Word V$
46		breq2	$⊢ p = ⟨“ a b a ”⟩ \to (F Cycles (G) p \leftrightarrow F Cycles (G) ⟨“ a b a ”⟩)$
47	46	rspcev	$⊢ (⟨“ a b a ”⟩ \in Word V \land F Cycles (G) ⟨“ a b a ”⟩) \to \exists p \in Word V F Cycles (G) p$
48	45 47	mpan	$⊢ F Cycles (G) ⟨“ a b a ”⟩ \to \exists p \in Word V F Cycles (G) p$
49		rexex	$⊢ \exists p \in Word V F Cycles (G) p \to \exists p F Cycles (G) p$
50	48 49	syl	$⊢ F Cycles (G) ⟨“ a b a ”⟩ \to \exists p F Cycles (G) p$
51	44 50	syl8	$⊢ φ \to (b \in Vtx (G) \to ((a \in Vtx (G) \land (a \neq b \land I (J) = \{a, b\})) \to \exists p F Cycles (G) p))$
52	51	rexlimdv	$⊢ φ \to (\exists b \in Vtx (G) (a \in Vtx (G) \land (a \neq b \land I (J) = \{a, b\})) \to \exists p F Cycles (G) p)$
53	20 52	syl5	$⊢ φ \to ((a \in Vtx (G) \land \exists b \in Vtx (G) (a \neq b \land I (J) = \{a, b\})) \to \exists p F Cycles (G) p)$
54	53	expd	$⊢ φ \to (a \in Vtx (G) \to (\exists b \in Vtx (G) (a \neq b \land I (J) = \{a, b\}) \to \exists p F Cycles (G) p))$
55	54	rexlimdv	$⊢ φ \to (\exists a \in Vtx (G) \exists b \in Vtx (G) (a \neq b \land I (J) = \{a, b\}) \to \exists p F Cycles (G) p)$
56	15 55	mpd	$⊢ φ \to \exists p F Cycles (G) p$

Metamath Proof Explorer

Theorem umgr2cycllem

Proof