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 30288

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 30287	. 2 ⊢ (Trails‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝐺)𝑝 ∧ Fun ^◡𝑓)}
2		cnveq 5852	. . . 4 ⊢ (𝑓 = 𝐹 → ^◡𝑓 = ^◡𝐹)
3	2	funeqd 6566	. . 3 ⊢ (𝑓 = 𝐹 → (Fun ^◡𝑓 ↔ Fun ^◡𝐹))
4	3	adantr 486	. 2 ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (Fun ^◡𝑓 ↔ Fun ^◡𝐹))
5		relwlk 30215	. 2 ⊢ Rel (Walks‘𝐺)
6	1, 4, 5	brfvopabrbr 6995	1 ⊢ (𝐹(Trails‘𝐺)𝑃 ↔ (𝐹(Walks‘𝐺)𝑃 ∧ Fun ^◡𝐹))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ↔ wb 209 ∧ wa 401 = wceq 1569 class class class wbr 5102 ^◡ccnv 5650 Fun wfun 6537 ‘cfv 6543 Walkscwlks 30186 Trailsctrls 30282

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pr 5391

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6497 df-fun 6545 df-fv 6551 df-wlks 30189 df-trls 30284

This theorem is used by: trliswlk 30289 trlf1 30290 trlres 30292 upgristrl 30294 subgrtrl 30303 dfpth2 30323 2pthnloop 30326 upgrspthswlk 30333 uhgrwkspth 30350 usgr2wlkspth 30354 uspgrn2crct 30406 crctcshtrl 30421 2trld 30536 0trl 30722 1trld 30742 ntrl2v2e 30768 3trld 30782 iseupthf1o 30812 upgrimtrls 49112 gpgprismgr4cycllem11 49311

W3C validator