frgrwopreglem5

Description: Lemma 5 for frgrwopreg . If A as well as B contain at least two vertices, there is a 4-cycle in a friendship graph. This corresponds to statement 6 in Huneke p. 2: "... otherwise, there are two different vertices in A, and they have two common neighbors in B, ...". (Contributed by Alexander van der Vekens, 31-Dec-2017) (Proof shortened by AV, 5-Feb-2022)

	Ref	Expression
Hypotheses	frgrwopreg.v	$⊢ V = Vtx (G)$
	frgrwopreg.d	$⊢ D = VtxDeg (G)$
	frgrwopreg.a	$⊢ A = \{x \in V \| D (x) = K\}$
	frgrwopreg.b	$⊢ B = V ∖ A$
	frgrwopreg.e	$⊢ E = Edg (G)$
Assertion	frgrwopreglem5	$⊢ (G \in FriendGraph \land 1 < \|A\| \land 1 < \|B\|) \to \exists a \in A \exists x \in A \exists b \in B \exists y \in B ((a \neq x \land b \neq y) \land (\{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		frgrwopreg.v	$⊢ V = Vtx (G)$
2		frgrwopreg.d	$⊢ D = VtxDeg (G)$
3		frgrwopreg.a	$⊢ A = \{x \in V \| D (x) = K\}$
4		frgrwopreg.b	$⊢ B = V ∖ A$
5		frgrwopreg.e	$⊢ E = Edg (G)$
6		simpllr	$⊢ (((G \in FriendGraph \land a \neq x) \land (a \in A \land x \in A)) \land (b \in B \land y \in B)) \to a \neq x$
7	6	anim1i	$⊢ ((((G \in FriendGraph \land a \neq x) \land (a \in A \land x \in A)) \land (b \in B \land y \in B)) \land b \neq y) \to (a \neq x \land b \neq y)$
8		simplll	$⊢ (((G \in FriendGraph \land a \neq x) \land (a \in A \land x \in A)) \land (b \in B \land y \in B)) \to G \in FriendGraph$
9		fveqeq2	$⊢ x = a \to (D (x) = K \leftrightarrow D (a) = K)$
10	9 3	elrab2	$⊢ a \in A \leftrightarrow (a \in V \land D (a) = K)$
11	10	simplbi	$⊢ a \in A \to a \in V$
12		rabidim1	$⊢ x \in \{x \in V \| D (x) = K\} \to x \in V$
13	12 3	eleq2s	$⊢ x \in A \to x \in V$
14	11 13	anim12i	$⊢ (a \in A \land x \in A) \to (a \in V \land x \in V)$
15	14	adantl	$⊢ ((G \in FriendGraph \land a \neq x) \land (a \in A \land x \in A)) \to (a \in V \land x \in V)$
16		eldifi	$⊢ b \in (V ∖ A) \to b \in V$
17	16 4	eleq2s	$⊢ b \in B \to b \in V$
18		eldifi	$⊢ y \in (V ∖ A) \to y \in V$
19	18 4	eleq2s	$⊢ y \in B \to y \in V$
20	17 19	anim12i	$⊢ (b \in B \land y \in B) \to (b \in V \land y \in V)$
21	15 20	anim12i	$⊢ (((G \in FriendGraph \land a \neq x) \land (a \in A \land x \in A)) \land (b \in B \land y \in B)) \to ((a \in V \land x \in V) \land (b \in V \land y \in V))$
22	1 2 3 4 5	frgrwopreglem5lem	$⊢ ((a \in A \land x \in A) \land (b \in B \land y \in B)) \to (D (a) = D (x) \land D (a) \neq D (b) \land D (x) \neq D (y))$
23	22	adantll	$⊢ (((G \in FriendGraph \land a \neq x) \land (a \in A \land x \in A)) \land (b \in B \land y \in B)) \to (D (a) = D (x) \land D (a) \neq D (b) \land D (x) \neq D (y))$
24	8 21 23	3jca	$⊢ (((G \in FriendGraph \land a \neq x) \land (a \in A \land x \in A)) \land (b \in B \land y \in B)) \to (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)))$
25	24	adantr	$⊢ ((((G \in FriendGraph \land a \neq x) \land (a \in A \land x \in A)) \land (b \in B \land y \in B)) \land b \neq y) \to (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)))$
26	1 2 5	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))$
27	25 26	syl	$⊢ ((((G \in FriendGraph \land a \neq x) \land (a \in A \land x \in A)) \land (b \in B \land y \in B)) \land b \neq y) \to ((\{a, b\} \in E \land \{b, x\} \in E) \land (\{x, y\} \in E \land \{y, a\} \in E))$
28		3anass	$⊢ ((a \neq x \land b \neq y) \land (\{a, b\} \in E \land \{b, x\} \in E) \land (\{x, y\} \in E \land \{y, a\} \in E)) \leftrightarrow ((a \neq x \land b \neq y) \land ((\{a, b\} \in E \land \{b, x\} \in E) \land (\{x, y\} \in E \land \{y, a\} \in E)))$
29	7 27 28	sylanbrc	$⊢ ((((G \in FriendGraph \land a \neq x) \land (a \in A \land x \in A)) \land (b \in B \land y \in B)) \land b \neq y) \to ((a \neq x \land b \neq y) \land (\{a, b\} \in E \land \{b, x\} \in E) \land (\{x, y\} \in E \land \{y, a\} \in E))$
30	29	ex	$⊢ (((G \in FriendGraph \land a \neq x) \land (a \in A \land x \in A)) \land (b \in B \land y \in B)) \to (b \neq y \to ((a \neq x \land b \neq y) \land (\{a, b\} \in E \land \{b, x\} \in E) \land (\{x, y\} \in E \land \{y, a\} \in E)))$
31	30	reximdvva	$⊢ ((G \in FriendGraph \land a \neq x) \land (a \in A \land x \in A)) \to (\exists b \in B \exists y \in B b \neq y \to \exists b \in B \exists y \in B ((a \neq x \land b \neq y) \land (\{a, b\} \in E \land \{b, x\} \in E) \land (\{x, y\} \in E \land \{y, a\} \in E)))$
32	31	exp31	$⊢ G \in FriendGraph \to (a \neq x \to ((a \in A \land x \in A) \to (\exists b \in B \exists y \in B b \neq y \to \exists b \in B \exists y \in B ((a \neq x \land b \neq y) \land (\{a, b\} \in E \land \{b, x\} \in E) \land (\{x, y\} \in E \land \{y, a\} \in E)))))$
33	32	com24	$⊢ G \in FriendGraph \to (\exists b \in B \exists y \in B b \neq y \to ((a \in A \land x \in A) \to (a \neq x \to \exists b \in B \exists y \in B ((a \neq x \land b \neq y) \land (\{a, b\} \in E \land \{b, x\} \in E) \land (\{x, y\} \in E \land \{y, a\} \in E)))))$
34	33	imp31	$⊢ ((G \in FriendGraph \land \exists b \in B \exists y \in B b \neq y) \land (a \in A \land x \in A)) \to (a \neq x \to \exists b \in B \exists y \in B ((a \neq x \land b \neq y) \land (\{a, b\} \in E \land \{b, x\} \in E) \land (\{x, y\} \in E \land \{y, a\} \in E)))$
35	34	reximdvva	$⊢ (G \in FriendGraph \land \exists b \in B \exists y \in B b \neq y) \to (\exists a \in A \exists x \in A a \neq x \to \exists a \in A \exists x \in A \exists b \in B \exists y \in B ((a \neq x \land b \neq y) \land (\{a, b\} \in E \land \{b, x\} \in E) \land (\{x, y\} \in E \land \{y, a\} \in E)))$
36	35	ex	$⊢ G \in FriendGraph \to (\exists b \in B \exists y \in B b \neq y \to (\exists a \in A \exists x \in A a \neq x \to \exists a \in A \exists x \in A \exists b \in B \exists y \in B ((a \neq x \land b \neq y) \land (\{a, b\} \in E \land \{b, x\} \in E) \land (\{x, y\} \in E \land \{y, a\} \in E))))$
37	36	com13	$⊢ \exists a \in A \exists x \in A a \neq x \to (\exists b \in B \exists y \in B b \neq y \to (G \in FriendGraph \to \exists a \in A \exists x \in A \exists b \in B \exists y \in B ((a \neq x \land b \neq y) \land (\{a, b\} \in E \land \{b, x\} \in E) \land (\{x, y\} \in E \land \{y, a\} \in E))))$
38	37	imp	$⊢ (\exists a \in A \exists x \in A a \neq x \land \exists b \in B \exists y \in B b \neq y) \to (G \in FriendGraph \to \exists a \in A \exists x \in A \exists b \in B \exists y \in B ((a \neq x \land b \neq y) \land (\{a, b\} \in E \land \{b, x\} \in E) \land (\{x, y\} \in E \land \{y, a\} \in E)))$
39	1 2 3 4	frgrwopreglem1	$⊢ (A \in V \land B \in V)$
40		hashgt12el	$⊢ (A \in V \land 1 < \|A\|) \to \exists a \in A \exists x \in A a \neq x$
41	40	ex	$⊢ A \in V \to (1 < \|A\| \to \exists a \in A \exists x \in A a \neq x)$
42		hashgt12el	$⊢ (B \in V \land 1 < \|B\|) \to \exists b \in B \exists y \in B b \neq y$
43	42	ex	$⊢ B \in V \to (1 < \|B\| \to \exists b \in B \exists y \in B b \neq y)$
44	41 43	im2anan9	$⊢ (A \in V \land B \in V) \to ((1 < \|A\| \land 1 < \|B\|) \to (\exists a \in A \exists x \in A a \neq x \land \exists b \in B \exists y \in B b \neq y))$
45	39 44	ax-mp	$⊢ (1 < \|A\| \land 1 < \|B\|) \to (\exists a \in A \exists x \in A a \neq x \land \exists b \in B \exists y \in B b \neq y)$
46	38 45	syl11	$⊢ G \in FriendGraph \to ((1 < \|A\| \land 1 < \|B\|) \to \exists a \in A \exists x \in A \exists b \in B \exists y \in B ((a \neq x \land b \neq y) \land (\{a, b\} \in E \land \{b, x\} \in E) \land (\{x, y\} \in E \land \{y, a\} \in E)))$
47	46	3impib	$⊢ (G \in FriendGraph \land 1 < \|A\| \land 1 < \|B\|) \to \exists a \in A \exists x \in A \exists b \in B \exists y \in B ((a \neq x \land b \neq y) \land (\{a, b\} \in E \land \{b, x\} \in E) \land (\{x, y\} \in E \land \{y, a\} \in E))$

Metamath Proof Explorer

Theorem frgrwopreglem5

Proof