structtocusgr

Description: Any (extensible) structure with a base set can be made a complete simple graph with the set of pairs of elements of the base set regarded as edges. (Contributed by AV, 10-Nov-2021) (Revised by AV, 17-Nov-2021) (Proof shortened by AV, 14-Feb-2022)

	Ref	Expression
Hypotheses	structtousgr.p	$⊢ P = \{x \in 𝒫 {Base}_{S} \| \|x\| = 2\}$
	structtousgr.s	$⊢ φ \to S Struct X$
	structtousgr.g	$⊢ G = S sSet ⟨ef (ndx), {I ↾}_{P}⟩$
	structtousgr.b	$⊢ φ \to {Base}_{ndx} \in dom S$
Assertion	structtocusgr	$⊢ φ \to G \in ComplUSGraph$

Proof

Step	Hyp	Ref	Expression
1		structtousgr.p	$⊢ P = \{x \in 𝒫 {Base}_{S} \| \|x\| = 2\}$
2		structtousgr.s	$⊢ φ \to S Struct X$
3		structtousgr.g	$⊢ G = S sSet ⟨ef (ndx), {I ↾}_{P}⟩$
4		structtousgr.b	$⊢ φ \to {Base}_{ndx} \in dom S$
5	1 2 3 4	structtousgr	$⊢ φ \to G \in USGraph$
6		simpr	$⊢ (φ \land v \in Vtx (G)) \to v \in Vtx (G)$
7		eldifi	$⊢ n \in (Vtx (G) ∖ \{v\}) \to n \in Vtx (G)$
8	6 7	anim12ci	$⊢ ((φ \land v \in Vtx (G)) \land n \in (Vtx (G) ∖ \{v\})) \to (n \in Vtx (G) \land v \in Vtx (G))$
9		eldifsni	$⊢ n \in (Vtx (G) ∖ \{v\}) \to n \neq v$
10	9	adantl	$⊢ ((φ \land v \in Vtx (G)) \land n \in (Vtx (G) ∖ \{v\})) \to n \neq v$
11		fvexd	$⊢ ((φ \land v \in Vtx (G)) \land n \in (Vtx (G) ∖ \{v\})) \to {Base}_{S} \in V$
12	3	fveq2i	$⊢ Vtx (G) = Vtx (S sSet ⟨ef (ndx), {I ↾}_{P}⟩)$
13		eqid	$⊢ ef (ndx) = ef (ndx)$
14		fvex	$⊢ {Base}_{S} \in V$
15	1	cusgrexilem1	$⊢ {Base}_{S} \in V \to {I ↾}_{P} \in V$
16	14 15	mp1i	$⊢ φ \to {I ↾}_{P} \in V$
17	13 2 4 16	setsvtx	$⊢ φ \to Vtx (S sSet ⟨ef (ndx), {I ↾}_{P}⟩) = {Base}_{S}$
18	12 17	eqtrid	$⊢ φ \to Vtx (G) = {Base}_{S}$
19	18	eleq2d	$⊢ φ \to (v \in Vtx (G) \leftrightarrow v \in {Base}_{S})$
20	19	biimpa	$⊢ (φ \land v \in Vtx (G)) \to v \in {Base}_{S}$
21	20	adantr	$⊢ ((φ \land v \in Vtx (G)) \land n \in (Vtx (G) ∖ \{v\})) \to v \in {Base}_{S}$
22	18	difeq1d	$⊢ φ \to Vtx (G) ∖ \{v\} = {Base}_{S} ∖ \{v\}$
23	22	eleq2d	$⊢ φ \to (n \in (Vtx (G) ∖ \{v\}) \leftrightarrow n \in ({Base}_{S} ∖ \{v\}))$
24	23	biimpd	$⊢ φ \to (n \in (Vtx (G) ∖ \{v\}) \to n \in ({Base}_{S} ∖ \{v\}))$
25	24	adantr	$⊢ (φ \land v \in Vtx (G)) \to (n \in (Vtx (G) ∖ \{v\}) \to n \in ({Base}_{S} ∖ \{v\}))$
26	25	imp	$⊢ ((φ \land v \in Vtx (G)) \land n \in (Vtx (G) ∖ \{v\})) \to n \in ({Base}_{S} ∖ \{v\})$
27	1	cusgrexilem2	$⊢ (({Base}_{S} \in V \land v \in {Base}_{S}) \land n \in ({Base}_{S} ∖ \{v\})) \to \exists e \in ran ({I ↾}_{P}) \{v, n\} \subseteq e$
28	11 21 26 27	syl21anc	$⊢ ((φ \land v \in Vtx (G)) \land n \in (Vtx (G) ∖ \{v\})) \to \exists e \in ran ({I ↾}_{P}) \{v, n\} \subseteq e$
29		edgval	$⊢ Edg (G) = ran iEdg (G)$
30	3	fveq2i	$⊢ iEdg (G) = iEdg (S sSet ⟨ef (ndx), {I ↾}_{P}⟩)$
31	13 2 4 16	setsiedg	$⊢ φ \to iEdg (S sSet ⟨ef (ndx), {I ↾}_{P}⟩) = {I ↾}_{P}$
32	30 31	eqtrid	$⊢ φ \to iEdg (G) = {I ↾}_{P}$
33	32	rneqd	$⊢ φ \to ran iEdg (G) = ran ({I ↾}_{P})$
34	29 33	eqtrid	$⊢ φ \to Edg (G) = ran ({I ↾}_{P})$
35	34	rexeqdv	$⊢ φ \to (\exists e \in Edg (G) \{v, n\} \subseteq e \leftrightarrow \exists e \in ran ({I ↾}_{P}) \{v, n\} \subseteq e)$
36	35	ad2antrr	$⊢ ((φ \land v \in Vtx (G)) \land n \in (Vtx (G) ∖ \{v\})) \to (\exists e \in Edg (G) \{v, n\} \subseteq e \leftrightarrow \exists e \in ran ({I ↾}_{P}) \{v, n\} \subseteq e)$
37	28 36	mpbird	$⊢ ((φ \land v \in Vtx (G)) \land n \in (Vtx (G) ∖ \{v\})) \to \exists e \in Edg (G) \{v, n\} \subseteq e$
38		eqid	$⊢ Vtx (G) = Vtx (G)$
39		eqid	$⊢ Edg (G) = Edg (G)$
40	38 39	nbgrel	$⊢ n \in (G NeighbVtx v) \leftrightarrow ((n \in Vtx (G) \land v \in Vtx (G)) \land n \neq v \land \exists e \in Edg (G) \{v, n\} \subseteq e)$
41	8 10 37 40	syl3anbrc	$⊢ ((φ \land v \in Vtx (G)) \land n \in (Vtx (G) ∖ \{v\})) \to n \in (G NeighbVtx v)$
42	41	ralrimiva	$⊢ (φ \land v \in Vtx (G)) \to \forall n \in (Vtx (G) ∖ \{v\}) n \in (G NeighbVtx v)$
43	38	uvtxel	$⊢ v \in UnivVtx (G) \leftrightarrow (v \in Vtx (G) \land \forall n \in (Vtx (G) ∖ \{v\}) n \in (G NeighbVtx v))$
44	6 42 43	sylanbrc	$⊢ (φ \land v \in Vtx (G)) \to v \in UnivVtx (G)$
45	44	ralrimiva	$⊢ φ \to \forall v \in Vtx (G) v \in UnivVtx (G)$
46	5	elexd	$⊢ φ \to G \in V$
47	38	iscplgr	$⊢ G \in V \to (G \in ComplGraph \leftrightarrow \forall v \in Vtx (G) v \in UnivVtx (G))$
48	46 47	syl	$⊢ φ \to (G \in ComplGraph \leftrightarrow \forall v \in Vtx (G) v \in UnivVtx (G))$
49	45 48	mpbird	$⊢ φ \to G \in ComplGraph$
50		iscusgr	$⊢ G \in ComplUSGraph \leftrightarrow (G \in USGraph \land G \in ComplGraph)$
51	5 49 50	sylanbrc	$⊢ φ \to G \in ComplUSGraph$

Metamath Proof Explorer

Theorem structtocusgr

Proof