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 28978

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 5655	. . 3 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ⟨𝑉, 𝐸⟩ ∈ (V × V))
2		opiedgval 28977	. . 3 ⊢ (⟨𝑉, 𝐸⟩ ∈ (V × V) → (iEdg‘⟨𝑉, 𝐸⟩) = (2^nd ‘⟨𝑉, 𝐸⟩))
3	1, 2	syl 17	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘⟨𝑉, 𝐸⟩) = (2^nd ‘⟨𝑉, 𝐸⟩))
4		op2ndg 7929	. 2 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (2^nd ‘⟨𝑉, 𝐸⟩) = 𝐸)
5	3, 4	eqtrd 2765	1 ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘⟨𝑉, 𝐸⟩) = 𝐸)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2110 Vcvv 3434 ⟨cop 4580 × cxp 5612 ‘cfv 6477 2^nd c2nd 7915 iEdgciedg 28968

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 1911 ax-6 1968 ax-7 2009 ax-8 2112 ax-9 2120 ax-10 2143 ax-11 2159 ax-12 2179 ax-ext 2702 ax-sep 5232 ax-nul 5242 ax-pr 5368 ax-un 7663

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-ral 3046 df-rex 3055 df-rab 3394 df-v 3436 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-nul 4282 df-if 4474 df-sn 4575 df-pr 4577 df-op 4581 df-uni 4858 df-br 5090 df-opab 5152 df-mpt 5171 df-id 5509 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-iota 6433 df-fun 6479 df-fv 6485 df-2nd 7917 df-iedg 28970

This theorem is referenced by: opiedgov 28979 opiedgfvi 28981 gropd 29002 edgopval 29022 isuhgrop 29041 uhgrunop 29046 upgrop 29065 upgr0eop 29085 upgr1eop 29086 upgrunop 29090 umgrunop 29092 isuspgrop 29132 isusgrop 29133 ausgrusgrb 29136 usgr0eop 29217 uspgr1eop 29218 usgr1eop 29221 usgrexmpllem 29231 uhgrspan1lem3 29273 upgrres1lem3 29283 fusgrfisbase 29299 fusgrfisstep 29300 usgrexi 29412 cusgrexi 29414 p1evtxdeqlem 29484 p1evtxdeq 29485 p1evtxdp1 29486 uspgrloopiedg 29489 umgr2v2eiedg 29495 wlk2v2e 30127 eupthvdres 30205 eupth2lemb 30207 konigsbergiedg 30217 isubgriedg 47873 opstrgric 47936 ushggricedg 47937 usgrexmpl1edg 48034 usgrexmpl2edg 48039

W3C validator