Metamath Proof Explorer

Theorem cplgrop

Description: A complete graph represented by an ordered pair. (Contributed by AV, 10-Nov-2020)

Ref Expression
Assertion cplgrop ⊢G∈ComplGraph→Vtx⁡GiEdg⁡G∈ComplGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 eqid ⊢Edg⁡G=Edg⁡G
3 1 2 iscplgredg ⊢G∈ComplGraph→G∈ComplGraph↔∀v∈Vtx⁡G∀n∈Vtx⁡G∖v∃e∈Edg⁡Gvn⊆e
4 edgval ⊢Edg⁡G=ran⁡iEdg⁡G
5 4 a1i ⊢G∈ComplGraph→Edg⁡G=ran⁡iEdg⁡G
6 simpl ⊢Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→Vtx⁡g=Vtx⁡G
7 6 adantl ⊢Edg⁡G=ran⁡iEdg⁡G∧Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→Vtx⁡g=Vtx⁡G
8 6 difeq1d ⊢Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→Vtx⁡g∖v=Vtx⁡G∖v
9 8 adantl ⊢Edg⁡G=ran⁡iEdg⁡G∧Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→Vtx⁡g∖v=Vtx⁡G∖v
10 edgval ⊢Edg⁡g=ran⁡iEdg⁡g
11 simpr ⊢Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→iEdg⁡g=iEdg⁡G
12 11 rneqd ⊢Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→ran⁡iEdg⁡g=ran⁡iEdg⁡G
13 10 12 eqtrid ⊢Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→Edg⁡g=ran⁡iEdg⁡G
14 13 adantl ⊢Edg⁡G=ran⁡iEdg⁡G∧Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→Edg⁡g=ran⁡iEdg⁡G
15 simpl ⊢Edg⁡G=ran⁡iEdg⁡G∧Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→Edg⁡G=ran⁡iEdg⁡G
16 14 15 eqtr4d ⊢Edg⁡G=ran⁡iEdg⁡G∧Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→Edg⁡g=Edg⁡G
17 16 rexeqdv ⊢Edg⁡G=ran⁡iEdg⁡G∧Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→∃e∈Edg⁡gvn⊆e↔∃e∈Edg⁡Gvn⊆e
18 9 17 raleqbidv ⊢Edg⁡G=ran⁡iEdg⁡G∧Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→∀n∈Vtx⁡g∖v∃e∈Edg⁡gvn⊆e↔∀n∈Vtx⁡G∖v∃e∈Edg⁡Gvn⊆e
19 7 18 raleqbidv ⊢Edg⁡G=ran⁡iEdg⁡G∧Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→∀v∈Vtx⁡g∀n∈Vtx⁡g∖v∃e∈Edg⁡gvn⊆e↔∀v∈Vtx⁡G∀n∈Vtx⁡G∖v∃e∈Edg⁡Gvn⊆e
20 19 biimpar ⊢Edg⁡G=ran⁡iEdg⁡G∧Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G∧∀v∈Vtx⁡G∀n∈Vtx⁡G∖v∃e∈Edg⁡Gvn⊆e→∀v∈Vtx⁡g∀n∈Vtx⁡g∖v∃e∈Edg⁡gvn⊆e
21 eqid ⊢Vtx⁡g=Vtx⁡g
22 eqid ⊢Edg⁡g=Edg⁡g
23 21 22 iscplgredg ⊢g∈V→g∈ComplGraph↔∀v∈Vtx⁡g∀n∈Vtx⁡g∖v∃e∈Edg⁡gvn⊆e
24 23 elv ⊢g∈ComplGraph↔∀v∈Vtx⁡g∀n∈Vtx⁡g∖v∃e∈Edg⁡gvn⊆e
25 20 24 sylibr ⊢Edg⁡G=ran⁡iEdg⁡G∧Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G∧∀v∈Vtx⁡G∀n∈Vtx⁡G∖v∃e∈Edg⁡Gvn⊆e→g∈ComplGraph
26 25 expcom ⊢∀v∈Vtx⁡G∀n∈Vtx⁡G∖v∃e∈Edg⁡Gvn⊆e→Edg⁡G=ran⁡iEdg⁡G∧Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→g∈ComplGraph
27 26 expd ⊢∀v∈Vtx⁡G∀n∈Vtx⁡G∖v∃e∈Edg⁡Gvn⊆e→Edg⁡G=ran⁡iEdg⁡G→Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→g∈ComplGraph
28 5 27 syl5com ⊢G∈ComplGraph→∀v∈Vtx⁡G∀n∈Vtx⁡G∖v∃e∈Edg⁡Gvn⊆e→Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→g∈ComplGraph
29 3 28 sylbid ⊢G∈ComplGraph→G∈ComplGraph→Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→g∈ComplGraph
30 29 pm2.43i ⊢G∈ComplGraph→Vtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→g∈ComplGraph
31 30 alrimiv ⊢G∈ComplGraph→∀gVtx⁡g=Vtx⁡G∧iEdg⁡g=iEdg⁡G→g∈ComplGraph
32 fvexd ⊢G∈ComplGraph→Vtx⁡G∈V
33 fvexd ⊢G∈ComplGraph→iEdg⁡G∈V
34 31 32 33 gropeld ⊢G∈ComplGraph→Vtx⁡GiEdg⁡G∈ComplGraph