Description: A graph represented as an extensible structure with vertices as base set and indexed edges is actually an extensible structure. (Contributed by AV, 23-Nov-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | struct2grvtx.g | ⊢ 𝐺 = { 〈 ( Base ‘ ndx ) , 𝑉 〉 , 〈 ( .ef ‘ ndx ) , 𝐸 〉 } | |
Assertion | struct2grstr | ⊢ 𝐺 Struct 〈 ( Base ‘ ndx ) , ( .ef ‘ ndx ) 〉 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | struct2grvtx.g | ⊢ 𝐺 = { 〈 ( Base ‘ ndx ) , 𝑉 〉 , 〈 ( .ef ‘ ndx ) , 𝐸 〉 } | |
2 | baseltedgf | ⊢ ( Base ‘ ndx ) < ( .ef ‘ ndx ) | |
3 | edgfndxnn | ⊢ ( .ef ‘ ndx ) ∈ ℕ | |
4 | 1 2 3 | 2strstr1 | ⊢ 𝐺 Struct 〈 ( Base ‘ ndx ) , ( .ef ‘ ndx ) 〉 |