This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
fusgrmaxsize.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
usgrsscusgra.h ⊢ 𝑉 = ( Vtx ‘ 𝐻 )
usgrsscusgra.f ⊢ 𝐹 = ( Edg ‘ 𝐻 )
Assertion usgredgsscusgredg ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → 𝐸 ⊆ 𝐹 )

Proof

Step Hyp Ref Expression
1 fusgrmaxsize.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 fusgrmaxsize.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 usgrsscusgra.h ⊢ 𝑉 = ( Vtx ‘ 𝐻 )
4 usgrsscusgra.f ⊢ 𝐹 = ( Edg ‘ 𝐻 )
5 1 2 usgredg ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑒 ∈ 𝐸 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) )
6 3 4 iscusgredg ⊢ ( 𝐻 ∈ ComplUSGraph ↔ ( 𝐻 ∈ USGraph ∧ ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 ) )
7 sneq ⊢ ( 𝑘 = 𝑎 → { 𝑘 } = { 𝑎 } )
8 7 difeq2d ⊢ ( 𝑘 = 𝑎 → ( 𝑉 ∖ { 𝑘 } ) = ( 𝑉 ∖ { 𝑎 } ) )
9 preq2 ⊢ ( 𝑘 = 𝑎 → { 𝑛 , 𝑘 } = { 𝑛 , 𝑎 } )
10 9 eleq1d ⊢ ( 𝑘 = 𝑎 → ( { 𝑛 , 𝑘 } ∈ 𝐹 ↔ { 𝑛 , 𝑎 } ∈ 𝐹 ) )
11 8 10 raleqbidv ⊢ ( 𝑘 = 𝑎 → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 ↔ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑎 } ) { 𝑛 , 𝑎 } ∈ 𝐹 ) )
12 11 rspcv ⊢ ( 𝑎 ∈ 𝑉 → ( ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 → ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑎 } ) { 𝑛 , 𝑎 } ∈ 𝐹 ) )
13 simpl ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) → 𝑎 ≠ 𝑏 )
14 13 necomd ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) → 𝑏 ≠ 𝑎 )
15 14 anim2i ⊢ ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( 𝑏 ∈ 𝑉 ∧ 𝑏 ≠ 𝑎 ) )
16 eldifsn ⊢ ( 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ↔ ( 𝑏 ∈ 𝑉 ∧ 𝑏 ≠ 𝑎 ) )
17 15 16 sylibr ⊢ ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) )
18 preq1 ⊢ ( 𝑛 = 𝑏 → { 𝑛 , 𝑎 } = { 𝑏 , 𝑎 } )
19 18 eleq1d ⊢ ( 𝑛 = 𝑏 → ( { 𝑛 , 𝑎 } ∈ 𝐹 ↔ { 𝑏 , 𝑎 } ∈ 𝐹 ) )
20 19 rspcv ⊢ ( 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑎 } ) { 𝑛 , 𝑎 } ∈ 𝐹 → { 𝑏 , 𝑎 } ∈ 𝐹 ) )
21 17 20 syl ⊢ ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑎 } ) { 𝑛 , 𝑎 } ∈ 𝐹 → { 𝑏 , 𝑎 } ∈ 𝐹 ) )
22 prcom ⊢ { 𝑎 , 𝑏 } = { 𝑏 , 𝑎 }
23 22 eqeq2i ⊢ ( 𝑒 = { 𝑎 , 𝑏 } ↔ 𝑒 = { 𝑏 , 𝑎 } )
24 eqcom ⊢ ( 𝑒 = { 𝑏 , 𝑎 } ↔ { 𝑏 , 𝑎 } = 𝑒 )
25 23 24 sylbb ⊢ ( 𝑒 = { 𝑎 , 𝑏 } → { 𝑏 , 𝑎 } = 𝑒 )
26 25 eleq1d ⊢ ( 𝑒 = { 𝑎 , 𝑏 } → ( { 𝑏 , 𝑎 } ∈ 𝐹 ↔ 𝑒 ∈ 𝐹 ) )
27 26 biimpd ⊢ ( 𝑒 = { 𝑎 , 𝑏 } → ( { 𝑏 , 𝑎 } ∈ 𝐹 → 𝑒 ∈ 𝐹 ) )
28 27 ad2antll ⊢ ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( { 𝑏 , 𝑎 } ∈ 𝐹 → 𝑒 ∈ 𝐹 ) )
29 21 28 syld ⊢ ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑎 } ) { 𝑛 , 𝑎 } ∈ 𝐹 → 𝑒 ∈ 𝐹 ) )
30 12 29 syl9 ⊢ ( 𝑎 ∈ 𝑉 → ( ( 𝑏 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 → 𝑒 ∈ 𝐹 ) ) )
31 30 impl ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 → 𝑒 ∈ 𝐹 ) )
32 31 adantld ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( ( 𝐻 ∈ USGraph ∧ ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) { 𝑛 , 𝑘 } ∈ 𝐹 ) → 𝑒 ∈ 𝐹 ) )
33 6 32 biimtrid ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) ) → ( 𝐻 ∈ ComplUSGraph → 𝑒 ∈ 𝐹 ) )
34 33 ex ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) → ( 𝐻 ∈ ComplUSGraph → 𝑒 ∈ 𝐹 ) ) )
35 34 rexlimivv ⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑒 = { 𝑎 , 𝑏 } ) → ( 𝐻 ∈ ComplUSGraph → 𝑒 ∈ 𝐹 ) )
36 5 35 syl ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑒 ∈ 𝐸 ) → ( 𝐻 ∈ ComplUSGraph → 𝑒 ∈ 𝐹 ) )
37 36 impancom ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → ( 𝑒 ∈ 𝐸 → 𝑒 ∈ 𝐹 ) )
38 37 ssrdv ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → 𝐸 ⊆ 𝐹 )