cusgrexi

Description: An arbitrary set V regarded as set of vertices together with the set of pairs of elements of this set regarded as edges is a complete simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 5-Nov-2020) (Proof shortened by AV, 14-Feb-2022)

		Ref	Expression
	Hypothesis	usgrexi.p	$⊢ P = \{x \in 𝒫 V \| \|x\| = 2\}$
	Assertion	cusgrexi	$⊢ V \in W \to ⟨V, {I ↾}_{P}⟩ \in ComplUSGraph$

Proof

Step	Hyp	Ref	Expression
1		usgrexi.p	$⊢ P = \{x \in 𝒫 V \| \|x\| = 2\}$
2	1	usgrexi	$⊢ V \in W \to ⟨V, {I ↾}_{P}⟩ \in USGraph$
3	1	cusgrexilem1	$⊢ V \in W \to {I ↾}_{P} \in V$
4		opvtxfv	$⊢ (V \in W \land {I ↾}_{P} \in V) \to Vtx (⟨V, {I ↾}_{P}⟩) = V$
5	4	eqcomd	$⊢ (V \in W \land {I ↾}_{P} \in V) \to V = Vtx (⟨V, {I ↾}_{P}⟩)$
6	3 5	mpdan	$⊢ V \in W \to V = Vtx (⟨V, {I ↾}_{P}⟩)$
7	6	eleq2d	$⊢ V \in W \to (v \in V \leftrightarrow v \in Vtx (⟨V, {I ↾}_{P}⟩))$
8	7	biimpa	$⊢ (V \in W \land v \in V) \to v \in Vtx (⟨V, {I ↾}_{P}⟩)$
9		eldifi	$⊢ n \in (V ∖ \{v\}) \to n \in V$
10	9	adantl	$⊢ ((V \in W \land v \in V) \land n \in (V ∖ \{v\})) \to n \in V$
11	3 4	mpdan	$⊢ V \in W \to Vtx (⟨V, {I ↾}_{P}⟩) = V$
12	11	eleq2d	$⊢ V \in W \to (n \in Vtx (⟨V, {I ↾}_{P}⟩) \leftrightarrow n \in V)$
13	12	ad2antrr	$⊢ ((V \in W \land v \in V) \land n \in (V ∖ \{v\})) \to (n \in Vtx (⟨V, {I ↾}_{P}⟩) \leftrightarrow n \in V)$
14	10 13	mpbird	$⊢ ((V \in W \land v \in V) \land n \in (V ∖ \{v\})) \to n \in Vtx (⟨V, {I ↾}_{P}⟩)$
15		simplr	$⊢ ((V \in W \land v \in V) \land n \in (V ∖ \{v\})) \to v \in V$
16	11	eleq2d	$⊢ V \in W \to (v \in Vtx (⟨V, {I ↾}_{P}⟩) \leftrightarrow v \in V)$
17	16	ad2antrr	$⊢ ((V \in W \land v \in V) \land n \in (V ∖ \{v\})) \to (v \in Vtx (⟨V, {I ↾}_{P}⟩) \leftrightarrow v \in V)$
18	15 17	mpbird	$⊢ ((V \in W \land v \in V) \land n \in (V ∖ \{v\})) \to v \in Vtx (⟨V, {I ↾}_{P}⟩)$
19	14 18	jca	$⊢ ((V \in W \land v \in V) \land n \in (V ∖ \{v\})) \to (n \in Vtx (⟨V, {I ↾}_{P}⟩) \land v \in Vtx (⟨V, {I ↾}_{P}⟩))$
20		eldifsni	$⊢ n \in (V ∖ \{v\}) \to n \neq v$
21	20	adantl	$⊢ ((V \in W \land v \in V) \land n \in (V ∖ \{v\})) \to n \neq v$
22	1	cusgrexilem2	$⊢ ((V \in W \land v \in V) \land n \in (V ∖ \{v\})) \to \exists e \in ran ({I ↾}_{P}) \{v, n\} \subseteq e$
23		edgval	$⊢ Edg (⟨V, {I ↾}_{P}⟩) = ran iEdg (⟨V, {I ↾}_{P}⟩)$
24		opiedgfv	$⊢ (V \in W \land {I ↾}_{P} \in V) \to iEdg (⟨V, {I ↾}_{P}⟩) = {I ↾}_{P}$
25	3 24	mpdan	$⊢ V \in W \to iEdg (⟨V, {I ↾}_{P}⟩) = {I ↾}_{P}$
26	25	rneqd	$⊢ V \in W \to ran iEdg (⟨V, {I ↾}_{P}⟩) = ran ({I ↾}_{P})$
27	23 26	syl5eq	$⊢ V \in W \to Edg (⟨V, {I ↾}_{P}⟩) = ran ({I ↾}_{P})$
28	27	rexeqdv	$⊢ V \in W \to (\exists e \in Edg (⟨V, {I ↾}_{P}⟩) \{v, n\} \subseteq e \leftrightarrow \exists e \in ran ({I ↾}_{P}) \{v, n\} \subseteq e)$
29	28	ad2antrr	$⊢ ((V \in W \land v \in V) \land n \in (V ∖ \{v\})) \to (\exists e \in Edg (⟨V, {I ↾}_{P}⟩) \{v, n\} \subseteq e \leftrightarrow \exists e \in ran ({I ↾}_{P}) \{v, n\} \subseteq e)$
30	22 29	mpbird	$⊢ ((V \in W \land v \in V) \land n \in (V ∖ \{v\})) \to \exists e \in Edg (⟨V, {I ↾}_{P}⟩) \{v, n\} \subseteq e$
31		eqid	$⊢ Vtx (⟨V, {I ↾}_{P}⟩) = Vtx (⟨V, {I ↾}_{P}⟩)$
32		eqid	$⊢ Edg (⟨V, {I ↾}_{P}⟩) = Edg (⟨V, {I ↾}_{P}⟩)$
33	31 32	nbgrel	$⊢ n \in (⟨V, {I ↾}_{P}⟩ NeighbVtx v) \leftrightarrow ((n \in Vtx (⟨V, {I ↾}_{P}⟩) \land v \in Vtx (⟨V, {I ↾}_{P}⟩)) \land n \neq v \land \exists e \in Edg (⟨V, {I ↾}_{P}⟩) \{v, n\} \subseteq e)$
34	19 21 30 33	syl3anbrc	$⊢ ((V \in W \land v \in V) \land n \in (V ∖ \{v\})) \to n \in (⟨V, {I ↾}_{P}⟩ NeighbVtx v)$
35	34	ralrimiva	$⊢ (V \in W \land v \in V) \to \forall n \in (V ∖ \{v\}) n \in (⟨V, {I ↾}_{P}⟩ NeighbVtx v)$
36	11	adantr	$⊢ (V \in W \land v \in V) \to Vtx (⟨V, {I ↾}_{P}⟩) = V$
37	36	difeq1d	$⊢ (V \in W \land v \in V) \to Vtx (⟨V, {I ↾}_{P}⟩) ∖ \{v\} = V ∖ \{v\}$
38	37	raleqdv	$⊢ (V \in W \land v \in V) \to (\forall n \in (Vtx (⟨V, {I ↾}_{P}⟩) ∖ \{v\}) n \in (⟨V, {I ↾}_{P}⟩ NeighbVtx v) \leftrightarrow \forall n \in (V ∖ \{v\}) n \in (⟨V, {I ↾}_{P}⟩ NeighbVtx v))$
39	35 38	mpbird	$⊢ (V \in W \land v \in V) \to \forall n \in (Vtx (⟨V, {I ↾}_{P}⟩) ∖ \{v\}) n \in (⟨V, {I ↾}_{P}⟩ NeighbVtx v)$
40	31	uvtxel	$⊢ v \in UnivVtx (⟨V, {I ↾}_{P}⟩) \leftrightarrow (v \in Vtx (⟨V, {I ↾}_{P}⟩) \land \forall n \in (Vtx (⟨V, {I ↾}_{P}⟩) ∖ \{v\}) n \in (⟨V, {I ↾}_{P}⟩ NeighbVtx v))$
41	8 39 40	sylanbrc	$⊢ (V \in W \land v \in V) \to v \in UnivVtx (⟨V, {I ↾}_{P}⟩)$
42	41	ralrimiva	$⊢ V \in W \to \forall v \in V v \in UnivVtx (⟨V, {I ↾}_{P}⟩)$
43	11	raleqdv	$⊢ V \in W \to (\forall v \in Vtx (⟨V, {I ↾}_{P}⟩) v \in UnivVtx (⟨V, {I ↾}_{P}⟩) \leftrightarrow \forall v \in V v \in UnivVtx (⟨V, {I ↾}_{P}⟩))$
44	42 43	mpbird	$⊢ V \in W \to \forall v \in Vtx (⟨V, {I ↾}_{P}⟩) v \in UnivVtx (⟨V, {I ↾}_{P}⟩)$
45		opex	$⊢ ⟨V, {I ↾}_{P}⟩ \in V$
46	31	iscplgr	$⊢ ⟨V, {I ↾}_{P}⟩ \in V \to (⟨V, {I ↾}_{P}⟩ \in ComplGraph \leftrightarrow \forall v \in Vtx (⟨V, {I ↾}_{P}⟩) v \in UnivVtx (⟨V, {I ↾}_{P}⟩))$
47	45 46	mp1i	$⊢ V \in W \to (⟨V, {I ↾}_{P}⟩ \in ComplGraph \leftrightarrow \forall v \in Vtx (⟨V, {I ↾}_{P}⟩) v \in UnivVtx (⟨V, {I ↾}_{P}⟩))$
48	44 47	mpbird	$⊢ V \in W \to ⟨V, {I ↾}_{P}⟩ \in ComplGraph$
49		iscusgr	$⊢ ⟨V, {I ↾}_{P}⟩ \in ComplUSGraph \leftrightarrow (⟨V, {I ↾}_{P}⟩ \in USGraph \land ⟨V, {I ↾}_{P}⟩ \in ComplGraph)$
50	2 48 49	sylanbrc	$⊢ V \in W \to ⟨V, {I ↾}_{P}⟩ \in ComplUSGraph$

Metamath Proof Explorer

Theorem cusgrexi

Proof