Theorem structtousgr

Description: Any (extensible) structure with a base set can be made a simple graph with the set of pairs of elements of the base set regarded as edges. (Contributed by AV, 10-Nov-2021) (Revised by AV, 17-Nov-2021)

	Ref	Expression
Hypotheses	structtousgr.p	⊢ 𝑃 = { 𝑥 ∈ 𝒫 ( Base ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
	structtousgr.s	⊢ ( 𝜑 → 𝑆 Struct 𝑋 )
	structtousgr.g	⊢ 𝐺 = ( 𝑆 sSet ⟨ ( .ef ‘ ndx ) , ( I ↾ 𝑃 ) ⟩ )
	structtousgr.b	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝑆 )
Assertion	structtousgr	⊢ ( 𝜑 → 𝐺 ∈ USGraph )

Proof

Step	Hyp	Ref	Expression
1		structtousgr.p	⊢ 𝑃 = { 𝑥 ∈ 𝒫 ( Base ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
2		structtousgr.s	⊢ ( 𝜑 → 𝑆 Struct 𝑋 )
3		structtousgr.g	⊢ 𝐺 = ( 𝑆 sSet ⟨ ( .ef ‘ ndx ) , ( I ↾ 𝑃 ) ⟩ )
4		structtousgr.b	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝑆 )
5		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
6		eqid	⊢ ( .ef ‘ ndx ) = ( .ef ‘ ndx )
7		fvex	⊢ ( Base ‘ 𝑆 ) ∈ V
8	1	cusgrexilem1	⊢ ( ( Base ‘ 𝑆 ) ∈ V → ( I ↾ 𝑃 ) ∈ V )
9	7 8	mp1i	⊢ ( 𝜑 → ( I ↾ 𝑃 ) ∈ V )
10	1	usgrexilem	⊢ ( ( Base ‘ 𝑆 ) ∈ V → ( I ↾ 𝑃 ) : dom ( I ↾ 𝑃 ) –1-1→ { 𝑥 ∈ 𝒫 ( Base ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
11	7 10	mp1i	⊢ ( 𝜑 → ( I ↾ 𝑃 ) : dom ( I ↾ 𝑃 ) –1-1→ { 𝑥 ∈ 𝒫 ( Base ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
12	5 6 2 4 9 11	usgrstrrepe	⊢ ( 𝜑 → ( 𝑆 sSet ⟨ ( .ef ‘ ndx ) , ( I ↾ 𝑃 ) ⟩ ) ∈ USGraph )
13	3 12	eqeltrid	⊢ ( 𝜑 → 𝐺 ∈ USGraph )