Metamath Proof Explorer

Theorem dfconngr1

Description: Alternative definition of the class of all connected graphs, requiring paths between distinct vertices. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Revised by AV, 15-Feb-2021)

Ref Expression
Assertion dfconngr1 ⊢ ConnGraph = g | [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p

Proof

Step Hyp Ref Expression
1 df-conngr ⊢ ConnGraph = g | [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∃ f ∃ p f k PathsOn ⁡ g n p
2 eqid ⊢ Vtx ⁡ g = Vtx ⁡ g
3 2 0pthonv ⊢ k ∈ Vtx ⁡ g → ∃ f ∃ p f k PathsOn ⁡ g k p
4 oveq2 ⊢ n = k → k PathsOn ⁡ g n = k PathsOn ⁡ g k
5 4 breqd ⊢ n = k → f k PathsOn ⁡ g n p ↔ f k PathsOn ⁡ g k p
6 5 2exbidv ⊢ n = k → ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∃ f ∃ p f k PathsOn ⁡ g k p
7 6 ralsng ⊢ k ∈ Vtx ⁡ g → ∀ n ∈ k ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∃ f ∃ p f k PathsOn ⁡ g k p
8 3 7 mpbird ⊢ k ∈ Vtx ⁡ g → ∀ n ∈ k ∃ f ∃ p f k PathsOn ⁡ g n p
9 difsnid ⊢ k ∈ Vtx ⁡ g → Vtx ⁡ g ∖ k ∪ k = Vtx ⁡ g
10 9 eqcomd ⊢ k ∈ Vtx ⁡ g → Vtx ⁡ g = Vtx ⁡ g ∖ k ∪ k
11 10 raleqdv ⊢ k ∈ Vtx ⁡ g → ∀ n ∈ Vtx ⁡ g ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ n ∈ Vtx ⁡ g ∖ k ∪ k ∃ f ∃ p f k PathsOn ⁡ g n p
12 ralunb ⊢ ∀ n ∈ Vtx ⁡ g ∖ k ∪ k ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ n ∈ Vtx ⁡ g ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p ∧ ∀ n ∈ k ∃ f ∃ p f k PathsOn ⁡ g n p
13 11 12 bitrdi ⊢ k ∈ Vtx ⁡ g → ∀ n ∈ Vtx ⁡ g ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ n ∈ Vtx ⁡ g ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p ∧ ∀ n ∈ k ∃ f ∃ p f k PathsOn ⁡ g n p
14 8 13 mpbiran2d ⊢ k ∈ Vtx ⁡ g → ∀ n ∈ Vtx ⁡ g ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ n ∈ Vtx ⁡ g ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p
15 14 ralbiia ⊢ ∀ k ∈ Vtx ⁡ g ∀ n ∈ Vtx ⁡ g ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ k ∈ Vtx ⁡ g ∀ n ∈ Vtx ⁡ g ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p
16 fvex ⊢ Vtx ⁡ g ∈ V
17 raleq ⊢ v = Vtx ⁡ g → ∀ n ∈ v ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ n ∈ Vtx ⁡ g ∃ f ∃ p f k PathsOn ⁡ g n p
18 17 raleqbi1dv ⊢ v = Vtx ⁡ g → ∀ k ∈ v ∀ n ∈ v ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ k ∈ Vtx ⁡ g ∀ n ∈ Vtx ⁡ g ∃ f ∃ p f k PathsOn ⁡ g n p
19 difeq1 ⊢ v = Vtx ⁡ g → v ∖ k = Vtx ⁡ g ∖ k
20 19 raleqdv ⊢ v = Vtx ⁡ g → ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ n ∈ Vtx ⁡ g ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p
21 20 raleqbi1dv ⊢ v = Vtx ⁡ g → ∀ k ∈ v ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ k ∈ Vtx ⁡ g ∀ n ∈ Vtx ⁡ g ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p
22 18 21 bibi12d ⊢ v = Vtx ⁡ g → ∀ k ∈ v ∀ n ∈ v ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ k ∈ v ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ k ∈ Vtx ⁡ g ∀ n ∈ Vtx ⁡ g ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ k ∈ Vtx ⁡ g ∀ n ∈ Vtx ⁡ g ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p
23 16 22 sbcie ⊢ [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ k ∈ v ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ k ∈ Vtx ⁡ g ∀ n ∈ Vtx ⁡ g ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ k ∈ Vtx ⁡ g ∀ n ∈ Vtx ⁡ g ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p
24 15 23 mpbir ⊢ [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ k ∈ v ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p
25 sbcbi1 ⊢ [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ k ∈ v ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p → [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∃ f ∃ p f k PathsOn ⁡ g n p ↔ [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p
26 24 25 ax-mp ⊢ [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∃ f ∃ p f k PathsOn ⁡ g n p ↔ [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p
27 26 abbii ⊢ g | [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∃ f ∃ p f k PathsOn ⁡ g n p = g | [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p
28 1 27 eqtri ⊢ ConnGraph = g | [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p