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) Remove is-walk hypothesis. (Revised by SN, 13-Dec-2024)

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
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 1 fvexi ⊢ V ∈ V
5 simp1 ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V → G ∈ V
6 simp2 ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V → A ∈ V
7 6 1 eleqtrdi ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V → A ∈ Vtx ⁡ G
8 simp3 ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V → B ∈ V
9 8 1 eleqtrdi ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V → B ∈ Vtx ⁡ G
10 5 7 9 3 mptmpoopabovd ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V → A W ⁡ G B = f p | f A O ⁡ G B p ∧ f Q ⁡ G p
11 fveq2 ⊢ g = G → Vtx ⁡ g = Vtx ⁡ G
12 11 1 eqtr4di ⊢ g = G → Vtx ⁡ g = V
13 fveq2 ⊢ g = G → O ⁡ g = O ⁡ G
14 13 oveqd ⊢ g = G → a O ⁡ g b = a O ⁡ G b
15 14 breqd ⊢ g = G → f a O ⁡ g b p ↔ f a O ⁡ G b p
16 fveq2 ⊢ g = G → Q ⁡ g = Q ⁡ G
17 16 breqd ⊢ g = G → f Q ⁡ g p ↔ f Q ⁡ G p
18 15 17 anbi12d ⊢ g = G → f a O ⁡ g b p ∧ f Q ⁡ g p ↔ f a O ⁡ G b p ∧ f Q ⁡ G p
19 3 10 12 12 18 bropfvvvv ⊢ V ∈ V ∧ V ∈ V → F A W ⁡ G B P → G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V
20 4 4 19 mp2an ⊢ F A W ⁡ G B P → G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V
21 3anass ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V ↔ G ∈ V ∧ A ∈ V ∧ B ∈ V
22 21 anbi1i ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V ↔ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V
23 df-3an ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V ↔ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V
24 22 23 bitr4i ⊢ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V ↔ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V
25 20 24 sylibr ⊢ F A W ⁡ G B P → G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ F ∈ V ∧ P ∈ V
26 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
27 26 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
28 25 27 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
29 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
30 28 29 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