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	eqtrid	⊢ ( ¬ 𝐺 ∈ 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 ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) )