Metamath Proof Explorer


Theorem umgr2v2e

Description: A multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020)

Ref Expression
Hypothesis umgr2v2evtx.g 𝐺 = ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩
Assertion umgr2v2e ( ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) → 𝐺 ∈ UMGraph )

Proof

Step Hyp Ref Expression
1 umgr2v2evtx.g 𝐺 = ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩
2 c0ex 0 ∈ V
3 1ex 1 ∈ V
4 2 3 pm3.2i ( 0 ∈ V ∧ 1 ∈ V )
5 prex { 𝐴 , 𝐵 } ∈ V
6 5 5 pm3.2i ( { 𝐴 , 𝐵 } ∈ V ∧ { 𝐴 , 𝐵 } ∈ V )
7 0ne1 0 ≠ 1
8 7 a1i ( ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) → 0 ≠ 1 )
9 fprg ( ( ( 0 ∈ V ∧ 1 ∈ V ) ∧ ( { 𝐴 , 𝐵 } ∈ V ∧ { 𝐴 , 𝐵 } ∈ V ) ∧ 0 ≠ 1 ) → { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } : { 0 , 1 } ⟶ { { 𝐴 , 𝐵 } , { 𝐴 , 𝐵 } } )
10 4 6 8 9 mp3an12i ( ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) → { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } : { 0 , 1 } ⟶ { { 𝐴 , 𝐵 } , { 𝐴 , 𝐵 } } )
11 dfsn2 { { 𝐴 , 𝐵 } } = { { 𝐴 , 𝐵 } , { 𝐴 , 𝐵 } }
12 fveqeq2 ( 𝑒 = { 𝐴 , 𝐵 } → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) )
13 prelpwi ( ( 𝐴𝑉𝐵𝑉 ) → { 𝐴 , 𝐵 } ∈ 𝒫 𝑉 )
14 13 3adant1 ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → { 𝐴 , 𝐵 } ∈ 𝒫 𝑉 )
15 1 umgr2v2evtx ( 𝑉𝑊 → ( Vtx ‘ 𝐺 ) = 𝑉 )
16 15 3ad2ant1 ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → ( Vtx ‘ 𝐺 ) = 𝑉 )
17 16 pweqd ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → 𝒫 ( Vtx ‘ 𝐺 ) = 𝒫 𝑉 )
18 14 17 eleqtrrd ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → { 𝐴 , 𝐵 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) )
19 18 adantr ( ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) → { 𝐴 , 𝐵 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) )
20 hashprg ( ( 𝐴𝑉𝐵𝑉 ) → ( 𝐴𝐵 ↔ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) )
21 20 biimpd ( ( 𝐴𝑉𝐵𝑉 ) → ( 𝐴𝐵 → ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) )
22 21 3adant1 ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → ( 𝐴𝐵 → ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) )
23 22 imp ( ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) → ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 )
24 12 19 23 elrabd ( ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) → { 𝐴 , 𝐵 } ∈ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
25 24 snssd ( ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) → { { 𝐴 , 𝐵 } } ⊆ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
26 11 25 eqsstrrid ( ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) → { { 𝐴 , 𝐵 } , { 𝐴 , 𝐵 } } ⊆ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
27 10 26 fssd ( ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) → { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } : { 0 , 1 } ⟶ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
28 27 ffdmd ( ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) → { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } : dom { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟶ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
29 1 umgr2v2eiedg ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → ( iEdg ‘ 𝐺 ) = { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } )
30 29 adantr ( ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) → ( iEdg ‘ 𝐺 ) = { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } )
31 30 dmeqd ( ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) → dom ( iEdg ‘ 𝐺 ) = dom { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } )
32 30 31 feq12d ( ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ↔ { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } : dom { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟶ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
33 28 32 mpbird ( ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
34 opex 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩ ∈ V
35 1 34 eqeltri 𝐺 ∈ V
36 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
37 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
38 36 37 isumgrs ( 𝐺 ∈ V → ( 𝐺 ∈ UMGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
39 35 38 mp1i ( ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) → ( 𝐺 ∈ UMGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
40 33 39 mpbird ( ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) ∧ 𝐴𝐵 ) → 𝐺 ∈ UMGraph )