Theorem isumgr

Description: The property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020)

	Ref	Expression
Hypotheses	isumgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	isumgr.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion	isumgr	⊢ ( 𝐺 ∈ 𝑈 → ( 𝐺 ∈ UMGraph ↔ 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )

Proof

Step	Hyp	Ref	Expression
1		isumgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		isumgr.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3		df-umgr	⊢ UMGraph = { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } }
4	3	eleq2i	⊢ ( 𝐺 ∈ UMGraph ↔ 𝐺 ∈ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } } )
5		fveq2	⊢ ( ℎ = 𝐺 → ( iEdg ‘ ℎ ) = ( iEdg ‘ 𝐺 ) )
6	5 2	eqtr4di	⊢ ( ℎ = 𝐺 → ( iEdg ‘ ℎ ) = 𝐸 )
7	5	dmeqd	⊢ ( ℎ = 𝐺 → dom ( iEdg ‘ ℎ ) = dom ( iEdg ‘ 𝐺 ) )
8	2	eqcomi	⊢ ( iEdg ‘ 𝐺 ) = 𝐸
9	8	dmeqi	⊢ dom ( iEdg ‘ 𝐺 ) = dom 𝐸
10	7 9	eqtrdi	⊢ ( ℎ = 𝐺 → dom ( iEdg ‘ ℎ ) = dom 𝐸 )
11		fveq2	⊢ ( ℎ = 𝐺 → ( Vtx ‘ ℎ ) = ( Vtx ‘ 𝐺 ) )
12	11 1	eqtr4di	⊢ ( ℎ = 𝐺 → ( Vtx ‘ ℎ ) = 𝑉 )
13	12	pweqd	⊢ ( ℎ = 𝐺 → 𝒫 ( Vtx ‘ ℎ ) = 𝒫 𝑉 )
14	13	difeq1d	⊢ ( ℎ = 𝐺 → ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) = ( 𝒫 𝑉 ∖ { ∅ } ) )
15	14	rabeqdv	⊢ ( ℎ = 𝐺 → { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
16	6 10 15	feq123d	⊢ ( ℎ = 𝐺 → ( ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
17		fvexd	⊢ ( 𝑔 = ℎ → ( Vtx ‘ 𝑔 ) ∈ V )
18		fveq2	⊢ ( 𝑔 = ℎ → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ ℎ ) )
19		fvexd	⊢ ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) → ( iEdg ‘ 𝑔 ) ∈ V )
20		fveq2	⊢ ( 𝑔 = ℎ → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ ℎ ) )
21	20	adantr	⊢ ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ ℎ ) )
22		simpr	⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → 𝑒 = ( iEdg ‘ ℎ ) )
23	22	dmeqd	⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → dom 𝑒 = dom ( iEdg ‘ ℎ ) )
24		pweq	⊢ ( 𝑣 = ( Vtx ‘ ℎ ) → 𝒫 𝑣 = 𝒫 ( Vtx ‘ ℎ ) )
25	24	ad2antlr	⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → 𝒫 𝑣 = 𝒫 ( Vtx ‘ ℎ ) )
26	25	difeq1d	⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → ( 𝒫 𝑣 ∖ { ∅ } ) = ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) )
27	26	rabeqdv	⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
28	22 23 27	feq123d	⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → ( 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
29	19 21 28	sbcied2	⊢ ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) → ( [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
30	17 18 29	sbcied2	⊢ ( 𝑔 = ℎ → ( [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
31	30	cbvabv	⊢ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } } = { ℎ ∣ ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } }
32	16 31	elab2g	⊢ ( 𝐺 ∈ 𝑈 → ( 𝐺 ∈ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } } ↔ 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
33	4 32	syl5bb	⊢ ( 𝐺 ∈ 𝑈 → ( 𝐺 ∈ UMGraph ↔ 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )