Theorem usgrexmpl1

Description: G is a simple graph of six vertices 0 , 1 , 2 , 3 , 4 , 5 , with edges { 0 , 1 } , { 1 , 2 } , { 0 , 2 } , { 0 , 3 } , { 3 , 4 } , { 3 , 5 } , { 4 , 5 } . (Contributed by AV, 3-Aug-2025)

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

Proof

Step	Hyp	Ref	Expression
1		usgrexmpl1.v	⊢ 𝑉 = ( 0 ... 5 )
2		usgrexmpl1.e	⊢ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩
3		usgrexmpl1.g	⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
4	1 2	usgrexmpl1lem	⊢ 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 }
5	3	eleq1i	⊢ ( 𝐺 ∈ USGraph ↔ ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph )
6	1	ovexi	⊢ 𝑉 ∈ V
7		s7cli	⊢ ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ∈ Word V
8	2 7	eqeltri	⊢ 𝐸 ∈ Word V
9		isusgrop	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ Word V ) → ( ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
10	6 8 9	mp2an	⊢ ( ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } )
11	5 10	bitri	⊢ ( 𝐺 ∈ USGraph ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } )
12	4 11	mpbir	⊢ 𝐺 ∈ USGraph