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

Metamath Proof Explorer

Theorem cplgrop

Description: A complete graph represented by an ordered pair. (Contributed by AV, 10-Nov-2020)

Ref Expression
Assertion cplgrop ( 𝐺 ∈ ComplGraph → ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ ComplGraph )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 1 2 iscplgredg ⊢ ( 𝐺 ∈ ComplGraph → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ) )
4 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
5 4 a1i ⊢ ( 𝐺 ∈ ComplGraph → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
6 simpl ⊢ ( ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
7 6 adantl ⊢ ( ( ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) ∧ ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) ) → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
8 6 difeq1d ⊢ ( ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) → ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) = ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) )
9 8 adantl ⊢ ( ( ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) ∧ ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) ) → ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) = ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) )
10 edgval ⊢ ( Edg ‘ 𝑔 ) = ran ( iEdg ‘ 𝑔 )
11 simpr ⊢ ( ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) )
12 11 rneqd ⊢ ( ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) → ran ( iEdg ‘ 𝑔 ) = ran ( iEdg ‘ 𝐺 ) )
13 10 12 eqtrid ⊢ ( ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) → ( Edg ‘ 𝑔 ) = ran ( iEdg ‘ 𝐺 ) )
14 13 adantl ⊢ ( ( ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) ∧ ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) ) → ( Edg ‘ 𝑔 ) = ran ( iEdg ‘ 𝐺 ) )
15 simpl ⊢ ( ( ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) ∧ ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) ) → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
16 14 15 eqtr4d ⊢ ( ( ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) ∧ ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) ) → ( Edg ‘ 𝑔 ) = ( Edg ‘ 𝐺 ) )
17 16 rexeqdv ⊢ ( ( ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) ∧ ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) ) → ( ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ) )
18 9 17 raleqbidv ⊢ ( ( ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) ∧ ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) ) → ( ∀ 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ↔ ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ) )
19 7 18 raleqbidv ⊢ ( ( ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) ∧ ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) ) → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ↔ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ) )
20 19 biimpar ⊢ ( ( ( ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) ∧ ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ) → ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 )
21 eqid ⊢ ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝑔 )
22 eqid ⊢ ( Edg ‘ 𝑔 ) = ( Edg ‘ 𝑔 )
23 21 22 iscplgredg ⊢ ( 𝑔 ∈ V → ( 𝑔 ∈ ComplGraph ↔ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ) )
24 23 elv ⊢ ( 𝑔 ∈ ComplGraph ↔ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑣 } ) ∃ 𝑒 ∈ ( Edg ‘ 𝑔 ) { 𝑣 , 𝑛 } ⊆ 𝑒 )
25 20 24 sylibr ⊢ ( ( ( ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) ∧ ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ) → 𝑔 ∈ ComplGraph )
26 25 expcom ⊢ ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 → ( ( ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) ∧ ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) ) → 𝑔 ∈ ComplGraph ) )
27 26 expd ⊢ ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 → ( ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) → ( ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) → 𝑔 ∈ ComplGraph ) ) )
28 5 27 syl5com ⊢ ( 𝐺 ∈ ComplGraph → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑣 } ) ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 → ( ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) → 𝑔 ∈ ComplGraph ) ) )
29 3 28 sylbid ⊢ ( 𝐺 ∈ ComplGraph → ( 𝐺 ∈ ComplGraph → ( ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) → 𝑔 ∈ ComplGraph ) ) )
30 29 pm2.43i ⊢ ( 𝐺 ∈ ComplGraph → ( ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) → 𝑔 ∈ ComplGraph ) )
31 30 alrimiv ⊢ ( 𝐺 ∈ ComplGraph → ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) ) → 𝑔 ∈ ComplGraph ) )
32 fvexd ⊢ ( 𝐺 ∈ ComplGraph → ( Vtx ‘ 𝐺 ) ∈ V )
33 fvexd ⊢ ( 𝐺 ∈ ComplGraph → ( iEdg ‘ 𝐺 ) ∈ V )
34 31 32 33 gropeld ⊢ ( 𝐺 ∈ ComplGraph → ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ ComplGraph )