Theorem usgrexmpl

Description: G is a simple graph of five vertices 0 , 1 , 2 , 3 , 4 , with edges { 0 , 1 } , { 1 , 2 } , { 2 , 0 } , { 0 , 3 } . (Contributed by Alexander van der Vekens, 15-Aug-2017) (Revised by AV, 21-Oct-2020)

	Ref	Expression
Hypotheses	usgrexmpl.v	⊢ 𝑉 = ( 0 ... 4 )
	usgrexmpl.e	⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩
	usgrexmpl.g	⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion	usgrexmpl	⊢ 𝐺 ∈ USGraph

Proof

Step	Hyp	Ref	Expression
1		usgrexmpl.v	⊢ 𝑉 = ( 0 ... 4 )
2		usgrexmpl.e	⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩
3		usgrexmpl.g	⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
4	1 2	usgrexmplef	⊢ 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 }
5		opex	⊢ ⟨ 𝑉 , 𝐸 ⟩ ∈ V
6	3 5	eqeltri	⊢ 𝐺 ∈ V
7		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
8		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
9	7 8	isusgrs	⊢ ( 𝐺 ∈ V → ( 𝐺 ∈ USGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
10	1 2 3	usgrexmpllem	⊢ ( ( Vtx ‘ 𝐺 ) = 𝑉 ∧ ( iEdg ‘ 𝐺 ) = 𝐸 )
11		simpr	⊢ ( ( ( Vtx ‘ 𝐺 ) = 𝑉 ∧ ( iEdg ‘ 𝐺 ) = 𝐸 ) → ( iEdg ‘ 𝐺 ) = 𝐸 )
12	11	dmeqd	⊢ ( ( ( Vtx ‘ 𝐺 ) = 𝑉 ∧ ( iEdg ‘ 𝐺 ) = 𝐸 ) → dom ( iEdg ‘ 𝐺 ) = dom 𝐸 )
13		pweq	⊢ ( ( Vtx ‘ 𝐺 ) = 𝑉 → 𝒫 ( Vtx ‘ 𝐺 ) = 𝒫 𝑉 )
14	13	adantr	⊢ ( ( ( Vtx ‘ 𝐺 ) = 𝑉 ∧ ( iEdg ‘ 𝐺 ) = 𝐸 ) → 𝒫 ( Vtx ‘ 𝐺 ) = 𝒫 𝑉 )
15	14	rabeqdv	⊢ ( ( ( Vtx ‘ 𝐺 ) = 𝑉 ∧ ( iEdg ‘ 𝐺 ) = 𝐸 ) → { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } = { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } )
16	11 12 15	f1eq123d	⊢ ( ( ( Vtx ‘ 𝐺 ) = 𝑉 ∧ ( iEdg ‘ 𝐺 ) = 𝐸 ) → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
17	10 16	ax-mp	⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } )
18	9 17	bitrdi	⊢ ( 𝐺 ∈ V → ( 𝐺 ∈ USGraph ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
19	6 18	ax-mp	⊢ ( 𝐺 ∈ USGraph ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } )
20	4 19	mpbir	⊢ 𝐺 ∈ USGraph