Metamath Proof Explorer

Theorem cplgrop

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

Ref Expression
Assertion cplgrop 
|- ( G e. ComplGraph -> <. ( Vtx ` G ) , ( iEdg ` G ) >. e. ComplGraph )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 iscplgredg 
 |-  ( G e. ComplGraph -> ( G e. ComplGraph <-> A. v e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { v } ) E. e e. ( Edg ` G ) { v , n } C_ e ) )
4 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
5 4 a1i 
 |-  ( G e. ComplGraph -> ( Edg ` G ) = ran ( iEdg ` G ) )
6 simpl 
 |-  ( ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) -> ( Vtx ` g ) = ( Vtx ` G ) )
7 6 adantl 
 |-  ( ( ( Edg ` G ) = ran ( iEdg ` G ) /\ ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) ) -> ( Vtx ` g ) = ( Vtx ` G ) )
8 6 difeq1d 
 |-  ( ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) -> ( ( Vtx ` g ) \ { v } ) = ( ( Vtx ` G ) \ { v } ) )
9 8 adantl 
 |-  ( ( ( Edg ` G ) = ran ( iEdg ` G ) /\ ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) ) -> ( ( Vtx ` g ) \ { v } ) = ( ( Vtx ` G ) \ { v } ) )
10 edgval 
 |-  ( Edg ` g ) = ran ( iEdg ` g )
11 simpr 
 |-  ( ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) -> ( iEdg ` g ) = ( iEdg ` G ) )
12 11 rneqd 
 |-  ( ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) -> ran ( iEdg ` g ) = ran ( iEdg ` G ) )
13 10 12 eqtrid 
 |-  ( ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) -> ( Edg ` g ) = ran ( iEdg ` G ) )
14 13 adantl 
 |-  ( ( ( Edg ` G ) = ran ( iEdg ` G ) /\ ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) ) -> ( Edg ` g ) = ran ( iEdg ` G ) )
15 simpl 
 |-  ( ( ( Edg ` G ) = ran ( iEdg ` G ) /\ ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) ) -> ( Edg ` G ) = ran ( iEdg ` G ) )
16 14 15 eqtr4d 
 |-  ( ( ( Edg ` G ) = ran ( iEdg ` G ) /\ ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) ) -> ( Edg ` g ) = ( Edg ` G ) )
17 16 rexeqdv 
 |-  ( ( ( Edg ` G ) = ran ( iEdg ` G ) /\ ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) ) -> ( E. e e. ( Edg ` g ) { v , n } C_ e <-> E. e e. ( Edg ` G ) { v , n } C_ e ) )
18 9 17 raleqbidv 
 |-  ( ( ( Edg ` G ) = ran ( iEdg ` G ) /\ ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) ) -> ( A. n e. ( ( Vtx ` g ) \ { v } ) E. e e. ( Edg ` g ) { v , n } C_ e <-> A. n e. ( ( Vtx ` G ) \ { v } ) E. e e. ( Edg ` G ) { v , n } C_ e ) )
19 7 18 raleqbidv 
 |-  ( ( ( Edg ` G ) = ran ( iEdg ` G ) /\ ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) ) -> ( A. v e. ( Vtx ` g ) A. n e. ( ( Vtx ` g ) \ { v } ) E. e e. ( Edg ` g ) { v , n } C_ e <-> A. v e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { v } ) E. e e. ( Edg ` G ) { v , n } C_ e ) )
20 19 biimpar 
 |-  ( ( ( ( Edg ` G ) = ran ( iEdg ` G ) /\ ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) ) /\ A. v e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { v } ) E. e e. ( Edg ` G ) { v , n } C_ e ) -> A. v e. ( Vtx ` g ) A. n e. ( ( Vtx ` g ) \ { v } ) E. e e. ( Edg ` g ) { v , n } C_ e )
21 eqid 
 |-  ( Vtx ` g ) = ( Vtx ` g )
22 eqid 
 |-  ( Edg ` g ) = ( Edg ` g )
23 21 22 iscplgredg 
 |-  ( g e. _V -> ( g e. ComplGraph <-> A. v e. ( Vtx ` g ) A. n e. ( ( Vtx ` g ) \ { v } ) E. e e. ( Edg ` g ) { v , n } C_ e ) )
24 23 elv 
 |-  ( g e. ComplGraph <-> A. v e. ( Vtx ` g ) A. n e. ( ( Vtx ` g ) \ { v } ) E. e e. ( Edg ` g ) { v , n } C_ e )
25 20 24 sylibr 
 |-  ( ( ( ( Edg ` G ) = ran ( iEdg ` G ) /\ ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) ) /\ A. v e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { v } ) E. e e. ( Edg ` G ) { v , n } C_ e ) -> g e. ComplGraph )
26 25 expcom 
 |-  ( A. v e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { v } ) E. e e. ( Edg ` G ) { v , n } C_ e -> ( ( ( Edg ` G ) = ran ( iEdg ` G ) /\ ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) ) -> g e. ComplGraph ) )
27 26 expd 
 |-  ( A. v e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { v } ) E. e e. ( Edg ` G ) { v , n } C_ e -> ( ( Edg ` G ) = ran ( iEdg ` G ) -> ( ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) -> g e. ComplGraph ) ) )
28 5 27 syl5com 
 |-  ( G e. ComplGraph -> ( A. v e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { v } ) E. e e. ( Edg ` G ) { v , n } C_ e -> ( ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) -> g e. ComplGraph ) ) )
29 3 28 sylbid 
 |-  ( G e. ComplGraph -> ( G e. ComplGraph -> ( ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) -> g e. ComplGraph ) ) )
30 29 pm2.43i 
 |-  ( G e. ComplGraph -> ( ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) -> g e. ComplGraph ) )
31 30 alrimiv 
 |-  ( G e. ComplGraph -> A. g ( ( ( Vtx ` g ) = ( Vtx ` G ) /\ ( iEdg ` g ) = ( iEdg ` G ) ) -> g e. ComplGraph ) )
32 fvexd 
 |-  ( G e. ComplGraph -> ( Vtx ` G ) e. _V )
33 fvexd 
 |-  ( G e. ComplGraph -> ( iEdg ` G ) e. _V )
34 31 32 33 gropeld 
 |-  ( G e. ComplGraph -> <. ( Vtx ` G ) , ( iEdg ` G ) >. e. ComplGraph )