Metamath Proof Explorer

Theorem 1pthon2v

Description: For each pair of adjacent vertices there is a path of length 1 from one vertex to the other in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017) (Revised by AV, 22-Jan-2021)

Ref Expression
Hypotheses 1pthon2v.v ⊢ V = Vtx ⁡ G
1pthon2v.e ⊢ E = Edg ⁡ G
Assertion 1pthon2v ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ ∃ e ∈ E A B ⊆ e → ∃ f ∃ p f A PathsOn ⁡ G B p

Proof

Step Hyp Ref Expression
1 1pthon2v.v ⊢ V = Vtx ⁡ G
2 1pthon2v.e ⊢ E = Edg ⁡ G
3 simpl ⊢ A ∈ V ∧ B ∈ V → A ∈ V
4 3 anim2i ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V → G ∈ UHGraph ∧ A ∈ V
5 4 3adant3 ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ ∃ e ∈ E A B ⊆ e → G ∈ UHGraph ∧ A ∈ V
6 5 adantl ⊢ A = B ∧ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ ∃ e ∈ E A B ⊆ e → G ∈ UHGraph ∧ A ∈ V
7 1 0pthonv ⊢ A ∈ V → ∃ f ∃ p f A PathsOn ⁡ G A p
8 6 7 simpl2im ⊢ A = B ∧ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ ∃ e ∈ E A B ⊆ e → ∃ f ∃ p f A PathsOn ⁡ G A p
9 oveq2 ⊢ B = A → A PathsOn ⁡ G B = A PathsOn ⁡ G A
10 9 eqcoms ⊢ A = B → A PathsOn ⁡ G B = A PathsOn ⁡ G A
11 10 breqd ⊢ A = B → f A PathsOn ⁡ G B p ↔ f A PathsOn ⁡ G A p
12 11 2exbidv ⊢ A = B → ∃ f ∃ p f A PathsOn ⁡ G B p ↔ ∃ f ∃ p f A PathsOn ⁡ G A p
13 12 adantr ⊢ A = B ∧ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ ∃ e ∈ E A B ⊆ e → ∃ f ∃ p f A PathsOn ⁡ G B p ↔ ∃ f ∃ p f A PathsOn ⁡ G A p
14 8 13 mpbird ⊢ A = B ∧ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ ∃ e ∈ E A B ⊆ e → ∃ f ∃ p f A PathsOn ⁡ G B p
15 14 ex ⊢ A = B → G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ ∃ e ∈ E A B ⊆ e → ∃ f ∃ p f A PathsOn ⁡ G B p
16 2 eleq2i ⊢ e ∈ E ↔ e ∈ Edg ⁡ G
17 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
18 17 uhgredgiedgb ⊢ G ∈ UHGraph → e ∈ Edg ⁡ G ↔ ∃ i ∈ dom ⁡ iEdg ⁡ G e = iEdg ⁡ G ⁡ i
19 16 18 syl5bb ⊢ G ∈ UHGraph → e ∈ E ↔ ∃ i ∈ dom ⁡ iEdg ⁡ G e = iEdg ⁡ G ⁡ i
20 19 3ad2ant1 ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → e ∈ E ↔ ∃ i ∈ dom ⁡ iEdg ⁡ G e = iEdg ⁡ G ⁡ i
21 s1cli ⊢ ⟨“ i ”⟩ ∈ Word V
22 s2cli ⊢ ⟨“ AB ”⟩ ∈ Word V
23 21 22 pm3.2i ⊢ ⟨“ i ”⟩ ∈ Word V ∧ ⟨“ AB ”⟩ ∈ Word V
24 eqid ⊢ ⟨“ AB ”⟩ = ⟨“ AB ”⟩
25 eqid ⊢ ⟨“ i ”⟩ = ⟨“ i ”⟩
26 simpl2l ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ e = iEdg ⁡ G ⁡ i ∧ A B ⊆ e → A ∈ V
27 simpl2r ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ e = iEdg ⁡ G ⁡ i ∧ A B ⊆ e → B ∈ V
28 eqneqall ⊢ A = B → A ≠ B → iEdg ⁡ G ⁡ i = A
29 28 com12 ⊢ A ≠ B → A = B → iEdg ⁡ G ⁡ i = A
30 29 3ad2ant3 ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → A = B → iEdg ⁡ G ⁡ i = A
31 30 adantr ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ e = iEdg ⁡ G ⁡ i ∧ A B ⊆ e → A = B → iEdg ⁡ G ⁡ i = A
32 31 imp ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ e = iEdg ⁡ G ⁡ i ∧ A B ⊆ e ∧ A = B → iEdg ⁡ G ⁡ i = A
33 sseq2 ⊢ e = iEdg ⁡ G ⁡ i → A B ⊆ e ↔ A B ⊆ iEdg ⁡ G ⁡ i
34 33 adantl ⊢ i ∈ dom ⁡ iEdg ⁡ G ∧ e = iEdg ⁡ G ⁡ i → A B ⊆ e ↔ A B ⊆ iEdg ⁡ G ⁡ i
35 34 biimpa ⊢ i ∈ dom ⁡ iEdg ⁡ G ∧ e = iEdg ⁡ G ⁡ i ∧ A B ⊆ e → A B ⊆ iEdg ⁡ G ⁡ i
36 35 adantl ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ e = iEdg ⁡ G ⁡ i ∧ A B ⊆ e → A B ⊆ iEdg ⁡ G ⁡ i
37 36 adantr ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ e = iEdg ⁡ G ⁡ i ∧ A B ⊆ e ∧ A ≠ B → A B ⊆ iEdg ⁡ G ⁡ i
38 24 25 26 27 32 37 1 17 1pthond ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ e = iEdg ⁡ G ⁡ i ∧ A B ⊆ e → ⟨“ i ”⟩ A PathsOn ⁡ G B ⟨“ AB ”⟩
39 breq12 ⊢ f = ⟨“ i ”⟩ ∧ p = ⟨“ AB ”⟩ → f A PathsOn ⁡ G B p ↔ ⟨“ i ”⟩ A PathsOn ⁡ G B ⟨“ AB ”⟩
40 39 spc2egv ⊢ ⟨“ i ”⟩ ∈ Word V ∧ ⟨“ AB ”⟩ ∈ Word V → ⟨“ i ”⟩ A PathsOn ⁡ G B ⟨“ AB ”⟩ → ∃ f ∃ p f A PathsOn ⁡ G B p
41 23 38 40 mpsyl ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ e = iEdg ⁡ G ⁡ i ∧ A B ⊆ e → ∃ f ∃ p f A PathsOn ⁡ G B p
42 41 exp44 ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → i ∈ dom ⁡ iEdg ⁡ G → e = iEdg ⁡ G ⁡ i → A B ⊆ e → ∃ f ∃ p f A PathsOn ⁡ G B p
43 42 rexlimdv ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → ∃ i ∈ dom ⁡ iEdg ⁡ G e = iEdg ⁡ G ⁡ i → A B ⊆ e → ∃ f ∃ p f A PathsOn ⁡ G B p
44 20 43 sylbid ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → e ∈ E → A B ⊆ e → ∃ f ∃ p f A PathsOn ⁡ G B p
45 44 rexlimdv ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ A ≠ B → ∃ e ∈ E A B ⊆ e → ∃ f ∃ p f A PathsOn ⁡ G B p
46 45 3exp ⊢ G ∈ UHGraph → A ∈ V ∧ B ∈ V → A ≠ B → ∃ e ∈ E A B ⊆ e → ∃ f ∃ p f A PathsOn ⁡ G B p
47 46 com34 ⊢ G ∈ UHGraph → A ∈ V ∧ B ∈ V → ∃ e ∈ E A B ⊆ e → A ≠ B → ∃ f ∃ p f A PathsOn ⁡ G B p
48 47 3imp ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ ∃ e ∈ E A B ⊆ e → A ≠ B → ∃ f ∃ p f A PathsOn ⁡ G B p
49 48 com12 ⊢ A ≠ B → G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ ∃ e ∈ E A B ⊆ e → ∃ f ∃ p f A PathsOn ⁡ G B p
50 15 49 pm2.61ine ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ ∃ e ∈ E A B ⊆ e → ∃ f ∃ p f A PathsOn ⁡ G B p