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