Metamath Proof Explorer

Theorem wksonproplem

Description: Lemma for theorems for properties of walks between two vertices, e.g., trlsonprop . (Contributed by AV, 16-Jan-2021)

Ref Expression
Hypotheses wksonproplem.v ⊢ V = Vtx ⁡ G
wksonproplem.b ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V → F A W ⁡ G B P ↔ F A O ⁡ G B P ∧ F Q ⁡ G P
wksonproplem.d ⊢ W = g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f a O ⁡ g b p ∧ f Q ⁡ g p
wksonproplem.w ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ f Q ⁡ G p → f Walks ⁡ G p
Assertion wksonproplem ⊢ F A W ⁡ G B P → G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V ∧ F A O ⁡ G B P ∧ F Q ⁡ G P

Proof

Step Hyp Ref Expression
1 wksonproplem.v ⊢ V = Vtx ⁡ G
2 wksonproplem.b ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V → F A W ⁡ G B P ↔ F A O ⁡ G B P ∧ F Q ⁡ G P
3 wksonproplem.d ⊢ W = g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f a O ⁡ g b p ∧ f Q ⁡ g p
4 wksonproplem.w ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ f Q ⁡ G p → f Walks ⁡ G p
5 1 fvexi ⊢ V ∈ V
6 simp1 ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V → G ∈ V
7 simp2 ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V → A ∈ V
8 7 1 eleqtrdi ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V → A ∈ Vtx ⁡ G
9 simp3 ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V → B ∈ V
10 9 1 eleqtrdi ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V → B ∈ Vtx ⁡ G
11 wksv ⊢ f p | f Walks ⁡ G p ∈ V
12 11 a1i ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V → f p | f Walks ⁡ G p ∈ V
13 6 8 10 12 4 3 mptmpoopabovd ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V → A W ⁡ G B = f p | f A O ⁡ G B p ∧ f Q ⁡ G p
14 fveq2 ⊢ g = G → Vtx ⁡ g = Vtx ⁡ G
15 14 1 syl6eqr ⊢ g = G → Vtx ⁡ g = V
16 fveq2 ⊢ g = G → O ⁡ g = O ⁡ G
17 16 oveqd ⊢ g = G → a O ⁡ g b = a O ⁡ G b
18 17 breqd ⊢ g = G → f a O ⁡ g b p ↔ f a O ⁡ G b p
19 fveq2 ⊢ g = G → Q ⁡ g = Q ⁡ G
20 19 breqd ⊢ g = G → f Q ⁡ g p ↔ f Q ⁡ G p
21 18 20 anbi12d ⊢ g = G → f a O ⁡ g b p ∧ f Q ⁡ g p ↔ f a O ⁡ G b p ∧ f Q ⁡ G p
22 3 13 15 15 21 bropfvvvv ⊢ V ∈ V ∧ V ∈ V → F A W ⁡ G B P → G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V
23 5 5 22 mp2an ⊢ F A W ⁡ G B P → G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V
24 3anass ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V ↔ G ∈ V ∧ A ∈ V ∧ B ∈ V
25 24 anbi1i ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V ↔ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V
26 df-3an ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V ↔ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V
27 25 26 bitr4i ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V ↔ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V
28 23 27 sylibr ⊢ F A W ⁡ G B P → G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V
29 2 biimpd ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V → F A W ⁡ G B P → F A O ⁡ G B P ∧ F Q ⁡ G P
30 29 imdistani ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V ∧ F A W ⁡ G B P → G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V ∧ F A O ⁡ G B P ∧ F Q ⁡ G P
31 28 30 mpancom ⊢ F A W ⁡ G B P → G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V ∧ F A O ⁡ G B P ∧ F Q ⁡ G P
32 df-3an ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V ∧ F A O ⁡ G B P ∧ F Q ⁡ G P ↔ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V ∧ F A O ⁡ G B P ∧ F Q ⁡ G P
33 31 32 sylibr ⊢ F A W ⁡ G B P → G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V ∧ F A O ⁡ G B P ∧ F Q ⁡ G P