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 ⊢ V = Vtx ⁡ G
Assertion prclisacycgr ⊢ ¬ G ∈ V → ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅

Proof

Step Hyp Ref Expression
1 prclisacycgr.1 ⊢ V = Vtx ⁡ G
2 fvprc ⊢ ¬ G ∈ V → Vtx ⁡ G = ∅
3 1 2 eqtrid ⊢ ¬ G ∈ V → V = ∅
4 br0 ⊢ ¬ f ∅ p
5 df-cycls ⊢ Cycles = g ∈ V ⟼ f p | f Paths ⁡ g p ∧ p ⁡ 0 = p ⁡ f
6 5 relmptopab ⊢ Rel ⁡ Cycles ⁡ G
7 cycliswlk ⊢ f Cycles ⁡ G p → f Walks ⁡ G p
8 df-br ⊢ f Cycles ⁡ G p ↔ f p ∈ Cycles ⁡ G
9 df-br ⊢ f Walks ⁡ G p ↔ f p ∈ Walks ⁡ G
10 7 8 9 3imtr3i ⊢ f p ∈ Cycles ⁡ G → f p ∈ Walks ⁡ G
11 6 10 relssi ⊢ Cycles ⁡ G ⊆ Walks ⁡ G
12 1 eqeq1i ⊢ V = ∅ ↔ Vtx ⁡ G = ∅
13 g0wlk0 ⊢ Vtx ⁡ G = ∅ → Walks ⁡ G = ∅
14 12 13 sylbi ⊢ V = ∅ → Walks ⁡ G = ∅
15 11 14 sseqtrid ⊢ V = ∅ → Cycles ⁡ G ⊆ ∅
16 ss0 ⊢ Cycles ⁡ G ⊆ ∅ → Cycles ⁡ G = ∅
17 breq ⊢ Cycles ⁡ G = ∅ → f Cycles ⁡ G p ↔ f ∅ p
18 17 notbid ⊢ Cycles ⁡ G = ∅ → ¬ f Cycles ⁡ G p ↔ ¬ f ∅ p
19 15 16 18 3syl ⊢ V = ∅ → ¬ f Cycles ⁡ G p ↔ ¬ f ∅ p
20 4 19 mpbiri ⊢ V = ∅ → ¬ f Cycles ⁡ G p
21 20 intnanrd ⊢ V = ∅ → ¬ f Cycles ⁡ G p ∧ f ≠ ∅
22 21 nexdv ⊢ V = ∅ → ¬ ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
23 22 nexdv ⊢ V = ∅ → ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
24 3 23 syl ⊢ ¬ G ∈ V → ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