uspgr2wlkeq

Description: Conditions for two walks within the same simple pseudograph being the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 3-Jul-2018) (Revised by AV, 14-Apr-2021)

		Ref	Expression
	Assertion	uspgr2wlkeq	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( 𝐴 = 𝐵 ↔ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		3anan32	⊢ ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) ↔ ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) )
2	1	a1i	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) ↔ ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) ) )
3		wlkeq	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( 𝐴 = 𝐵 ↔ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) ) )
4	3	3expa	⊢ ( ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( 𝐴 = 𝐵 ↔ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) ) )
5	4	3adant1	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( 𝐴 = 𝐵 ↔ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) ) )
6		fzofzp1	⊢ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → ( 𝑥 + 1 ) ∈ ( 0 ... 𝑁 ) )
7	6	adantl	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑥 + 1 ) ∈ ( 0 ... 𝑁 ) )
8		fveq2	⊢ ( 𝑦 = ( 𝑥 + 1 ) → ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑥 + 1 ) ) )
9		fveq2	⊢ ( 𝑦 = ( 𝑥 + 1 ) → ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑥 + 1 ) ) )
10	8 9	eqeq12d	⊢ ( 𝑦 = ( 𝑥 + 1 ) → ( ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ↔ ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑥 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑥 + 1 ) ) ) )
11	10	adantl	⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 = ( 𝑥 + 1 ) ) → ( ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ↔ ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑥 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑥 + 1 ) ) ) )
12	7 11	rspcdv	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) → ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑥 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑥 + 1 ) ) ) )
13	12	impancom	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) → ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑥 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑥 + 1 ) ) ) )
14	13	ralrimiv	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) → ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑥 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑥 + 1 ) ) )
15		fvoveq1	⊢ ( 𝑦 = 𝑥 → ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) = ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑥 + 1 ) ) )
16		fvoveq1	⊢ ( 𝑦 = 𝑥 → ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑥 + 1 ) ) )
17	15 16	eqeq12d	⊢ ( 𝑦 = 𝑥 → ( ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) ↔ ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑥 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑥 + 1 ) ) ) )
18	17	cbvralvw	⊢ ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) ↔ ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑥 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑥 + 1 ) ) )
19	14 18	sylibr	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) )
20		fzossfz	⊢ ( 0 ..^ 𝑁 ) ⊆ ( 0 ... 𝑁 )
21		ssralv	⊢ ( ( 0 ..^ 𝑁 ) ⊆ ( 0 ... 𝑁 ) → ( ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) )
22	20 21	mp1i	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) )
23		r19.26	⊢ ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ∧ ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) ) ↔ ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) ) )
24		preq12	⊢ ( ( ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ∧ ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) ) → { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } )
25	24	a1i	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ( ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ∧ ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) ) → { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) )
26	25	ralimdv	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ∧ ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) ) → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) )
27	23 26	biimtrrid	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) ) → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) )
28	27	expd	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) ) )
29	22 28	syld	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) ) )
30	29	imp	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) = ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) )
31	19 30	mpd	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } )
32	31	ex	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) )
33		uspgrupgr	⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph )
34		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
35		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
36		eqid	⊢ ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐴 )
37		eqid	⊢ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐴 )
38	34 35 36 37	upgrwlkcompim	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ ( Walks ‘ 𝐺 ) ) → ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ) )
39	38	ex	⊢ ( 𝐺 ∈ UPGraph → ( 𝐴 ∈ ( Walks ‘ 𝐺 ) → ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ) ) )
40	33 39	syl	⊢ ( 𝐺 ∈ USPGraph → ( 𝐴 ∈ ( Walks ‘ 𝐺 ) → ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ) ) )
41		eqid	⊢ ( 1^st ‘ 𝐵 ) = ( 1^st ‘ 𝐵 )
42		eqid	⊢ ( 2^nd ‘ 𝐵 ) = ( 2^nd ‘ 𝐵 )
43	34 35 41 42	upgrwlkcompim	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) → ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) )
44	43	ex	⊢ ( 𝐺 ∈ UPGraph → ( 𝐵 ∈ ( Walks ‘ 𝐺 ) → ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) ) )
45	33 44	syl	⊢ ( 𝐺 ∈ USPGraph → ( 𝐵 ∈ ( Walks ‘ 𝐺 ) → ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) ) )
46		oveq2	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) = 𝑁 → ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) = ( 0 ..^ 𝑁 ) )
47	46	eqcoms	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) → ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) = ( 0 ..^ 𝑁 ) )
48	47	raleqdv	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) → ( ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ↔ ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) )
49		oveq2	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) = 𝑁 → ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) = ( 0 ..^ 𝑁 ) )
50	49	eqcoms	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) = ( 0 ..^ 𝑁 ) )
51	50	raleqdv	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ↔ ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ) )
52	48 51	bi2anan9r	⊢ ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ( ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ) ↔ ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ∧ ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ) ) )
53		r19.26	⊢ ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ) ↔ ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ∧ ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ) )
54		eqeq2	⊢ ( { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ( ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) )
55		eqeq2	⊢ ( { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) )
56	55	eqcoms	⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ( ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) )
57	56	biimpd	⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ( ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) )
58	54 57	biimtrdi	⊢ ( { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ( ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } → ( ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) ) )
59	58	com13	⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ( ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } → ( { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) ) )
60	59	imp	⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ) → ( { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) )
61	60	ral2imi	⊢ ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) )
62	53 61	sylbir	⊢ ( ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ∧ ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) )
63	52 62	biimtrdi	⊢ ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ( ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) ) )
64	63	com12	⊢ ( ( ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ) → ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) ) )
65	64	ex	⊢ ( ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ( ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } → ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) ) ) )
66	65	3ad2ant3	⊢ ( ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) → ( ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } → ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) ) ) )
67	66	com12	⊢ ( ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } → ( ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) → ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) ) ) )
68	67	3ad2ant3	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ) → ( ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) → ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) ) ) )
69	68	imp	⊢ ( ( ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ) ∧ ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) ) → ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) ) )
70	69	expd	⊢ ( ( ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ) ∧ ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) ) → ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) ) ) )
71	70	a1i	⊢ ( 𝐺 ∈ USPGraph → ( ( ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } ) ∧ ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } ) ) → ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) ) ) ) )
72	40 45 71	syl2and	⊢ ( 𝐺 ∈ USPGraph → ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) → ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) ) ) ) )
73	72	3imp1	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) { ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐴 ) ‘ ( 𝑦 + 1 ) ) } = { ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) , ( ( 2^nd ‘ 𝐵 ) ‘ ( 𝑦 + 1 ) ) } → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ) )
74		eqcom	⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) )
75	35	uspgrf1oedg	⊢ ( 𝐺 ∈ USPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) )
76		f1of1	⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) )
77	75 76	syl	⊢ ( 𝐺 ∈ USPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) )
78		eqidd	⊢ ( 𝐺 ∈ USPGraph → ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) )
79		eqidd	⊢ ( 𝐺 ∈ USPGraph → dom ( iEdg ‘ 𝐺 ) = dom ( iEdg ‘ 𝐺 ) )
80		edgval	⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
81	80	eqcomi	⊢ ran ( iEdg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
82	81	a1i	⊢ ( 𝐺 ∈ USPGraph → ran ( iEdg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) )
83	78 79 82	f1eq123d	⊢ ( 𝐺 ∈ USPGraph → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ran ( iEdg ‘ 𝐺 ) ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) ) )
84	77 83	mpbird	⊢ ( 𝐺 ∈ USPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ran ( iEdg ‘ 𝐺 ) )
85	84	3ad2ant1	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ran ( iEdg ‘ 𝐺 ) )
86	85	adantr	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ran ( iEdg ‘ 𝐺 ) )
87	34 35 36 37	wlkelwrd	⊢ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) → ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
88	34 35 41 42	wlkelwrd	⊢ ( 𝐵 ∈ ( Walks ‘ 𝐺 ) → ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
89		oveq2	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( 0 ..^ 𝑁 ) = ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) )
90	89	eleq2d	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ) )
91		wrdsymbcl	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ) → ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) )
92	91	expcom	⊢ ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) )
93	90 92	biimtrdi	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) )
94	93	adantr	⊢ ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) )
95	94	imp	⊢ ( ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) )
96	95	com12	⊢ ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) )
97	96	adantl	⊢ ( ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) )
98		oveq2	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) → ( 0 ..^ 𝑁 ) = ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) )
99	98	eleq2d	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ) )
100		wrdsymbcl	⊢ ( ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ) → ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) )
101	100	expcom	⊢ ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) )
102	99 101	biimtrdi	⊢ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) )
103	102	adantl	⊢ ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) )
104	103	imp	⊢ ( ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) )
105	104	com12	⊢ ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) )
106	105	adantr	⊢ ( ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) )
107	97 106	jcad	⊢ ( ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) )
108	107	ex	⊢ ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) ) )
109	108	adantr	⊢ ( ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) ) )
110	109	com12	⊢ ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) ) )
111	110	adantr	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) ) )
112	111	imp	⊢ ( ( ( ( 1^st ‘ 𝐴 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐴 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 1^st ‘ 𝐵 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝐵 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) )
113	87 88 112	syl2an	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) → ( ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) )
114	113	expd	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) → ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) ) )
115	114	expd	⊢ ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) → ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) → ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) ) ) )
116	115	imp	⊢ ( ( ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) ) )
117	116	3adant1	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) ) )
118	117	imp	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) )
119	118	imp	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) )
120		f1veqaeq	⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ran ( iEdg ‘ 𝐺 ) ∧ ( ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) → ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) )
121	86 119 120	syl2an2r	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) → ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) )
122	74 121	biimtrid	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) → ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) )
123	122	ralimdva	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) ) → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) )
124	32 73 123	3syld	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ) → ( ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) )
125	124	expimpd	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) → ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) )
126	125	pm4.71d	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) ↔ ( ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( ( 1^st ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐵 ) ‘ 𝑦 ) ) ) )
127	2 5 126	3bitr4d	⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝐴 ∈ ( Walks ‘ 𝐺 ) ∧ 𝐵 ∈ ( Walks ‘ 𝐺 ) ) ∧ 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐴 ) ) ) → ( 𝐴 = 𝐵 ↔ ( 𝑁 = ( ♯ ‘ ( 1^st ‘ 𝐵 ) ) ∧ ∀ 𝑦 ∈ ( 0 ... 𝑁 ) ( ( 2^nd ‘ 𝐴 ) ‘ 𝑦 ) = ( ( 2^nd ‘ 𝐵 ) ‘ 𝑦 ) ) ) )

Metamath Proof Explorer

Theorem uspgr2wlkeq

Proof