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		simp2	$⊢ (φ \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))$
23		simp3l	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to a \neq b$
24		eqimss2	$⊢ I (J) = \{a, b\} \to \{a, b\} \subseteq I (J)$
25	24	adantl	$⊢ (a \neq b \land I (J) = \{a, b\}) \to \{a, b\} \subseteq I (J)$
26	25	3ad2ant3	$⊢ (φ \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)$
27	6	sseq2d	$⊢ φ \to (\{a, b\} \subseteq I (J) \leftrightarrow \{a, b\} \subseteq I (K))$
28	24 27	imbitrid	$⊢ φ \to (I (J) = \{a, b\} \to \{a, b\} \subseteq I (K))$
29	28	adantld	$⊢ φ \to ((a \neq b \land I (J) = \{a, b\}) \to \{a, b\} \subseteq I (K))$
30	29	adantld	$⊢ φ \to (((a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to \{a, b\} \subseteq I (K))$
31	30	3impib	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G)) \land (a \neq b \land I (J) = \{a, b\})) \to \{a, b\} \subseteq I (K)$
32	26 31	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 \{a, b\} \subseteq I (K))$
33	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$
34	21 1 22 23 32 12 2 33	2cycl2d	$⊢ (φ \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 ”⟩$
35	34	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 ”⟩)$
36	35	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 ”⟩)))$
37	36	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 ”⟩)))$
38	37	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 ”⟩))$
39		s3cli	$⊢ ⟨“ a b a ”⟩ \in Word V$
40		breq2	$⊢ p = ⟨“ a b a ”⟩ \to (F Cycles (G) p \leftrightarrow F Cycles (G) ⟨“ a b a ”⟩)$
41	40	rspcev	$⊢ (⟨“ a b a ”⟩ \in Word V \land F Cycles (G) ⟨“ a b a ”⟩) \to \exists p \in Word V F Cycles (G) p$
42	39 41	mpan	$⊢ F Cycles (G) ⟨“ a b a ”⟩ \to \exists p \in Word V F Cycles (G) p$
43		rexex	$⊢ \exists p \in Word V F Cycles (G) p \to \exists p F Cycles (G) p$
44	42 43	syl	$⊢ F Cycles (G) ⟨“ a b a ”⟩ \to \exists p F Cycles (G) p$
45	38 44	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))$
46	45	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)$
47	20 46	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)$
48	47	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))$
49	48	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)$
50	15 49	mpd	$⊢ φ \to \exists p F Cycles (G) p$

Metamath Proof Explorer

Theorem umgr2cycllem

Proof