Metamath Proof Explorer

Theorem cycldlenngric

Description: Two simple pseudographs are not isomorphic if one has a cycle and the other has no cycle of the same length. (Contributed by AV, 6-Nov-2025)

Ref Expression
Assertion cycldlenngric ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ( ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ∧ ¬ ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ 𝐻 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) → ¬ 𝐺 ≃𝑔𝑟 𝐻 ) )

Proof

Step Hyp Ref Expression
1 brgric ⊢ ( 𝐺 ≃𝑔𝑟 𝐻 ↔ ( 𝐺 GraphIso 𝐻 ) ≠ ∅ )
2 n0rex ⊢ ( ( 𝐺 GraphIso 𝐻 ) ≠ ∅ → ∃ 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) )
3 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
4 eqid ⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐻 )
5 simprll ⊢ ( ( 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) → 𝐺 ∈ USPGraph )
6 simprlr ⊢ ( ( 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) → 𝐻 ∈ USPGraph )
7 simpl ⊢ ( ( 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) → 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) )
8 2fveq3 ⊢ ( 𝑥 = 𝑗 → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑗 ) ) )
9 8 imaeq2d ⊢ ( 𝑥 = 𝑗 → ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) = ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑗 ) ) ) )
10 9 fveq2d ⊢ ( 𝑥 = 𝑗 → ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) = ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑗 ) ) ) ) )
11 10 cbvmptv ⊢ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) = ( 𝑗 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑗 ) ) ) ) )
12 cycliswlk ⊢ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
13 12 ad2antrl ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
14 13 adantl ⊢ ( ( 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
15 3 4 5 6 7 11 14 upgrimwlklen ⊢ ( ( 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) → ( ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ( Walks ‘ 𝐻 ) ( 𝑖 ∘ 𝑝 ) ∧ ( ♯ ‘ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) = ( ♯ ‘ 𝑓 ) ) )
16 simprrl ⊢ ( ( 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) → 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 )
17 3 4 5 6 7 11 16 upgrimcycls ⊢ ( ( 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) → ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ( Cycles ‘ 𝐻 ) ( 𝑖 ∘ 𝑝 ) )
18 simp3 ⊢ ( ( ( 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) ∧ ( ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ( Walks ‘ 𝐻 ) ( 𝑖 ∘ 𝑝 ) ∧ ( ♯ ‘ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) = ( ♯ ‘ 𝑓 ) ) ∧ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ( Cycles ‘ 𝐻 ) ( 𝑖 ∘ 𝑝 ) ) → ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ( Cycles ‘ 𝐻 ) ( 𝑖 ∘ 𝑝 ) )
19 simp2r ⊢ ( ( ( 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) ∧ ( ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ( Walks ‘ 𝐻 ) ( 𝑖 ∘ 𝑝 ) ∧ ( ♯ ‘ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) = ( ♯ ‘ 𝑓 ) ) ∧ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ( Cycles ‘ 𝐻 ) ( 𝑖 ∘ 𝑝 ) ) → ( ♯ ‘ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) = ( ♯ ‘ 𝑓 ) )
20 simprrr ⊢ ( ( 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) → ( ♯ ‘ 𝑓 ) = 𝑁 )
21 20 3ad2ant1 ⊢ ( ( ( 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) ∧ ( ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ( Walks ‘ 𝐻 ) ( 𝑖 ∘ 𝑝 ) ∧ ( ♯ ‘ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) = ( ♯ ‘ 𝑓 ) ) ∧ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ( Cycles ‘ 𝐻 ) ( 𝑖 ∘ 𝑝 ) ) → ( ♯ ‘ 𝑓 ) = 𝑁 )
22 19 21 eqtrd ⊢ ( ( ( 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) ∧ ( ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ( Walks ‘ 𝐻 ) ( 𝑖 ∘ 𝑝 ) ∧ ( ♯ ‘ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) = ( ♯ ‘ 𝑓 ) ) ∧ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ( Cycles ‘ 𝐻 ) ( 𝑖 ∘ 𝑝 ) ) → ( ♯ ‘ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) = 𝑁 )
23 vex ⊢ 𝑖 ∈ V
24 vex ⊢ 𝑝 ∈ V
25 23 24 coex ⊢ ( 𝑖 ∘ 𝑝 ) ∈ V
26 vex ⊢ 𝑓 ∈ V
27 26 dmex ⊢ dom 𝑓 ∈ V
28 27 mptex ⊢ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ∈ V
29 breq12 ⊢ ( ( 𝑔 = ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ∧ 𝑞 = ( 𝑖 ∘ 𝑝 ) ) → ( 𝑔 ( Cycles ‘ 𝐻 ) 𝑞 ↔ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ( Cycles ‘ 𝐻 ) ( 𝑖 ∘ 𝑝 ) ) )
30 29 ancoms ⊢ ( ( 𝑞 = ( 𝑖 ∘ 𝑝 ) ∧ 𝑔 = ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) → ( 𝑔 ( Cycles ‘ 𝐻 ) 𝑞 ↔ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ( Cycles ‘ 𝐻 ) ( 𝑖 ∘ 𝑝 ) ) )
31 fveqeq2 ⊢ ( 𝑔 = ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) → ( ( ♯ ‘ 𝑔 ) = 𝑁 ↔ ( ♯ ‘ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) = 𝑁 ) )
32 31 adantl ⊢ ( ( 𝑞 = ( 𝑖 ∘ 𝑝 ) ∧ 𝑔 = ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) → ( ( ♯ ‘ 𝑔 ) = 𝑁 ↔ ( ♯ ‘ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) = 𝑁 ) )
33 30 32 anbi12d ⊢ ( ( 𝑞 = ( 𝑖 ∘ 𝑝 ) ∧ 𝑔 = ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) → ( ( 𝑔 ( Cycles ‘ 𝐻 ) 𝑞 ∧ ( ♯ ‘ 𝑔 ) = 𝑁 ) ↔ ( ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ( Cycles ‘ 𝐻 ) ( 𝑖 ∘ 𝑝 ) ∧ ( ♯ ‘ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) = 𝑁 ) ) )
34 25 28 33 spc2ev ⊢ ( ( ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ( Cycles ‘ 𝐻 ) ( 𝑖 ∘ 𝑝 ) ∧ ( ♯ ‘ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) = 𝑁 ) → ∃ 𝑞 ∃ 𝑔 ( 𝑔 ( Cycles ‘ 𝐻 ) 𝑞 ∧ ( ♯ ‘ 𝑔 ) = 𝑁 ) )
35 18 22 34 syl2anc ⊢ ( ( ( 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) ∧ ( ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ( Walks ‘ 𝐻 ) ( 𝑖 ∘ 𝑝 ) ∧ ( ♯ ‘ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) = ( ♯ ‘ 𝑓 ) ) ∧ ( 𝑥 ∈ dom 𝑓 ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑖 “ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ) ( Cycles ‘ 𝐻 ) ( 𝑖 ∘ 𝑝 ) ) → ∃ 𝑞 ∃ 𝑔 ( 𝑔 ( Cycles ‘ 𝐻 ) 𝑞 ∧ ( ♯ ‘ 𝑔 ) = 𝑁 ) )
36 15 17 35 mpd3an23 ⊢ ( ( 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) ) → ∃ 𝑞 ∃ 𝑔 ( 𝑔 ( Cycles ‘ 𝐻 ) 𝑞 ∧ ( ♯ ‘ 𝑔 ) = 𝑁 ) )
37 36 ex ⊢ ( 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) → ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) → ∃ 𝑞 ∃ 𝑔 ( 𝑔 ( Cycles ‘ 𝐻 ) 𝑞 ∧ ( ♯ ‘ 𝑔 ) = 𝑁 ) ) )
38 37 rexlimivw ⊢ ( ∃ 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) 𝑖 ∈ ( 𝐺 GraphIso 𝐻 ) → ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) → ∃ 𝑞 ∃ 𝑔 ( 𝑔 ( Cycles ‘ 𝐻 ) 𝑞 ∧ ( ♯ ‘ 𝑔 ) = 𝑁 ) ) )
39 2 38 syl ⊢ ( ( 𝐺 GraphIso 𝐻 ) ≠ ∅ → ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) → ∃ 𝑞 ∃ 𝑔 ( 𝑔 ( Cycles ‘ 𝐻 ) 𝑞 ∧ ( ♯ ‘ 𝑔 ) = 𝑁 ) ) )
40 1 39 sylbi ⊢ ( 𝐺 ≃𝑔𝑟 𝐻 → ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) → ∃ 𝑞 ∃ 𝑔 ( 𝑔 ( Cycles ‘ 𝐻 ) 𝑞 ∧ ( ♯ ‘ 𝑔 ) = 𝑁 ) ) )
41 40 expdcom ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) → ( 𝐺 ≃𝑔𝑟 𝐻 → ∃ 𝑞 ∃ 𝑔 ( 𝑔 ( Cycles ‘ 𝐻 ) 𝑞 ∧ ( ♯ ‘ 𝑔 ) = 𝑁 ) ) ) )
42 41 exlimdvv ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) → ( 𝐺 ≃𝑔𝑟 𝐻 → ∃ 𝑞 ∃ 𝑔 ( 𝑔 ( Cycles ‘ 𝐻 ) 𝑞 ∧ ( ♯ ‘ 𝑔 ) = 𝑁 ) ) ) )
43 42 imp ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) → ( 𝐺 ≃𝑔𝑟 𝐻 → ∃ 𝑞 ∃ 𝑔 ( 𝑔 ( Cycles ‘ 𝐻 ) 𝑞 ∧ ( ♯ ‘ 𝑔 ) = 𝑁 ) ) )
44 breq12 ⊢ ( ( 𝑓 = 𝑔 ∧ 𝑝 = 𝑞 ) → ( 𝑓 ( Cycles ‘ 𝐻 ) 𝑝 ↔ 𝑔 ( Cycles ‘ 𝐻 ) 𝑞 ) )
45 44 ancoms ⊢ ( ( 𝑝 = 𝑞 ∧ 𝑓 = 𝑔 ) → ( 𝑓 ( Cycles ‘ 𝐻 ) 𝑝 ↔ 𝑔 ( Cycles ‘ 𝐻 ) 𝑞 ) )
46 fveqeq2 ⊢ ( 𝑓 = 𝑔 → ( ( ♯ ‘ 𝑓 ) = 𝑁 ↔ ( ♯ ‘ 𝑔 ) = 𝑁 ) )
47 46 adantl ⊢ ( ( 𝑝 = 𝑞 ∧ 𝑓 = 𝑔 ) → ( ( ♯ ‘ 𝑓 ) = 𝑁 ↔ ( ♯ ‘ 𝑔 ) = 𝑁 ) )
48 45 47 anbi12d ⊢ ( ( 𝑝 = 𝑞 ∧ 𝑓 = 𝑔 ) → ( ( 𝑓 ( Cycles ‘ 𝐻 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ↔ ( 𝑔 ( Cycles ‘ 𝐻 ) 𝑞 ∧ ( ♯ ‘ 𝑔 ) = 𝑁 ) ) )
49 48 cbvex2vw ⊢ ( ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ 𝐻 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ↔ ∃ 𝑞 ∃ 𝑔 ( 𝑔 ( Cycles ‘ 𝐻 ) 𝑞 ∧ ( ♯ ‘ 𝑔 ) = 𝑁 ) )
50 43 49 imbitrrdi ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) → ( 𝐺 ≃𝑔𝑟 𝐻 → ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ 𝐻 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) )
51 50 con3d ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) → ( ¬ ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ 𝐻 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) → ¬ 𝐺 ≃𝑔𝑟 𝐻 ) )
52 51 expimpd ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ( ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ∧ ¬ ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ 𝐻 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 𝑁 ) ) → ¬ 𝐺 ≃𝑔𝑟 𝐻 ) )