Metamath Proof Explorer

Theorem umgracycusgr

Description: An acyclic multigraph is a simple graph. (Contributed by BTernaryTau, 17-Oct-2023)

Ref Expression
Assertion umgracycusgr ( ( 𝐺 ∈ UMGraph ∧ 𝐺 ∈ AcyclicGraph ) → 𝐺 ∈ USGraph )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
3 1 2 umgrf ⊢ ( 𝐺 ∈ UMGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
4 isacycgr ⊢ ( 𝐺 ∈ UMGraph → ( 𝐺 ∈ AcyclicGraph ↔ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
5 4 biimpa ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐺 ∈ AcyclicGraph ) → ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) )
6 2 umgr2cycl ⊢ ( ( 𝐺 ∈ UMGraph ∧ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )
7 2ne0 ⊢ 2 ≠ 0
8 neeq1 ⊢ ( ( ♯ ‘ 𝑓 ) = 2 → ( ( ♯ ‘ 𝑓 ) ≠ 0 ↔ 2 ≠ 0 ) )
9 7 8 mpbiri ⊢ ( ( ♯ ‘ 𝑓 ) = 2 → ( ♯ ‘ 𝑓 ) ≠ 0 )
10 hasheq0 ⊢ ( 𝑓 ∈ V → ( ( ♯ ‘ 𝑓 ) = 0 ↔ 𝑓 = ∅ ) )
11 10 elv ⊢ ( ( ♯ ‘ 𝑓 ) = 0 ↔ 𝑓 = ∅ )
12 11 necon3bii ⊢ ( ( ♯ ‘ 𝑓 ) ≠ 0 ↔ 𝑓 ≠ ∅ )
13 9 12 sylib ⊢ ( ( ♯ ‘ 𝑓 ) = 2 → 𝑓 ≠ ∅ )
14 13 anim2i ⊢ ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) )
15 14 2eximi ⊢ ( ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) )
16 6 15 syl ⊢ ( ( 𝐺 ∈ UMGraph ∧ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) )
17 16 ex ⊢ ( 𝐺 ∈ UMGraph → ( ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
18 17 con3d ⊢ ( 𝐺 ∈ UMGraph → ( ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) → ¬ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) )
19 18 adantr ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐺 ∈ AcyclicGraph ) → ( ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) → ¬ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) )
20 5 19 mpd ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐺 ∈ AcyclicGraph ) → ¬ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) )
21 dff15 ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ∧ ¬ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) )
22 21 biimpri ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ∧ ¬ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
23 3 20 22 syl2an2r ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐺 ∈ AcyclicGraph ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
24 1 2 isusgrs ⊢ ( 𝐺 ∈ UMGraph → ( 𝐺 ∈ USGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
25 24 biimprd ⊢ ( 𝐺 ∈ UMGraph → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → 𝐺 ∈ USGraph ) )
26 25 adantr ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐺 ∈ AcyclicGraph ) → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → 𝐺 ∈ USGraph ) )
27 23 26 mpd ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐺 ∈ AcyclicGraph ) → 𝐺 ∈ USGraph )