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 syl5bi ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑎𝑏𝑒 = { 𝑎 , 𝑏 } ) ) → ( 𝐻 ∈ 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 ) → 𝐸𝐹 )