Metamath Proof Explorer

Theorem cusgredgex

Description: Any two (distinct) vertices in a complete simple graph are connected to each other by an edge. (Contributed by BTernaryTau, 3-Oct-2023)

Ref Expression
Hypotheses cusgredgex.1 
|- V = ( Vtx ` G )
cusgredgex.2 
|- E = ( Edg ` G )
Assertion cusgredgex 
|- ( G e. ComplUSGraph -> ( ( A e. V /\ B e. ( V \ { A } ) ) -> { A , B } e. E ) )

Proof

Step Hyp Ref Expression
1 cusgredgex.1 
 |-  V = ( Vtx ` G )
2 cusgredgex.2 
 |-  E = ( Edg ` G )
3 cusgrcplgr 
 |-  ( G e. ComplUSGraph -> G e. ComplGraph )
4 1 2 cplgredgex 
 |-  ( G e. ComplGraph -> ( ( A e. V /\ B e. ( V \ { A } ) ) -> E. e e. E { A , B } C_ e ) )
5 3 4 syl 
 |-  ( G e. ComplUSGraph -> ( ( A e. V /\ B e. ( V \ { A } ) ) -> E. e e. E { A , B } C_ e ) )
6 5 imp 
 |-  ( ( G e. ComplUSGraph /\ ( A e. V /\ B e. ( V \ { A } ) ) ) -> E. e e. E { A , B } C_ e )
7 df-rex 
 |-  ( E. e e. E { A , B } C_ e <-> E. e ( e e. E /\ { A , B } C_ e ) )
8 6 7 sylib 
 |-  ( ( G e. ComplUSGraph /\ ( A e. V /\ B e. ( V \ { A } ) ) ) -> E. e ( e e. E /\ { A , B } C_ e ) )
9 eldifsni 
 |-  ( B e. ( V \ { A } ) -> B =/= A )
10 9 necomd 
 |-  ( B e. ( V \ { A } ) -> A =/= B )
11 10 adantl 
 |-  ( ( A e. V /\ B e. ( V \ { A } ) ) -> A =/= B )
