Metamath Proof Explorer

Theorem usgrstrrepe

Description: Replacing (or adding) the edges (between elements of the base set) of an extensible structure results in a simple graph. Instead of requiring ( ph -> G Struct X ) , it would be sufficient to require ( ph -> Fun ( G \ { (/) } ) ) and ( ph -> G e. _V ) . (Contributed by AV, 13-Nov-2021) (Proof shortened by AV, 16-Nov-2021)

Ref Expression
Hypotheses usgrstrrepe.v ⊢ 𝑉 = ( Base ‘ 𝐺 )
usgrstrrepe.i ⊢ 𝐼 = ( .ef ‘ ndx )
usgrstrrepe.s ⊢ ( 𝜑 → 𝐺 Struct 𝑋 )
usgrstrrepe.b ⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝐺 )
usgrstrrepe.w ⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
usgrstrrepe.e ⊢ ( 𝜑 → 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
Assertion usgrstrrepe ( 𝜑 → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∈ USGraph )

Proof

Step Hyp Ref Expression
1 usgrstrrepe.v ⊢ 𝑉 = ( Base ‘ 𝐺 )
2 usgrstrrepe.i ⊢ 𝐼 = ( .ef ‘ ndx )
3 usgrstrrepe.s ⊢ ( 𝜑 → 𝐺 Struct 𝑋 )
4 usgrstrrepe.b ⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝐺 )
5 usgrstrrepe.w ⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
6 usgrstrrepe.e ⊢ ( 𝜑 → 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
7 2 3 4 5 setsvtx ⊢ ( 𝜑 → ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = ( Base ‘ 𝐺 ) )
8 7 1 eqtr4di ⊢ ( 𝜑 → ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = 𝑉 )
9 8 pweqd ⊢ ( 𝜑 → 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = 𝒫 𝑉 )
10 9 rabeqdv ⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
11 f1eq3 ⊢ ( { 𝑥 ∈ 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
12 10 11 syl ⊢ ( 𝜑 → ( 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
13 6 12 mpbird ⊢ ( 𝜑 → 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
14 2 3 4 5 setsiedg ⊢ ( 𝜑 → ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = 𝐸 )
15 14 dmeqd ⊢ ( 𝜑 → dom ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = dom 𝐸 )
16 eqidd ⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
17 14 15 16 f1eq123d ⊢ ( 𝜑 → ( ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) : dom ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
18 13 17 mpbird ⊢ ( 𝜑 → ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) : dom ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
19 ovex ⊢ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∈ V
20 eqid ⊢ ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) )
21 eqid ⊢ ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) )
22 20 21 isusgrs ⊢ ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∈ V → ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∈ USGraph ↔ ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) : dom ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
23 19 22 mp1i ⊢ ( 𝜑 → ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∈ USGraph ↔ ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) : dom ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
24 18 23 mpbird ⊢ ( 𝜑 → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∈ USGraph )