Metamath Proof Explorer


Theorem cusgrexi

Description: An arbitrary set V regarded as set of vertices together with the set of pairs of elements of this set regarded as edges is a complete simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 5-Nov-2020) (Proof shortened by AV, 14-Feb-2022)

Ref Expression
Hypothesis usgrexi.p 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
Assertion cusgrexi ( 𝑉𝑊 → ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ ComplUSGraph )

Proof

Step Hyp Ref Expression
1 usgrexi.p 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
2 1 usgrexi ( 𝑉𝑊 → ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ USGraph )
3 1 cusgrexilem1 ( 𝑉𝑊 → ( I ↾ 𝑃 ) ∈ V )
4 opvtxfv ( ( 𝑉𝑊 ∧ ( I ↾ 𝑃 ) ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = 𝑉 )
5 4 eqcomd ( ( 𝑉𝑊 ∧ ( I ↾ 𝑃 ) ∈ V ) → 𝑉 = ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) )
6 3 5 mpdan ( 𝑉𝑊𝑉 = ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) )
7 6 eleq2d ( 𝑉𝑊 → ( 𝑣𝑉𝑣 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ) )
8 7 biimpa ( ( 𝑉𝑊𝑣𝑉 ) → 𝑣 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) )
9 eldifi ( 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) → 𝑛𝑉 )
10 9 adantl ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → 𝑛𝑉 )
11 3 4 mpdan ( 𝑉𝑊 → ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = 𝑉 )
12 11 eleq2d ( 𝑉𝑊 → ( 𝑛 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ↔ 𝑛𝑉 ) )
13 12 ad2antrr ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ( 𝑛 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ↔ 𝑛𝑉 ) )
14 10 13 mpbird ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → 𝑛 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) )
15 simplr ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → 𝑣𝑉 )
16 11 eleq2d ( 𝑉𝑊 → ( 𝑣 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ↔ 𝑣𝑉 ) )
17 16 ad2antrr ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ( 𝑣 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ↔ 𝑣𝑉 ) )
18 15 17 mpbird ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → 𝑣 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) )
19 14 18 jca ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ( 𝑛 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ∧ 𝑣 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ) )
20 eldifsni ( 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) → 𝑛𝑣 )
21 20 adantl ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → 𝑛𝑣 )
22 1 cusgrexilem2 ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ∃ 𝑒 ∈ ran ( I ↾ 𝑃 ) { 𝑣 , 𝑛 } ⊆ 𝑒 )
23 edgval ( Edg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = ran ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ )
24 opiedgfv ( ( 𝑉𝑊 ∧ ( I ↾ 𝑃 ) ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = ( I ↾ 𝑃 ) )
25 3 24 mpdan ( 𝑉𝑊 → ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = ( I ↾ 𝑃 ) )
26 25 rneqd ( 𝑉𝑊 → ran ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = ran ( I ↾ 𝑃 ) )
27 23 26 syl5eq ( 𝑉𝑊 → ( Edg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = ran ( I ↾ 𝑃 ) )
28 27 rexeqdv ( 𝑉𝑊 → ( ∃ 𝑒 ∈ ( Edg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) { 𝑣 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ ran ( I ↾ 𝑃 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ) )
29 28 ad2antrr ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ( ∃ 𝑒 ∈ ( Edg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) { 𝑣 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ ran ( I ↾ 𝑃 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ) )
30 22 29 mpbird ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ∃ 𝑒 ∈ ( Edg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) { 𝑣 , 𝑛 } ⊆ 𝑒 )
31 eqid ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ )
32 eqid ( Edg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = ( Edg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ )
33 31 32 nbgrel ( 𝑛 ∈ ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ NeighbVtx 𝑣 ) ↔ ( ( 𝑛 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ∧ 𝑣 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ) ∧ 𝑛𝑣 ∧ ∃ 𝑒 ∈ ( Edg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) { 𝑣 , 𝑛 } ⊆ 𝑒 ) )
34 19 21 30 33 syl3anbrc ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → 𝑛 ∈ ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ NeighbVtx 𝑣 ) )
35 34 ralrimiva ( ( 𝑉𝑊𝑣𝑉 ) → ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ NeighbVtx 𝑣 ) )
36 11 adantr ( ( 𝑉𝑊𝑣𝑉 ) → ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = 𝑉 )
37 36 difeq1d ( ( 𝑉𝑊𝑣𝑉 ) → ( ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ∖ { 𝑣 } ) = ( 𝑉 ∖ { 𝑣 } ) )
38 37 raleqdv ( ( 𝑉𝑊𝑣𝑉 ) → ( ∀ 𝑛 ∈ ( ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ∖ { 𝑣 } ) 𝑛 ∈ ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ NeighbVtx 𝑣 ) ↔ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ NeighbVtx 𝑣 ) ) )
39 35 38 mpbird ( ( 𝑉𝑊𝑣𝑉 ) → ∀ 𝑛 ∈ ( ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ∖ { 𝑣 } ) 𝑛 ∈ ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ NeighbVtx 𝑣 ) )
40 31 uvtxel ( 𝑣 ∈ ( UnivVtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ↔ ( 𝑣 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ∧ ∀ 𝑛 ∈ ( ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ∖ { 𝑣 } ) 𝑛 ∈ ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ NeighbVtx 𝑣 ) ) )
41 8 39 40 sylanbrc ( ( 𝑉𝑊𝑣𝑉 ) → 𝑣 ∈ ( UnivVtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) )
42 41 ralrimiva ( 𝑉𝑊 → ∀ 𝑣𝑉 𝑣 ∈ ( UnivVtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) )
43 11 raleqdv ( 𝑉𝑊 → ( ∀ 𝑣 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) 𝑣 ∈ ( UnivVtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ↔ ∀ 𝑣𝑉 𝑣 ∈ ( UnivVtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ) )
44 42 43 mpbird ( 𝑉𝑊 → ∀ 𝑣 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) 𝑣 ∈ ( UnivVtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) )
45 opex 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ V
46 31 iscplgr ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ V → ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ ComplGraph ↔ ∀ 𝑣 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) 𝑣 ∈ ( UnivVtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ) )
47 45 46 mp1i ( 𝑉𝑊 → ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ ComplGraph ↔ ∀ 𝑣 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) 𝑣 ∈ ( UnivVtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ) )
48 44 47 mpbird ( 𝑉𝑊 → ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ ComplGraph )
49 iscusgr ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ ComplUSGraph ↔ ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ USGraph ∧ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ ComplGraph ) )
50 2 48 49 sylanbrc ( 𝑉𝑊 → ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ ComplUSGraph )