opiedgfv - Metamath Proof Explorer

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

Theorem opiedgfv 28988

Description: The set of indexed edges 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
opiedgfv	⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘⟨𝑉, 𝐸⟩) = 𝐸)

**Proof of Theorem opiedgfv**
Step	Hyp	Ref	Expression
1		opelvvg 5672	. . 3 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ⟨𝑉, 𝐸⟩ ∈ (V × V))
2		opiedgval 28987	. . 3 ⊢ (⟨𝑉, 𝐸⟩ ∈ (V × V) → (iEdg‘⟨𝑉, 𝐸⟩) = (2^nd ‘⟨𝑉, 𝐸⟩))
3	1, 2	syl 17	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘⟨𝑉, 𝐸⟩) = (2^nd ‘⟨𝑉, 𝐸⟩))
4		op2ndg 7960	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (2^nd ‘⟨𝑉, 𝐸⟩) = 𝐸)
5	3, 4	eqtrd 2764	1 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘⟨𝑉, 𝐸⟩) = 𝐸)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 Vcvv 3444 ⟨cop 4591 × cxp 5629 ‘cfv 6499 2^nd c2nd 7946 iEdgciedg 28978

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5246 ax-nul 5256 ax-pr 5382 ax-un 7691

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rab 3403 df-v 3446 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4485 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5103 df-opab 5165 df-mpt 5184 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-iota 6452 df-fun 6501 df-fv 6507 df-2nd 7948 df-iedg 28980

This theorem is referenced by: opiedgov 28989 opiedgfvi 28991 gropd 29012 edgopval 29032 isuhgrop 29051 uhgrunop 29056 upgrop 29075 upgr0eop 29095 upgr1eop 29096 upgrunop 29100 umgrunop 29102 isuspgrop 29142 isusgrop 29143 ausgrusgrb 29146 usgr0eop 29227 uspgr1eop 29228 usgr1eop 29231 usgrexmpllem 29241 uhgrspan1lem3 29283 upgrres1lem3 29293 fusgrfisbase 29309 fusgrfisstep 29310 usgrexi 29422 cusgrexi 29424 p1evtxdeqlem 29494 p1evtxdeq 29495 p1evtxdp1 29496 uspgrloopiedg 29499 umgr2v2eiedg 29505 wlk2v2e 30137 eupthvdres 30215 eupth2lemb 30217 konigsbergiedg 30227 isubgriedg 47857 opstrgric 47920 ushggricedg 47921 usgrexmpl1edg 48009 usgrexmpl2edg 48014

W3C validator