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 )