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 ⁡ G iEdg ⁡ 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 ⁡ G v n ⊆ 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 syl5eq ⊢ 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 ⁡ g v n ⊆ e ↔ ∃ e ∈ Edg ⁡ G v n ⊆ e
18 9 17 raleqbidv ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G ∧ Vtx ⁡ g = Vtx ⁡ G ∧ iEdg ⁡ g = iEdg ⁡ G → ∀ n ∈ Vtx ⁡ g ∖ v ∃ e ∈ Edg ⁡ g v n ⊆ e ↔ ∀ n ∈ Vtx ⁡ G ∖ v ∃ e ∈ Edg ⁡ G v n ⊆ 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 ⁡ g v n ⊆ e ↔ ∀ v ∈ Vtx ⁡ G ∀ n ∈ Vtx ⁡ G ∖ v ∃ e ∈ Edg ⁡ G v n ⊆ 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 ⁡ G v n ⊆ e → ∀ v ∈ Vtx ⁡ g ∀ n ∈ Vtx ⁡ g ∖ v ∃ e ∈ Edg ⁡ g v n ⊆ 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 ⁡ g v n ⊆ e
24 23 elv ⊢ g ∈ ComplGraph ↔ ∀ v ∈ Vtx ⁡ g ∀ n ∈ Vtx ⁡ g ∖ v ∃ e ∈ Edg ⁡ g v n ⊆ 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 ⁡ G v n ⊆ e → g ∈ ComplGraph
26 25 expcom ⊢ ∀ v ∈ Vtx ⁡ G ∀ n ∈ Vtx ⁡ G ∖ v ∃ e ∈ Edg ⁡ G v n ⊆ 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 ⁡ G v n ⊆ 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 ⁡ G v n ⊆ 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 → ∀ g Vtx ⁡ 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 ⁡ G iEdg ⁡ G ∈ ComplGraph