frgrwopreglem5a

Description: If a friendship graph has two vertices with the same degree and two other vertices with different degrees, then there is a 4-cycle in the graph. Alternate version of frgrwopreglem5 without a fixed degree and without using the sets A and B . (Contributed by Alexander van der Vekens, 31-Dec-2017) (Revised by AV, 4-Feb-2022)

	Ref	Expression
Hypotheses	frgrncvvdeq.v	$⊢ V = Vtx (G)$
	frgrncvvdeq.d	$⊢ D = VtxDeg (G)$
	frgrwopreglem4a.e	$⊢ E = Edg (G)$
Assertion	frgrwopreglem5a	$⊢ (G \in FriendGraph \land ((A \in V \land X \in V) \land (B \in V \land Y \in V)) \land (D (A) = D (X) \land D (A) \neq D (B) \land D (X) \neq D (Y))) \to ((\{A, B\} \in E \land \{B, X\} \in E) \land (\{X, Y\} \in E \land \{Y, A\} \in E))$

Proof

Step	Hyp	Ref	Expression
1		frgrncvvdeq.v	$⊢ V = Vtx (G)$
2		frgrncvvdeq.d	$⊢ D = VtxDeg (G)$
3		frgrwopreglem4a.e	$⊢ E = Edg (G)$
4		id	$⊢ G \in FriendGraph \to G \in FriendGraph$
5		simpl	$⊢ (A \in V \land X \in V) \to A \in V$
6		simpl	$⊢ (B \in V \land Y \in V) \to B \in V$
7	5 6	anim12i	$⊢ ((A \in V \land X \in V) \land (B \in V \land Y \in V)) \to (A \in V \land B \in V)$
8		simp2	$⊢ (D (A) = D (X) \land D (A) \neq D (B) \land D (X) \neq D (Y)) \to D (A) \neq D (B)$
9	1 2 3	frgrwopreglem4a	$⊢ (G \in FriendGraph \land (A \in V \land B \in V) \land D (A) \neq D (B)) \to \{A, B\} \in E$
10	4 7 8 9	syl3an	$⊢ (G \in FriendGraph \land ((A \in V \land X \in V) \land (B \in V \land Y \in V)) \land (D (A) = D (X) \land D (A) \neq D (B) \land D (X) \neq D (Y))) \to \{A, B\} \in E$
11		simpr	$⊢ (A \in V \land X \in V) \to X \in V$
12	11 6	anim12ci	$⊢ ((A \in V \land X \in V) \land (B \in V \land Y \in V)) \to (B \in V \land X \in V)$
13		pm13.18	$⊢ (D (A) = D (X) \land D (A) \neq D (B)) \to D (X) \neq D (B)$
14	13	3adant3	$⊢ (D (A) = D (X) \land D (A) \neq D (B) \land D (X) \neq D (Y)) \to D (X) \neq D (B)$
15	14	necomd	$⊢ (D (A) = D (X) \land D (A) \neq D (B) \land D (X) \neq D (Y)) \to D (B) \neq D (X)$
16	1 2 3	frgrwopreglem4a	$⊢ (G \in FriendGraph \land (B \in V \land X \in V) \land D (B) \neq D (X)) \to \{B, X\} \in E$
17	4 12 15 16	syl3an	$⊢ (G \in FriendGraph \land ((A \in V \land X \in V) \land (B \in V \land Y \in V)) \land (D (A) = D (X) \land D (A) \neq D (B) \land D (X) \neq D (Y))) \to \{B, X\} \in E$
18		simpr	$⊢ (B \in V \land Y \in V) \to Y \in V$
19	11 18	anim12i	$⊢ ((A \in V \land X \in V) \land (B \in V \land Y \in V)) \to (X \in V \land Y \in V)$
20		simp3	$⊢ (D (A) = D (X) \land D (A) \neq D (B) \land D (X) \neq D (Y)) \to D (X) \neq D (Y)$
21	1 2 3	frgrwopreglem4a	$⊢ (G \in FriendGraph \land (X \in V \land Y \in V) \land D (X) \neq D (Y)) \to \{X, Y\} \in E$
22	4 19 20 21	syl3an	$⊢ (G \in FriendGraph \land ((A \in V \land X \in V) \land (B \in V \land Y \in V)) \land (D (A) = D (X) \land D (A) \neq D (B) \land D (X) \neq D (Y))) \to \{X, Y\} \in E$
23	5 18	anim12ci	$⊢ ((A \in V \land X \in V) \land (B \in V \land Y \in V)) \to (Y \in V \land A \in V)$
24		pm13.181	$⊢ (D (A) = D (X) \land D (X) \neq D (Y)) \to D (A) \neq D (Y)$
25	24	3adant2	$⊢ (D (A) = D (X) \land D (A) \neq D (B) \land D (X) \neq D (Y)) \to D (A) \neq D (Y)$
26	25	necomd	$⊢ (D (A) = D (X) \land D (A) \neq D (B) \land D (X) \neq D (Y)) \to D (Y) \neq D (A)$
27	1 2 3	frgrwopreglem4a	$⊢ (G \in FriendGraph \land (Y \in V \land A \in V) \land D (Y) \neq D (A)) \to \{Y, A\} \in E$
28	4 23 26 27	syl3an	$⊢ (G \in FriendGraph \land ((A \in V \land X \in V) \land (B \in V \land Y \in V)) \land (D (A) = D (X) \land D (A) \neq D (B) \land D (X) \neq D (Y))) \to \{Y, A\} \in E$
29	22 28	jca	$⊢ (G \in FriendGraph \land ((A \in V \land X \in V) \land (B \in V \land Y \in V)) \land (D (A) = D (X) \land D (A) \neq D (B) \land D (X) \neq D (Y))) \to (\{X, Y\} \in E \land \{Y, A\} \in E)$
30	10 17 29	jca31	$⊢ (G \in FriendGraph \land ((A \in V \land X \in V) \land (B \in V \land Y \in V)) \land (D (A) = D (X) \land D (A) \neq D (B) \land D (X) \neq D (Y))) \to ((\{A, B\} \in E \land \{B, X\} \in E) \land (\{X, Y\} \in E \land \{Y, A\} \in E))$

Metamath Proof Explorer

Theorem frgrwopreglem5a

Proof