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 29658

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

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1540 class class class wbr 5095 ^◡ccnv 5622 Fun wfun 6480 ‘cfv 6486 Walkscwlks 29560 Trailsctrls 29652

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 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 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 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4479 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5518 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-iota 6442 df-fun 6488 df-fv 6494 df-wlks 29563 df-trls 29654

This theorem is referenced by: trliswlk 29659 trlf1 29660 trlres 29662 upgristrl 29664 dfpth2 29692 2pthnloop 29694 upgrspthswlk 29701 uhgrwkspth 29718 usgr2wlkspth 29722 uspgrn2crct 29771 crctcshtrl 29786 2trld 29901 0trl 30084 1trld 30104 ntrl2v2e 30120 3trld 30134 iseupthf1o 30164 subgrtrl 35108 upgrimtrls 47894 gpgprismgr4cycllem11 48093

W3C validator