12 hashprg 
 |-  ( ( A e. V /\ B e. ( V \ { A } ) ) -> ( A =/= B <-> ( # ` { A , B } ) = 2 ) )
13 11 12 mpbid 
 |-  ( ( A e. V /\ B e. ( V \ { A } ) ) -> ( # ` { A , B } ) = 2 )
14 13 adantl 
 |-  ( ( ( G e. ComplUSGraph /\ e e. E ) /\ ( A e. V /\ B e. ( V \ { A } ) ) ) -> ( # ` { A , B } ) = 2 )
15 cusgrusgr 
 |-  ( G e. ComplUSGraph -> G e. USGraph )
16 2 usgredgppr 
 |-  ( ( G e. USGraph /\ e e. E ) -> ( # ` e ) = 2 )
17 15 16 sylan 
 |-  ( ( G e. ComplUSGraph /\ e e. E ) -> ( # ` e ) = 2 )
18 17 adantr 
 |-  ( ( ( G e. ComplUSGraph /\ e e. E ) /\ ( A e. V /\ B e. ( V \ { A } ) ) ) -> ( # ` e ) = 2 )
19 14 18 eqtr4d 
 |-  ( ( ( G e. ComplUSGraph /\ e e. E ) /\ ( A e. V /\ B e. ( V \ { A } ) ) ) -> ( # ` { A , B } ) = ( # ` e ) )
20 simpl 
 |-  ( ( ( G e. ComplUSGraph /\ e e. E ) /\ ( A e. V /\ B e. ( V \ { A } ) ) ) -> ( G e. ComplUSGraph /\ e e. E ) )
21 vex 
 |-  e e. _V
22 2nn0 
 |-  2 e. NN0
23 hashvnfin 
 |-  ( ( e e. _V /\ 2 e. NN0 ) -> ( ( # ` e ) = 2 -> e e. Fin ) )
24 21 22 23 mp2an 
 |-  ( ( # ` e ) = 2 -> e e. Fin )
25 17 24 syl 
 |-  ( ( G e. ComplUSGraph /\ e e. E ) -> e e. Fin )
26 fisshasheq 
 |-  ( ( e e. Fin /\ { A , B } C_ e /\ ( # ` { A , B } ) = ( # ` e ) ) -> { A , B } = e )
27 25 26 syl3an1 
 |-  ( ( ( G e. ComplUSGraph /\ e e. E ) /\ { A , B } C_ e /\ ( # ` { A , B } ) = ( # ` e ) ) -> { A , B } = e )
28 27 3comr 
 |-  ( ( ( # ` { A , B } ) = ( # ` e ) /\ ( G e. ComplUSGraph /\ e e. E ) /\ { A , B } C_ e ) -> { A , B } = e )
29 28 3exp 
 |-  ( ( # ` { A , B } ) = ( # ` e ) -> ( ( G e. ComplUSGraph /\ e e. E ) -> ( { A , B } C_ e -> { A , B } = e ) ) )
30 19 20 29 sylc 
 |-  ( ( ( G e. ComplUSGraph /\ e e. E ) /\ ( A e. V /\ B e. ( V \ { A } ) ) ) -> ( { A , B } C_ e -> { A , B } = e ) )
31 30 3impa 
 |-  ( ( G e. ComplUSGraph /\ e e. E /\ ( A e. V /\ B e. ( V \ { A } ) ) ) -> ( { A , B } C_ e -> { A , B } = e ) )
32 31 3com23 
 |-  ( ( G e. ComplUSGraph /\ ( A e. V /\ B e. ( V \ { A } ) ) /\ e e. E ) -> ( { A , B } C_ e -> { A , B } = e ) )
33 32 3expia 
 |-  ( ( G e. ComplUSGraph /\ ( A e. V /\ B e. ( V \ { A } ) ) ) -> ( e e. E -> ( { A , B } C_ e -> { A , B } = e ) ) )
34 33 imdistand 
 |-  ( ( G e. ComplUSGraph /\ ( A e. V /\ B e. ( V \ { A } ) ) ) -> ( ( e e. E /\ { A , B } C_ e ) -> ( e e. E /\ { A , B } = e ) ) )
35 34 eximdv 
 |-  ( ( G e. ComplUSGraph /\ ( A e. V /\ B e. ( V \ { A } ) ) ) -> ( E. e ( e e. E /\ { A , B } C_ e ) -> E. e ( e e. E /\ { A , B } = e ) ) )
36 8 35 mpd 
 |-  ( ( G e. ComplUSGraph /\ ( A e. V /\ B e. ( V \ { A } ) ) ) -> E. e ( e e. E /\ { A , B } = e ) )
37 pm3.22 
 |-  ( ( e e. E /\ { A , B } = e ) -> ( { A , B } = e /\ e e. E ) )
38 eqcom 
 |-  ( { A , B } = e <-> e = { A , B } )
39 38 anbi1i 
 |-  ( ( { A , B } = e /\ e e. E ) <-> ( e = { A , B } /\ e e. E ) )
40 37 39 sylib 
 |-  ( ( e e. E /\ { A , B } = e ) -> ( e = { A , B } /\ e e. E ) )
41 40 eximi 
 |-  ( E. e ( e e. E /\ { A , B } = e ) -> E. e ( e = { A , B } /\ e e. E ) )
42 36 41 syl 
 |-  ( ( G e. ComplUSGraph /\ ( A e. V /\ B e. ( V \ { A } ) ) ) -> E. e ( e = { A , B } /\ e e. E ) )
43 prex 
 |-  { A , B } e. _V
44 eleq1 
 |-  ( e = { A , B } -> ( e e. E <-> { A , B } e. E ) )
45 43 44 ceqsexv 
 |-  ( E. e ( e = { A , B } /\ e e. E ) <-> { A , B } e. E )
46 42 45 sylib 
 |-  ( ( G e. ComplUSGraph /\ ( A e. V /\ B e. ( V \ { A } ) ) ) -> { A , B } e. E )
47 46 ex 
 |-  ( G e. ComplUSGraph -> ( ( A e. V /\ B e. ( V \ { A } ) ) -> { A , B } e. E ) )