frgrwopreglem4a

Description: In a friendship graph any two vertices with different degrees are connected. Alternate version of frgrwopreglem4 without a fixed degree and without using the sets A and B . (Contributed by Alexander van der Vekens, 30-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	frgrwopreglem4a	$⊢ (G \in FriendGraph \land (X \in V \land Y \in V) \land D (X) \neq D (Y)) \to \{X, Y\} \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		fveq2	$⊢ X = Y \to D (X) = D (Y)$
5	4	a1i	$⊢ (X \in V \land Y \in V) \to (X = Y \to D (X) = D (Y))$
6	5	necon3d	$⊢ (X \in V \land Y \in V) \to (D (X) \neq D (Y) \to X \neq Y)$
7	6	imp	$⊢ ((X \in V \land Y \in V) \land D (X) \neq D (Y)) \to X \neq Y$
8	7	3adant1	$⊢ (G \in FriendGraph \land (X \in V \land Y \in V) \land D (X) \neq D (Y)) \to X \neq Y$
9	1 2	frgrncvvdeq	$⊢ G \in FriendGraph \to \forall x \in V \forall y \in (V ∖ \{x\}) (y \notin (G NeighbVtx x) \to D (x) = D (y))$
10		oveq2	$⊢ x = X \to G NeighbVtx x = G NeighbVtx X$
11		neleq2	$⊢ G NeighbVtx x = G NeighbVtx X \to (y \notin (G NeighbVtx x) \leftrightarrow y \notin (G NeighbVtx X))$
12	10 11	syl	$⊢ x = X \to (y \notin (G NeighbVtx x) \leftrightarrow y \notin (G NeighbVtx X))$
13		fveqeq2	$⊢ x = X \to (D (x) = D (y) \leftrightarrow D (X) = D (y))$
14	12 13	imbi12d	$⊢ x = X \to ((y \notin (G NeighbVtx x) \to D (x) = D (y)) \leftrightarrow (y \notin (G NeighbVtx X) \to D (X) = D (y)))$
15		neleq1	$⊢ y = Y \to (y \notin (G NeighbVtx X) \leftrightarrow Y \notin (G NeighbVtx X))$
16		fveq2	$⊢ y = Y \to D (y) = D (Y)$
17	16	eqeq2d	$⊢ y = Y \to (D (X) = D (y) \leftrightarrow D (X) = D (Y))$
18	15 17	imbi12d	$⊢ y = Y \to ((y \notin (G NeighbVtx X) \to D (X) = D (y)) \leftrightarrow (Y \notin (G NeighbVtx X) \to D (X) = D (Y)))$
19		simpll	$⊢ ((X \in V \land Y \in V) \land X \neq Y) \to X \in V$
20		sneq	$⊢ x = X \to \{x\} = \{X\}$
21	20	difeq2d	$⊢ x = X \to V ∖ \{x\} = V ∖ \{X\}$
22	21	adantl	$⊢ (((X \in V \land Y \in V) \land X \neq Y) \land x = X) \to V ∖ \{x\} = V ∖ \{X\}$
23		simpr	$⊢ (X \in V \land Y \in V) \to Y \in V$
24		necom	$⊢ X \neq Y \leftrightarrow Y \neq X$
25	24	biimpi	$⊢ X \neq Y \to Y \neq X$
26	23 25	anim12i	$⊢ ((X \in V \land Y \in V) \land X \neq Y) \to (Y \in V \land Y \neq X)$
27		eldifsn	$⊢ Y \in (V ∖ \{X\}) \leftrightarrow (Y \in V \land Y \neq X)$
28	26 27	sylibr	$⊢ ((X \in V \land Y \in V) \land X \neq Y) \to Y \in (V ∖ \{X\})$
29	14 18 19 22 28	rspc2vd	$⊢ ((X \in V \land Y \in V) \land X \neq Y) \to (\forall x \in V \forall y \in (V ∖ \{x\}) (y \notin (G NeighbVtx x) \to D (x) = D (y)) \to (Y \notin (G NeighbVtx X) \to D (X) = D (Y)))$
30		nnel	$⊢ \neg Y \notin (G NeighbVtx X) \leftrightarrow Y \in (G NeighbVtx X)$
31		nbgrsym	$⊢ Y \in (G NeighbVtx X) \leftrightarrow X \in (G NeighbVtx Y)$
32		frgrusgr	$⊢ G \in FriendGraph \to G \in USGraph$
33	3	nbusgreledg	$⊢ G \in USGraph \to (X \in (G NeighbVtx Y) \leftrightarrow \{X, Y\} \in E)$
34	32 33	syl	$⊢ G \in FriendGraph \to (X \in (G NeighbVtx Y) \leftrightarrow \{X, Y\} \in E)$
35	34	biimpd	$⊢ G \in FriendGraph \to (X \in (G NeighbVtx Y) \to \{X, Y\} \in E)$
36	31 35	biimtrid	$⊢ G \in FriendGraph \to (Y \in (G NeighbVtx X) \to \{X, Y\} \in E)$
37	36	imp	$⊢ (G \in FriendGraph \land Y \in (G NeighbVtx X)) \to \{X, Y\} \in E$
38	37	a1d	$⊢ (G \in FriendGraph \land Y \in (G NeighbVtx X)) \to (D (X) \neq D (Y) \to \{X, Y\} \in E)$
39	38	expcom	$⊢ Y \in (G NeighbVtx X) \to (G \in FriendGraph \to (D (X) \neq D (Y) \to \{X, Y\} \in E))$
40	39	a1d	$⊢ Y \in (G NeighbVtx X) \to (((X \in V \land Y \in V) \land X \neq Y) \to (G \in FriendGraph \to (D (X) \neq D (Y) \to \{X, Y\} \in E)))$
41	30 40	sylbi	$⊢ \neg Y \notin (G NeighbVtx X) \to (((X \in V \land Y \in V) \land X \neq Y) \to (G \in FriendGraph \to (D (X) \neq D (Y) \to \{X, Y\} \in E)))$
42		eqneqall	$⊢ D (X) = D (Y) \to (D (X) \neq D (Y) \to \{X, Y\} \in E)$
43	42	2a1d	$⊢ D (X) = D (Y) \to (((X \in V \land Y \in V) \land X \neq Y) \to (G \in FriendGraph \to (D (X) \neq D (Y) \to \{X, Y\} \in E)))$
44	41 43	ja	$⊢ (Y \notin (G NeighbVtx X) \to D (X) = D (Y)) \to (((X \in V \land Y \in V) \land X \neq Y) \to (G \in FriendGraph \to (D (X) \neq D (Y) \to \{X, Y\} \in E)))$
45	44	com12	$⊢ ((X \in V \land Y \in V) \land X \neq Y) \to ((Y \notin (G NeighbVtx X) \to D (X) = D (Y)) \to (G \in FriendGraph \to (D (X) \neq D (Y) \to \{X, Y\} \in E)))$
46	29 45	syld	$⊢ ((X \in V \land Y \in V) \land X \neq Y) \to (\forall x \in V \forall y \in (V ∖ \{x\}) (y \notin (G NeighbVtx x) \to D (x) = D (y)) \to (G \in FriendGraph \to (D (X) \neq D (Y) \to \{X, Y\} \in E)))$
47	46	com3l	$⊢ \forall x \in V \forall y \in (V ∖ \{x\}) (y \notin (G NeighbVtx x) \to D (x) = D (y)) \to (G \in FriendGraph \to (((X \in V \land Y \in V) \land X \neq Y) \to (D (X) \neq D (Y) \to \{X, Y\} \in E)))$
48	9 47	mpcom	$⊢ G \in FriendGraph \to (((X \in V \land Y \in V) \land X \neq Y) \to (D (X) \neq D (Y) \to \{X, Y\} \in E))$
49	48	expd	$⊢ G \in FriendGraph \to ((X \in V \land Y \in V) \to (X \neq Y \to (D (X) \neq D (Y) \to \{X, Y\} \in E)))$
50	49	com34	$⊢ G \in FriendGraph \to ((X \in V \land Y \in V) \to (D (X) \neq D (Y) \to (X \neq Y \to \{X, Y\} \in E)))$
51	50	3imp	$⊢ (G \in FriendGraph \land (X \in V \land Y \in V) \land D (X) \neq D (Y)) \to (X \neq Y \to \{X, Y\} \in E)$
52	8 51	mpd	$⊢ (G \in FriendGraph \land (X \in V \land Y \in V) \land D (X) \neq D (Y)) \to \{X, Y\} \in E$

Metamath Proof Explorer

Theorem frgrwopreglem4a

Proof