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 eqtrid ⊢ ( 𝑉 ∈ 𝑊 → ( 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 35 37 raleqtrrdv ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉 ) → ∀ 𝑛 ∈ ( ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ∖ { 𝑣 } ) 𝑛 ∈ ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ NeighbVtx 𝑣 ) )
39 31 uvtxel ⊢ ( 𝑣 ∈ ( UnivVtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ↔ ( 𝑣 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ∧ ∀ 𝑛 ∈ ( ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ∖ { 𝑣 } ) 𝑛 ∈ ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ NeighbVtx 𝑣 ) ) )
40 8 38 39 sylanbrc ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ ( UnivVtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) )
41 40 ralrimiva ⊢ ( 𝑉 ∈ 𝑊 → ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) )
42 41 11 raleqtrrdv ⊢ ( 𝑉 ∈ 𝑊 → ∀ 𝑣 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) 𝑣 ∈ ( UnivVtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) )
43 opex ⊢ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ V
44 31 iscplgr ⊢ ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ V → ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ ComplGraph ↔ ∀ 𝑣 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) 𝑣 ∈ ( UnivVtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ) )
45 43 44 mp1i ⊢ ( 𝑉 ∈ 𝑊 → ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ ComplGraph ↔ ∀ 𝑣 ∈ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) 𝑣 ∈ ( UnivVtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ) )
46 42 45 mpbird ⊢ ( 𝑉 ∈ 𝑊 → ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ ComplGraph )
47 iscusgr ⊢ ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ ComplUSGraph ↔ ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ USGraph ∧ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ ComplGraph ) )
48 2 46 47 sylanbrc ⊢ ( 𝑉 ∈ 𝑊 → ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ ComplUSGraph )