upgrex

Description: An edge is an unordered pair of vertices. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 10-Oct-2020)

	Ref	Expression
Hypotheses	isupgr.v	$⊢ V = Vtx (G)$
	isupgr.e	$⊢ E = iEdg (G)$
Assertion	upgrex	$⊢ (G \in UPGraph \land E Fn A \land F \in A) \to \exists x \in V \exists y \in V E (F) = \{x, y\}$

Proof

Step	Hyp	Ref	Expression
1		isupgr.v	$⊢ V = Vtx (G)$
2		isupgr.e	$⊢ E = iEdg (G)$
3	1 2	upgrn0	$⊢ (G \in UPGraph \land E Fn A \land F \in A) \to E (F) \neq \emptyset$
4		n0	$⊢ E (F) \neq \emptyset \leftrightarrow \exists x x \in E (F)$
5	3 4	sylib	$⊢ (G \in UPGraph \land E Fn A \land F \in A) \to \exists x x \in E (F)$
6		simp1	$⊢ (G \in UPGraph \land E Fn A \land F \in A) \to G \in UPGraph$
7		fndm	$⊢ E Fn A \to dom E = A$
8	7	eqcomd	$⊢ E Fn A \to A = dom E$
9	8	eleq2d	$⊢ E Fn A \to (F \in A \leftrightarrow F \in dom E)$
10	9	biimpd	$⊢ E Fn A \to (F \in A \to F \in dom E)$
11	10	a1i	$⊢ G \in UPGraph \to (E Fn A \to (F \in A \to F \in dom E))$
12	11	3imp	$⊢ (G \in UPGraph \land E Fn A \land F \in A) \to F \in dom E$
13	1 2	upgrss	$⊢ (G \in UPGraph \land F \in dom E) \to E (F) \subseteq V$
14	6 12 13	syl2anc	$⊢ (G \in UPGraph \land E Fn A \land F \in A) \to E (F) \subseteq V$
15	14	sselda	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land x \in E (F)) \to x \in V$
16	15	adantr	$⊢ (((G \in UPGraph \land E Fn A \land F \in A) \land x \in E (F)) \land E (F) ∖ \{x\} = \emptyset) \to x \in V$
17		simpr	$⊢ (((G \in UPGraph \land E Fn A \land F \in A) \land x \in E (F)) \land E (F) ∖ \{x\} = \emptyset) \to E (F) ∖ \{x\} = \emptyset$
18		ssdif0	$⊢ E (F) \subseteq \{x\} \leftrightarrow E (F) ∖ \{x\} = \emptyset$
19	17 18	sylibr	$⊢ (((G \in UPGraph \land E Fn A \land F \in A) \land x \in E (F)) \land E (F) ∖ \{x\} = \emptyset) \to E (F) \subseteq \{x\}$
20		simpr	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land x \in E (F)) \to x \in E (F)$
21	20	snssd	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land x \in E (F)) \to \{x\} \subseteq E (F)$
22	21	adantr	$⊢ (((G \in UPGraph \land E Fn A \land F \in A) \land x \in E (F)) \land E (F) ∖ \{x\} = \emptyset) \to \{x\} \subseteq E (F)$
23	19 22	eqssd	$⊢ (((G \in UPGraph \land E Fn A \land F \in A) \land x \in E (F)) \land E (F) ∖ \{x\} = \emptyset) \to E (F) = \{x\}$
24		preq2	$⊢ y = x \to \{x, y\} = \{x, x\}$
25		dfsn2	$⊢ \{x\} = \{x, x\}$
26	24 25	eqtr4di	$⊢ y = x \to \{x, y\} = \{x\}$
27	26	rspceeqv	$⊢ (x \in V \land E (F) = \{x\}) \to \exists y \in V E (F) = \{x, y\}$
28	16 23 27	syl2anc	$⊢ (((G \in UPGraph \land E Fn A \land F \in A) \land x \in E (F)) \land E (F) ∖ \{x\} = \emptyset) \to \exists y \in V E (F) = \{x, y\}$
29		n0	$⊢ E (F) ∖ \{x\} \neq \emptyset \leftrightarrow \exists y y \in (E (F) ∖ \{x\})$
30	14	adantr	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to E (F) \subseteq V$
31		simprr	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to y \in (E (F) ∖ \{x\})$
32	31	eldifad	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to y \in E (F)$
33	30 32	sseldd	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to y \in V$
34	1 2	upgrfi	$⊢ (G \in UPGraph \land E Fn A \land F \in A) \to E (F) \in Fin$
35	34	adantr	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to E (F) \in Fin$
36		simprl	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to x \in E (F)$
37	36 32	prssd	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to \{x, y\} \subseteq E (F)$
38		fvex	$⊢ E (F) \in V$
39		ssdomg	$⊢ E (F) \in V \to (\{x, y\} \subseteq E (F) \to \{x, y\} ≼ E (F))$
40	38 37 39	mpsyl	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to \{x, y\} ≼ E (F)$
41	1 2	upgrle	$⊢ (G \in UPGraph \land E Fn A \land F \in A) \to \|E (F)\| \leq 2$
42	41	adantr	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to \|E (F)\| \leq 2$
43		eldifsni	$⊢ y \in (E (F) ∖ \{x\}) \to y \neq x$
44	43	ad2antll	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to y \neq x$
45	44	necomd	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to x \neq y$
46		hashprg	$⊢ (x \in V \land y \in V) \to (x \neq y \leftrightarrow \|\{x, y\}\| = 2)$
47	46	el2v	$⊢ x \neq y \leftrightarrow \|\{x, y\}\| = 2$
48	45 47	sylib	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to \|\{x, y\}\| = 2$
49	42 48	breqtrrd	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to \|E (F)\| \leq \|\{x, y\}\|$
50		prfi	$⊢ \{x, y\} \in Fin$
51		hashdom	$⊢ (E (F) \in Fin \land \{x, y\} \in Fin) \to (\|E (F)\| \leq \|\{x, y\}\| \leftrightarrow E (F) ≼ \{x, y\})$
52	35 50 51	sylancl	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to (\|E (F)\| \leq \|\{x, y\}\| \leftrightarrow E (F) ≼ \{x, y\})$
53	49 52	mpbid	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to E (F) ≼ \{x, y\}$
54		sbth	$⊢ (\{x, y\} ≼ E (F) \land E (F) ≼ \{x, y\}) \to \{x, y\} \approx E (F)$
55	40 53 54	syl2anc	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to \{x, y\} \approx E (F)$
56		fisseneq	$⊢ (E (F) \in Fin \land \{x, y\} \subseteq E (F) \land \{x, y\} \approx E (F)) \to \{x, y\} = E (F)$
57	35 37 55 56	syl3anc	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to \{x, y\} = E (F)$
58	57	eqcomd	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to E (F) = \{x, y\}$
59	33 58	jca	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land (x \in E (F) \land y \in (E (F) ∖ \{x\}))) \to (y \in V \land E (F) = \{x, y\})$
60	59	expr	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land x \in E (F)) \to (y \in (E (F) ∖ \{x\}) \to (y \in V \land E (F) = \{x, y\}))$
61	60	eximdv	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land x \in E (F)) \to (\exists y y \in (E (F) ∖ \{x\}) \to \exists y (y \in V \land E (F) = \{x, y\}))$
62	61	imp	$⊢ (((G \in UPGraph \land E Fn A \land F \in A) \land x \in E (F)) \land \exists y y \in (E (F) ∖ \{x\})) \to \exists y (y \in V \land E (F) = \{x, y\})$
63		df-rex	$⊢ \exists y \in V E (F) = \{x, y\} \leftrightarrow \exists y (y \in V \land E (F) = \{x, y\})$
64	62 63	sylibr	$⊢ (((G \in UPGraph \land E Fn A \land F \in A) \land x \in E (F)) \land \exists y y \in (E (F) ∖ \{x\})) \to \exists y \in V E (F) = \{x, y\}$
65	29 64	sylan2b	$⊢ (((G \in UPGraph \land E Fn A \land F \in A) \land x \in E (F)) \land E (F) ∖ \{x\} \neq \emptyset) \to \exists y \in V E (F) = \{x, y\}$
66	28 65	pm2.61dane	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land x \in E (F)) \to \exists y \in V E (F) = \{x, y\}$
67	15 66	jca	$⊢ ((G \in UPGraph \land E Fn A \land F \in A) \land x \in E (F)) \to (x \in V \land \exists y \in V E (F) = \{x, y\})$
68	67	ex	$⊢ (G \in UPGraph \land E Fn A \land F \in A) \to (x \in E (F) \to (x \in V \land \exists y \in V E (F) = \{x, y\}))$
69	68	eximdv	$⊢ (G \in UPGraph \land E Fn A \land F \in A) \to (\exists x x \in E (F) \to \exists x (x \in V \land \exists y \in V E (F) = \{x, y\}))$
70	5 69	mpd	$⊢ (G \in UPGraph \land E Fn A \land F \in A) \to \exists x (x \in V \land \exists y \in V E (F) = \{x, y\})$
71		df-rex	$⊢ \exists x \in V \exists y \in V E (F) = \{x, y\} \leftrightarrow \exists x (x \in V \land \exists y \in V E (F) = \{x, y\})$
72	70 71	sylibr	$⊢ (G \in UPGraph \land E Fn A \land F \in A) \to \exists x \in V \exists y \in V E (F) = \{x, y\}$

Metamath Proof Explorer

Theorem upgrex

Proof