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 29677

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 29676	. 2 ⊢ (Trails‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝐺)𝑝 ∧ Fun ^◡𝑓)}
2		cnveq 5819	. . . 4 ⊢ (𝑓 = 𝐹 → ^◡𝑓 = ^◡𝐹)
3	2	funeqd 6510	. . 3 ⊢ (𝑓 = 𝐹 → (Fun ^◡𝑓 ↔ Fun ^◡𝐹))
4	3	adantr 480	. 2 ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (Fun ^◡𝑓 ↔ Fun ^◡𝐹))
5		relwlk 29608	. 2 ⊢ Rel (Walks‘𝐺)
6	1, 4, 5	brfvopabrbr 6934	1 ⊢ (𝐹(Trails‘𝐺)𝑃 ↔ (𝐹(Walks‘𝐺)𝑃 ∧ Fun ^◡𝐹))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1541 class class class wbr 5095 ^◡ccnv 5620 Fun wfun 6482 ‘cfv 6488 Walkscwlks 29579 Trailsctrls 29671

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 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-sep 5238 ax-nul 5248 ax-pr 5374

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 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-ral 3049 df-rex 3058 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4283 df-if 4477 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5516 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-iota 6444 df-fun 6490 df-fv 6496 df-wlks 29582 df-trls 29673

This theorem is referenced by: trliswlk 29678 trlf1 29679 trlres 29681 upgristrl 29683 dfpth2 29711 2pthnloop 29713 upgrspthswlk 29720 uhgrwkspth 29737 usgr2wlkspth 29741 uspgrn2crct 29790 crctcshtrl 29805 2trld 29920 0trl 30106 1trld 30126 ntrl2v2e 30142 3trld 30156 iseupthf1o 30186 subgrtrl 35200 upgrimtrls 48033 gpgprismgr4cycllem11 48232

W3C validator