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 27576

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 5654	. . 3 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ⟨𝑉, 𝐸⟩ ∈ (V × V))
2		opvtxval 27575	. . 3 ⊢ (⟨𝑉, 𝐸⟩ ∈ (V × V) → (Vtx‘⟨𝑉, 𝐸⟩) = (1^st ‘⟨𝑉, 𝐸⟩))
3	1, 2	syl 17	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘⟨𝑉, 𝐸⟩) = (1^st ‘⟨𝑉, 𝐸⟩))
4		op1stg 7903	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (1^st ‘⟨𝑉, 𝐸⟩) = 𝑉)
5	3, 4	eqtrd 2776	1 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘⟨𝑉, 𝐸⟩) = 𝑉)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 = wceq 1540 ∈ wcel 2105 Vcvv 3441 ⟨cop 4578 × cxp 5612 ‘cfv 6473 1^st c1st 7889 Vtxcvtx 27568

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-sep 5240 ax-nul 5247 ax-pr 5369 ax-un 7642

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3404 df-v 3443 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-nul 4269 df-if 4473 df-sn 4573 df-pr 4575 df-op 4579 df-uni 4852 df-br 5090 df-opab 5152 df-mpt 5173 df-id 5512 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-iota 6425 df-fun 6475 df-fv 6481 df-1st 7891 df-vtx 27570

This theorem is referenced by: opvtxov 27577 opvtxfvi 27581 gropd 27603 isuhgrop 27642 uhgrunop 27647 upgrop 27666 upgr1eop 27687 upgrunop 27691 umgrunop 27693 isuspgrop 27733 isusgrop 27734 ausgrusgrb 27737 uspgr1eop 27816 usgr1eop 27819 usgrexmpllem 27829 uhgrspan1lem2 27870 upgrres1lem2 27880 opfusgr 27892 fusgrfisbase 27897 fusgrfisstep 27898 usgrexi 28010 cusgrexi 28012 p1evtxdeqlem 28081 p1evtxdeq 28082 p1evtxdp1 28083 uspgrloopvtx 28084 umgr2v2evtx 28090 wlk2v2e 28722 eupthvdres 28800 eupth2lemb 28802 konigsbergvtx 28811 konigsberg 28822 strisomgrop 45632 ushrisomgr 45633 uspgrsprfo 45650

W3C validator