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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
cusgredgex.2 ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion cusgredgex ( 𝐺 ∈ ComplUSGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → { 𝐴 , 𝐵 } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 cusgredgex.1 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 cusgredgex.2 ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 cusgrcplgr ⊢ ( 𝐺 ∈ ComplUSGraph → 𝐺 ∈ ComplGraph )
4 1 2 cplgredgex ⊢ ( 𝐺 ∈ ComplGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) )
5 3 4 syl ⊢ ( 𝐺 ∈ ComplUSGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) )
6 5 imp ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ) → ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 )
7 df-rex ⊢ ( ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ↔ ∃ 𝑒 ( 𝑒 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝑒 ) )
8 6 7 sylib ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ) → ∃ 𝑒 ( 𝑒 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝑒 ) )
9 eldifsni ⊢ ( 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) → 𝐵 ≠ 𝐴 )
10 9 necomd ⊢ ( 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) → 𝐴 ≠ 𝐵 )
11 10 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → 𝐴 ≠ 𝐵 )
12 hashprg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → ( 𝐴 ≠ 𝐵 ↔ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) )
13 11 12 mpbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 )
14 13 adantl ⊢ ( ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑒 ∈ 𝐸 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ) → ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 )
15 cusgrusgr ⊢ ( 𝐺 ∈ ComplUSGraph → 𝐺 ∈ USGraph )
16 2 usgredgppr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑒 ∈ 𝐸 ) → ( ♯ ‘ 𝑒 ) = 2 )
17 15 16 sylan ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑒 ∈ 𝐸 ) → ( ♯ ‘ 𝑒 ) = 2 )
18 17 adantr ⊢ ( ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑒 ∈ 𝐸 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ) → ( ♯ ‘ 𝑒 ) = 2 )
19 14 18 eqtr4d ⊢ ( ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑒 ∈ 𝐸 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ) → ( ♯ ‘ { 𝐴 , 𝐵 } ) = ( ♯ ‘ 𝑒 ) )
20 simpl ⊢ ( ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑒 ∈ 𝐸 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ) → ( 𝐺 ∈ ComplUSGraph ∧ 𝑒 ∈ 𝐸 ) )
21 vex ⊢ 𝑒 ∈ V
22 2nn0 ⊢ 2 ∈ ℕ0
23 hashvnfin ⊢ ( ( 𝑒 ∈ V ∧ 2 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑒 ) = 2 → 𝑒 ∈ Fin ) )
24 21 22 23 mp2an ⊢ ( ( ♯ ‘ 𝑒 ) = 2 → 𝑒 ∈ Fin )
25 17 24 syl ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ∈ Fin )
26 fisshasheq ⊢ ( ( 𝑒 ∈ Fin ∧ { 𝐴 , 𝐵 } ⊆ 𝑒 ∧ ( ♯ ‘ { 𝐴 , 𝐵 } ) = ( ♯ ‘ 𝑒 ) ) → { 𝐴 , 𝐵 } = 𝑒 )
27 25 26 syl3an1 ⊢ ( ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑒 ∈ 𝐸 ) ∧ { 𝐴 , 𝐵 } ⊆ 𝑒 ∧ ( ♯ ‘ { 𝐴 , 𝐵 } ) = ( ♯ ‘ 𝑒 ) ) → { 𝐴 , 𝐵 } = 𝑒 )
28 27 3comr ⊢ ( ( ( ♯ ‘ { 𝐴 , 𝐵 } ) = ( ♯ ‘ 𝑒 ) ∧ ( 𝐺 ∈ ComplUSGraph ∧ 𝑒 ∈ 𝐸 ) ∧ { 𝐴 , 𝐵 } ⊆ 𝑒 ) → { 𝐴 , 𝐵 } = 𝑒 )
29 28 3exp ⊢ ( ( ♯ ‘ { 𝐴 , 𝐵 } ) = ( ♯ ‘ 𝑒 ) → ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑒 ∈ 𝐸 ) → ( { 𝐴 , 𝐵 } ⊆ 𝑒 → { 𝐴 , 𝐵 } = 𝑒 ) ) )
30 19 20 29 sylc ⊢ ( ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑒 ∈ 𝐸 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ) → ( { 𝐴 , 𝐵 } ⊆ 𝑒 → { 𝐴 , 𝐵 } = 𝑒 ) )
31 30 3impa ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑒 ∈ 𝐸 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ) → ( { 𝐴 , 𝐵 } ⊆ 𝑒 → { 𝐴 , 𝐵 } = 𝑒 ) )
32 31 3com23 ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ∧ 𝑒 ∈ 𝐸 ) → ( { 𝐴 , 𝐵 } ⊆ 𝑒 → { 𝐴 , 𝐵 } = 𝑒 ) )
33 32 3expia ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ) → ( 𝑒 ∈ 𝐸 → ( { 𝐴 , 𝐵 } ⊆ 𝑒 → { 𝐴 , 𝐵 } = 𝑒 ) ) )
34 33 imdistand ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ) → ( ( 𝑒 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝑒 ) → ( 𝑒 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } = 𝑒 ) ) )
35 34 eximdv ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ) → ( ∃ 𝑒 ( 𝑒 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝑒 ) → ∃ 𝑒 ( 𝑒 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } = 𝑒 ) ) )
36 8 35 mpd ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ) → ∃ 𝑒 ( 𝑒 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } = 𝑒 ) )
37 pm3.22 ⊢ ( ( 𝑒 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } = 𝑒 ) → ( { 𝐴 , 𝐵 } = 𝑒 ∧ 𝑒 ∈ 𝐸 ) )
38 eqcom ⊢ ( { 𝐴 , 𝐵 } = 𝑒 ↔ 𝑒 = { 𝐴 , 𝐵 } )
39 38 anbi1i ⊢ ( ( { 𝐴 , 𝐵 } = 𝑒 ∧ 𝑒 ∈ 𝐸 ) ↔ ( 𝑒 = { 𝐴 , 𝐵 } ∧ 𝑒 ∈ 𝐸 ) )
40 37 39 sylib ⊢ ( ( 𝑒 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } = 𝑒 ) → ( 𝑒 = { 𝐴 , 𝐵 } ∧ 𝑒 ∈ 𝐸 ) )
41 40 eximi ⊢ ( ∃ 𝑒 ( 𝑒 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } = 𝑒 ) → ∃ 𝑒 ( 𝑒 = { 𝐴 , 𝐵 } ∧ 𝑒 ∈ 𝐸 ) )
42 36 41 syl ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ) → ∃ 𝑒 ( 𝑒 = { 𝐴 , 𝐵 } ∧ 𝑒 ∈ 𝐸 ) )
43 prex ⊢ { 𝐴 , 𝐵 } ∈ V
44 eleq1 ⊢ ( 𝑒 = { 𝐴 , 𝐵 } → ( 𝑒 ∈ 𝐸 ↔ { 𝐴 , 𝐵 } ∈ 𝐸 ) )
45 43 44 ceqsexv ⊢ ( ∃ 𝑒 ( 𝑒 = { 𝐴 , 𝐵 } ∧ 𝑒 ∈ 𝐸 ) ↔ { 𝐴 , 𝐵 } ∈ 𝐸 )
46 42 45 sylib ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) ) → { 𝐴 , 𝐵 } ∈ 𝐸 )
47 46 ex ⊢ ( 𝐺 ∈ ComplUSGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝑉 ∖ { 𝐴 } ) ) → { 𝐴 , 𝐵 } ∈ 𝐸 ) )