Metamath Proof Explorer

Theorem usgredgsscusgredg

Description: A simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11-Jan-2018) (Revised by AV, 13-Nov-2020)

Ref Expression
Hypotheses fusgrmaxsize.v ⊢V=Vtx⁡G
fusgrmaxsize.e ⊢E=Edg⁡G
usgrsscusgra.h ⊢V=Vtx⁡H
usgrsscusgra.f ⊢F=Edg⁡H
Assertion usgredgsscusgredg ⊢G∈USGraph∧H∈ComplUSGraph→E⊆F

Proof

Step Hyp Ref Expression
1 fusgrmaxsize.v ⊢V=Vtx⁡G
2 fusgrmaxsize.e ⊢E=Edg⁡G
3 usgrsscusgra.h ⊢V=Vtx⁡H
4 usgrsscusgra.f ⊢F=Edg⁡H
5 1 2 usgredg ⊢G∈USGraph∧e∈E→∃a∈V∃b∈Va≠b∧e=ab
6 3 4 iscusgredg ⊢H∈ComplUSGraph↔H∈USGraph∧∀k∈V∀n∈V∖knk∈F
7 sneq ⊢k=a→k=a
8 7 difeq2d ⊢k=a→V∖k=V∖a
9 preq2 ⊢k=a→nk=na
10 9 eleq1d ⊢k=a→nk∈F↔na∈F
11 8 10 raleqbidv ⊢k=a→∀n∈V∖knk∈F↔∀n∈V∖ana∈F
12 11 rspcv ⊢a∈V→∀k∈V∀n∈V∖knk∈F→∀n∈V∖ana∈F
13 simpl ⊢a≠b∧e=ab→a≠b
14 13 necomd ⊢a≠b∧e=ab→b≠a
15 14 anim2i ⊢b∈V∧a≠b∧e=ab→b∈V∧b≠a
16 eldifsn ⊢b∈V∖a↔b∈V∧b≠a
17 15 16 sylibr ⊢b∈V∧a≠b∧e=ab→b∈V∖a
18 preq1 ⊢n=b→na=ba
19 18 eleq1d ⊢n=b→na∈F↔ba∈F
20 19 rspcv ⊢b∈V∖a→∀n∈V∖ana∈F→ba∈F
21 17 20 syl ⊢b∈V∧a≠b∧e=ab→∀n∈V∖ana∈F→ba∈F
22 prcom ⊢ab=ba
23 22 eqeq2i ⊢e=ab↔e=ba
24 eqcom ⊢e=ba↔ba=e
25 23 24 sylbb ⊢e=ab→ba=e
26 25 eleq1d ⊢e=ab→ba∈F↔e∈F
27 26 biimpd ⊢e=ab→ba∈F→e∈F
28 27 ad2antll ⊢b∈V∧a≠b∧e=ab→ba∈F→e∈F
29 21 28 syld ⊢b∈V∧a≠b∧e=ab→∀n∈V∖ana∈F→e∈F
30 12 29 syl9 ⊢a∈V→b∈V∧a≠b∧e=ab→∀k∈V∀n∈V∖knk∈F→e∈F
31 30 impl ⊢a∈V∧b∈V∧a≠b∧e=ab→∀k∈V∀n∈V∖knk∈F→e∈F
32 31 adantld ⊢a∈V∧b∈V∧a≠b∧e=ab→H∈USGraph∧∀k∈V∀n∈V∖knk∈F→e∈F
33 6 32 biimtrid ⊢a∈V∧b∈V∧a≠b∧e=ab→H∈ComplUSGraph→e∈F
34 33 ex ⊢a∈V∧b∈V→a≠b∧e=ab→H∈ComplUSGraph→e∈F
35 34 rexlimivv ⊢∃a∈V∃b∈Va≠b∧e=ab→H∈ComplUSGraph→e∈F
36 5 35 syl ⊢G∈USGraph∧e∈E→H∈ComplUSGraph→e∈F
37 36 impancom ⊢G∈USGraph∧H∈ComplUSGraph→e∈E→e∈F
38 37 ssrdv ⊢G∈USGraph∧H∈ComplUSGraph→E⊆F