opvtxfv - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > opvtxfv		Structured version Visualization version GIF version

Theorem opvtxfv 29058

Description: The set of vertices of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 21-Sep-2020.)

**Assertion**
Ref	Expression
opvtxfv	⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘⟨𝑉, 𝐸⟩) = 𝑉)

**Proof of Theorem opvtxfv**
Step	Hyp	Ref	Expression
1		opelvvg 5664	. . 3 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ⟨𝑉, 𝐸⟩ ∈ (V × V))
2		opvtxval 29057	. . 3 ⊢ (⟨𝑉, 𝐸⟩ ∈ (V × V) → (Vtx‘⟨𝑉, 𝐸⟩) = (1^st ‘⟨𝑉, 𝐸⟩))
3	1, 2	syl 17	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘⟨𝑉, 𝐸⟩) = (1^st ‘⟨𝑉, 𝐸⟩))
4		op1stg 7945	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (1^st ‘⟨𝑉, 𝐸⟩) = 𝑉)
5	3, 4	eqtrd 2770	1 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘⟨𝑉, 𝐸⟩) = 𝑉)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 Vcvv 3439 ⟨cop 4585 × cxp 5621 ‘cfv 6491 1^st c1st 7931 Vtxcvtx 29050

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2183 ax-ext 2707 ax-sep 5240 ax-nul 5250 ax-pr 5376 ax-un 7680

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2538 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2810 df-nfc 2884 df-ne 2932 df-ral 3051 df-rex 3060 df-rab 3399 df-v 3441 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-nul 4285 df-if 4479 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-br 5098 df-opab 5160 df-mpt 5179 df-id 5518 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-iota 6447 df-fun 6493 df-fv 6499 df-1st 7933 df-vtx 29052

This theorem is referenced by: opvtxov 29059 opvtxfvi 29063 gropd 29085 isuhgrop 29124 uhgrunop 29129 upgrop 29148 upgr1eop 29169 upgrunop 29173 umgrunop 29175 isuspgrop 29215 isusgrop 29216 ausgrusgrb 29219 uspgr1eop 29301 usgr1eop 29304 usgrexmpllem 29314 uhgrspan1lem2 29355 upgrres1lem2 29365 opfusgr 29377 fusgrfisbase 29382 fusgrfisstep 29383 usgrexi 29495 cusgrexi 29497 p1evtxdeqlem 29567 p1evtxdeq 29568 p1evtxdp1 29569 uspgrloopvtx 29570 umgr2v2evtx 29576 wlk2v2e 30213 eupthvdres 30291 eupth2lemb 30293 konigsbergvtx 30302 konigsberg 30313 isubgrvtx 48150 opstrgric 48209 ushggricedg 48210 usgrexmpl1vtx 48306 usgrexmpl2vtx 48311 uspgrsprfo 48431

W3C validator