This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wlkiswwlkupgr

Description: A walk as word corresponds to a walk in a pseudograph. This variant of wlkiswwlks does not require G to be a simple pseudograph, but it requires (indirectly) the Axiom of Choice for its proof. (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 10-Apr-2021)

		Ref	Expression
	Assertion	wlkiswwlkupgr	\|- ( G e. UPGraph -> ( E. f f ( Walks ` G ) P <-> P e. ( WWalks ` G ) ) )

Proof

Step	Hyp	Ref	Expression
1		wlkiswwlks1	\|- ( G e. UPGraph -> ( f ( Walks ` G ) P -> P e. ( WWalks ` G ) ) )
2	1	exlimdv	\|- ( G e. UPGraph -> ( E. f f ( Walks ` G ) P -> P e. ( WWalks ` G ) ) )
3		wlkiswwlksupgr2	\|- ( G e. UPGraph -> ( P e. ( WWalks ` G ) -> E. f f ( Walks ` G ) P ) )
4	2 3	impbid	\|- ( G e. UPGraph -> ( E. f f ( Walks ` G ) P <-> P e. ( WWalks ` G ) ) )