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 29295

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 5703	. . 3 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ⟨𝑉, 𝐸⟩ ∈ (V × V))
2		opvtxval 29294	. . 3 ⊢ (⟨𝑉, 𝐸⟩ ∈ (V × V) → (Vtx‘⟨𝑉, 𝐸⟩) = (1^st ‘⟨𝑉, 𝐸⟩))
3	1, 2	syl 18	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘⟨𝑉, 𝐸⟩) = (1^st ‘⟨𝑉, 𝐸⟩))
4		op1stg 7998	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (1^st ‘⟨𝑉, 𝐸⟩) = 𝑉)
5	3, 4	eqtrd 2804	1 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘⟨𝑉, 𝐸⟩) = 𝑉)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1567 ∈ wcel 2149 Vcvv 3461 ⟨cop 4598 × cxp 5660 ‘cfv 6537 1^st c1st 7984 Vtxcvtx 29287

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5259 ax-nul 5271 ax-pr 5405 ax-un 7733

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-rab 3423 df-v 3463 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4491 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5557 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-iota 6493 df-fun 6539 df-fv 6545 df-1st 7986 df-vtx 29289

This theorem is referenced by: opvtxov 29296 opvtxfvi 29300 gropd 29322 isuhgrop 29361 uhgrunop 29366 upgrop 29385 upgr1eop 29406 upgrunop 29410 umgrunop 29412 isuspgrop 29452 isusgrop 29453 ausgrusgrb 29456 uspgr1eop 29538 usgr1eop 29541 usgrexmpllem 29551 uhgrspan1lem2 29592 upgrres1lem2 29602 opfusgr 29614 fusgrfisbase 29619 fusgrfisstep 29620 usgrexi 29732 cusgrexi 29734 p1evtxdeqlem 29803 p1evtxdeq 29804 p1evtxdp1 29805 uspgrloopvtx 29806 umgr2v2evtx 29812 wlk2v2e 30449 eupthvdres 30527 eupth2lemb 30529 konigsbergvtx 30538 konigsberg 30549 isubgrvtx 48556 opstrgric 48615 ushggricedg 48616 usgrexmpl1vtx 48712 usgrexmpl2vtx 48717 uspgrsprfo 48837

W3C validator