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 V a b e = a b
6 3 4 iscusgredg H ComplUSGraph H USGraph k V n V k n k F
7 sneq k = a k = a
8 7 difeq2d k = a V k = V a
9 preq2 k = a n k = n a
10 9 eleq1d k = a n k F n a F
11 8 10 raleqbidv k = a n V k n k F n V a n a F
12 11 rspcv a V k V n V k n k F n V a n a F
13 simpl a b e = a b a b
14 13 necomd a b e = a b b a
15 14 anim2i b V a b e = a b b V b a
16 eldifsn b V a b V b a
17 15 16 sylibr b V a b e = a b b V a
18 preq1 n = b n a = b a
19 18 eleq1d n = b n a F b a F
20 19 rspcv b V a n V a n a F b a F
21 17 20 syl b V a b e = a b n V a n a F b a F
22 prcom a b = b a
23 22 eqeq2i e = a b e = b a
24 eqcom e = b a b a = e
25 23 24 sylbb e = a b b a = e
26 25 eleq1d e = a b b a F e F
27 26 biimpd e = a b b a F e F
28 27 ad2antll b V a b e = a b b a F e F
29 21 28 syld b V a b e = a b n V a n a F e F
30 12 29 syl9 a V b V a b e = a b k V n V k n k F e F
31 30 impl a V b V a b e = a b k V n V k n k F e F
32 31 adantld a V b V a b e = a b H USGraph k V n V k n k F e F
33 6 32 syl5bi a V b V a b e = a b H ComplUSGraph e F
34 33 ex a V b V a b e = a b H ComplUSGraph e F
35 34 rexlimivv a V b V a b e = a b 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