Metamath Proof Explorer


Theorem prclisacycgr

Description: A proper class (representing a null graph, see vtxvalprc ) has the property of an acyclic graph (see also acycgr0v ). (Contributed by BTernaryTau, 11-Oct-2023) (New usage is discouraged.)

Ref Expression
Hypothesis prclisacycgr.1 𝑉 = ( Vtx ‘ 𝐺 )
Assertion prclisacycgr ( ¬ 𝐺 ∈ V → ¬ ∃ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝𝑓 ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 prclisacycgr.1 𝑉 = ( Vtx ‘ 𝐺 )
2 fvprc ( ¬ 𝐺 ∈ V → ( Vtx ‘ 𝐺 ) = ∅ )
3 1 2 syl5eq ( ¬ 𝐺 ∈ V → 𝑉 = ∅ )
4 br0 ¬ 𝑓𝑝
5 df-cycls Cycles = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Paths ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) } )
6 5 relmptopab Rel ( Cycles ‘ 𝐺 )
7 cycliswlk ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
8 df-br ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ↔ ⟨ 𝑓 , 𝑝 ⟩ ∈ ( Cycles ‘ 𝐺 ) )
9 df-br ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ↔ ⟨ 𝑓 , 𝑝 ⟩ ∈ ( Walks ‘ 𝐺 ) )
10 7 8 9 3imtr3i ( ⟨ 𝑓 , 𝑝 ⟩ ∈ ( Cycles ‘ 𝐺 ) → ⟨ 𝑓 , 𝑝 ⟩ ∈ ( Walks ‘ 𝐺 ) )
11 6 10 relssi ( Cycles ‘ 𝐺 ) ⊆ ( Walks ‘ 𝐺 )
12 1 eqeq1i ( 𝑉 = ∅ ↔ ( Vtx ‘ 𝐺 ) = ∅ )
13 g0wlk0 ( ( Vtx ‘ 𝐺 ) = ∅ → ( Walks ‘ 𝐺 ) = ∅ )
14 12 13 sylbi ( 𝑉 = ∅ → ( Walks ‘ 𝐺 ) = ∅ )
15 11 14 sseqtrid ( 𝑉 = ∅ → ( Cycles ‘ 𝐺 ) ⊆ ∅ )
16 ss0 ( ( Cycles ‘ 𝐺 ) ⊆ ∅ → ( Cycles ‘ 𝐺 ) = ∅ )
17 breq ( ( Cycles ‘ 𝐺 ) = ∅ → ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝𝑓𝑝 ) )
18 17 notbid ( ( Cycles ‘ 𝐺 ) = ∅ → ( ¬ 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ↔ ¬ 𝑓𝑝 ) )
19 15 16 18 3syl ( 𝑉 = ∅ → ( ¬ 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ↔ ¬ 𝑓𝑝 ) )
20 4 19 mpbiri ( 𝑉 = ∅ → ¬ 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 )
21 20 intnanrd ( 𝑉 = ∅ → ¬ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝𝑓 ≠ ∅ ) )
22 21 nexdv ( 𝑉 = ∅ → ¬ ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝𝑓 ≠ ∅ ) )
23 22 nexdv ( 𝑉 = ∅ → ¬ ∃ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝𝑓 ≠ ∅ ) )
24 3 23 syl ( ¬ 𝐺 ∈ V → ¬ ∃ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝𝑓 ≠ ∅ ) )