istrl - Metamath Proof Explorer

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

Theorem istrl 30336

Description: Conditions for a pair of classes/functions to be a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) (Revised by AV, 29-Oct-2021.)

**Assertion**
Ref	Expression
istrl	⊢ (𝐹(Trails‘𝐺)𝑃 ↔ (𝐹(Walks‘𝐺)𝑃 ∧ Fun ^◡𝐹))

Proof of Theorem istrl Dummy variables 𝑓 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		trlsfval 30335	. 2 ⊢ (Trails‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝐺)𝑝 ∧ Fun ^◡𝑓)}
2		cnveq 5863	. . . 4 ⊢ (𝑓 = 𝐹 → ^◡𝑓 = ^◡𝐹)
3	2	funeqd 6589	. . 3 ⊢ (𝑓 = 𝐹 → (Fun ^◡𝑓 ↔ Fun ^◡𝐹))
4	3	adantr 486	. 2 ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (Fun ^◡𝑓 ↔ Fun ^◡𝐹))
5		relwlk 30263	. 2 ⊢ Rel (Walks‘𝐺)
6	1, 4, 5	brfvopabrbr 7021	1 ⊢ (𝐹(Trails‘𝐺)𝑃 ↔ (𝐹(Walks‘𝐺)𝑃 ∧ Fun ^◡𝐹))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ↔ wb 209 ∧ wa 401 = wceq 1570 class class class wbr 5108 ^◡ccnv 5657 Fun wfun 6560 ‘cfv 6566 Walkscwlks 30234 Trailsctrls 30330

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5255 ax-nul 5266 ax-pr 5398

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-br 5109 df-opab 5174 df-mpt 5193 df-id 5553 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-iota 6520 df-fun 6568 df-fv 6574 df-wlks 30237 df-trls 30332

This theorem is used by: trliswlk 30337 trlf1 30338 trlres 30340 upgristrl 30342 subgrtrl 30351 dfpth2 30371 2pthnloop 30374 upgrspthswlk 30381 uhgrwkspth 30398 usgr2wlkspth 30402 uspgrn2crct 30454 crctcshtrl 30469 2trld 30584 0trl 30770 1trld 30790 ntrl2v2e 30816 3trld 30830 iseupthf1o 30860 upgrimtrls 49277 gpgprismgr4cycllem11 49476

W3C validator