konigsbergssiedgwpr

Description: Each subset of the indexed edges of the Königsberg graph G is a word over the pairs of vertices. (Contributed by AV, 28-Feb-2021)

	Ref	Expression
Hypotheses	konigsberg.v	$⊢ V = (0 \dots 3)$
	konigsberg.e	$⊢ E = ⟨“ \{0, 1\} \{0, 2\} \{0, 3\} \{1, 2\} \{1, 2\} \{2, 3\} \{2, 3\} ”⟩$
	konigsberg.g	$⊢ G = ⟨V, E⟩$
Assertion	konigsbergssiedgwpr	$⊢ (A \in Word V \land B \in Word V \land E = A ++ B) \to A \in Word \{x \in 𝒫 V \| \|x\| = 2\}$

Step	Hyp	Ref	Expression
1		konigsberg.v	$⊢ V = (0 \dots 3)$
2		konigsberg.e	$⊢ E = ⟨“ \{0, 1\} \{0, 2\} \{0, 3\} \{1, 2\} \{1, 2\} \{2, 3\} \{2, 3\} ”⟩$
3		konigsberg.g	$⊢ G = ⟨V, E⟩$
4	1 2 3	konigsbergiedgw	$⊢ E \in Word \{x \in 𝒫 V \| \|x\| = 2\}$
5	4	jctr	$⊢ E = A ++ B \to (E = A ++ B \land E \in Word \{x \in 𝒫 V \| \|x\| = 2\})$
6		ccatrcl1	$⊢ (A \in Word V \land B \in Word V \land (E = A ++ B \land E \in Word \{x \in 𝒫 V \| \|x\| = 2\})) \to A \in Word \{x \in 𝒫 V \| \|x\| = 2\}$
7	5 6	syl3an3	$⊢ (A \in Word V \land B \in Word V \land E = A ++ B) \to A \in Word \{x \in 𝒫 V \| \|x\| = 2\}$

Metamath Proof Explorer