Metamath Proof Explorer

Theorem isomgrtrlem

Description: Lemma for isomgrtr . (Contributed by AV, 5-Dec-2022)

Ref Expression
Assertion isomgrtrlem ⊢ A ∈ UHGraph ∧ B ∈ UHGraph ∧ C ∈ X ∧ f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ v : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ C ∧ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ∧ w : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ C ∧ ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k → ∀ j ∈ dom ⁡ iEdg ⁡ A v ∘ f iEdg ⁡ A ⁡ j = iEdg ⁡ C ⁡ w ∘ g ⁡ j

Proof

Step Hyp Ref Expression
1 imaco ⊢ v ∘ f iEdg ⁡ A ⁡ j = v f iEdg ⁡ A ⁡ j
2 1 a1i ⊢ A ∈ UHGraph ∧ B ∈ UHGraph ∧ C ∈ X ∧ f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ v : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ C ∧ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ∧ w : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ C ∧ ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k ∧ j ∈ dom ⁡ iEdg ⁡ A → v ∘ f iEdg ⁡ A ⁡ j = v f iEdg ⁡ A ⁡ j
3 fveq2 ⊢ i = j → iEdg ⁡ A ⁡ i = iEdg ⁡ A ⁡ j
4 3 imaeq2d ⊢ i = j → f iEdg ⁡ A ⁡ i = f iEdg ⁡ A ⁡ j
5 2fveq3 ⊢ i = j → iEdg ⁡ B ⁡ g ⁡ i = iEdg ⁡ B ⁡ g ⁡ j
6 4 5 eqeq12d ⊢ i = j → f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ↔ f iEdg ⁡ A ⁡ j = iEdg ⁡ B ⁡ g ⁡ j
7 6 rspccv ⊢ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i → j ∈ dom ⁡ iEdg ⁡ A → f iEdg ⁡ A ⁡ j = iEdg ⁡ B ⁡ g ⁡ j
8 7 adantl ⊢ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i → j ∈ dom ⁡ iEdg ⁡ A → f iEdg ⁡ A ⁡ j = iEdg ⁡ B ⁡ g ⁡ j
9 8 ad2antlr ⊢ A ∈ UHGraph ∧ B ∈ UHGraph ∧ C ∈ X ∧ f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ v : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ C ∧ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ∧ w : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ C ∧ ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k → j ∈ dom ⁡ iEdg ⁡ A → f iEdg ⁡ A ⁡ j = iEdg ⁡ B ⁡ g ⁡ j
10 9 imp ⊢ A ∈ UHGraph ∧ B ∈ UHGraph ∧ C ∈ X ∧ f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ v : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ C ∧ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ∧ w : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ C ∧ ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k ∧ j ∈ dom ⁡ iEdg ⁡ A → f iEdg ⁡ A ⁡ j = iEdg ⁡ B ⁡ g ⁡ j
11 10 imaeq2d ⊢ A ∈ UHGraph ∧ B ∈ UHGraph ∧ C ∈ X ∧ f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ v : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ C ∧ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ∧ w : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ C ∧ ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k ∧ j ∈ dom ⁡ iEdg ⁡ A → v f iEdg ⁡ A ⁡ j = v iEdg ⁡ B ⁡ g ⁡ j
12 simplrr ⊢ A ∈ UHGraph ∧ B ∈ UHGraph ∧ C ∈ X ∧ f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ v : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ C ∧ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ∧ w : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ C ∧ ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k ∧ j ∈ dom ⁡ iEdg ⁡ A → ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k
13 f1of ⊢ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B → g : dom ⁡ iEdg ⁡ A ⟶ dom ⁡ iEdg ⁡ B
14 ffvelrn ⊢ g : dom ⁡ iEdg ⁡ A ⟶ dom ⁡ iEdg ⁡ B ∧ j ∈ dom ⁡ iEdg ⁡ A → g ⁡ j ∈ dom ⁡ iEdg ⁡ B
15 14 ex ⊢ g : dom ⁡ iEdg ⁡ A ⟶ dom ⁡ iEdg ⁡ B → j ∈ dom ⁡ iEdg ⁡ A → g ⁡ j ∈ dom ⁡ iEdg ⁡ B
16 13 15 syl ⊢ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B → j ∈ dom ⁡ iEdg ⁡ A → g ⁡ j ∈ dom ⁡ iEdg ⁡ B
17 16 adantr ⊢ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i → j ∈ dom ⁡ iEdg ⁡ A → g ⁡ j ∈ dom ⁡ iEdg ⁡ B
18 17 ad2antlr ⊢ A ∈ UHGraph ∧ B ∈ UHGraph ∧ C ∈ X ∧ f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ v : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ C ∧ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ∧ w : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ C ∧ ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k → j ∈ dom ⁡ iEdg ⁡ A → g ⁡ j ∈ dom ⁡ iEdg ⁡ B
19 18 imp ⊢ A ∈ UHGraph ∧ B ∈ UHGraph ∧ C ∈ X ∧ f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ v : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ C ∧ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ∧ w : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ C ∧ ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k ∧ j ∈ dom ⁡ iEdg ⁡ A → g ⁡ j ∈ dom ⁡ iEdg ⁡ B
20 fveq2 ⊢ k = g ⁡ j → iEdg ⁡ B ⁡ k = iEdg ⁡ B ⁡ g ⁡ j
21 20 imaeq2d ⊢ k = g ⁡ j → v iEdg ⁡ B ⁡ k = v iEdg ⁡ B ⁡ g ⁡ j
22 2fveq3 ⊢ k = g ⁡ j → iEdg ⁡ C ⁡ w ⁡ k = iEdg ⁡ C ⁡ w ⁡ g ⁡ j
23 21 22 eqeq12d ⊢ k = g ⁡ j → v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k ↔ v iEdg ⁡ B ⁡ g ⁡ j = iEdg ⁡ C ⁡ w ⁡ g ⁡ j
24 23 rspccv ⊢ ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k → g ⁡ j ∈ dom ⁡ iEdg ⁡ B → v iEdg ⁡ B ⁡ g ⁡ j = iEdg ⁡ C ⁡ w ⁡ g ⁡ j
25 12 19 24 sylc ⊢ A ∈ UHGraph ∧ B ∈ UHGraph ∧ C ∈ X ∧ f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ v : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ C ∧ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ∧ w : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ C ∧ ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k ∧ j ∈ dom ⁡ iEdg ⁡ A → v iEdg ⁡ B ⁡ g ⁡ j = iEdg ⁡ C ⁡ w ⁡ g ⁡ j
26 11 25 eqtrd ⊢ A ∈ UHGraph ∧ B ∈ UHGraph ∧ C ∈ X ∧ f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ v : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ C ∧ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ∧ w : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ C ∧ ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k ∧ j ∈ dom ⁡ iEdg ⁡ A → v f iEdg ⁡ A ⁡ j = iEdg ⁡ C ⁡ w ⁡ g ⁡ j
27 f1ofn ⊢ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B → g Fn dom ⁡ iEdg ⁡ A
28 27 adantr ⊢ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i → g Fn dom ⁡ iEdg ⁡ A
29 28 ad2antlr ⊢ A ∈ UHGraph ∧ B ∈ UHGraph ∧ C ∈ X ∧ f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ v : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ C ∧ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ∧ w : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ C ∧ ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k → g Fn dom ⁡ iEdg ⁡ A
30 fvco2 ⊢ g Fn dom ⁡ iEdg ⁡ A ∧ j ∈ dom ⁡ iEdg ⁡ A → w ∘ g ⁡ j = w ⁡ g ⁡ j
31 29 30 sylan ⊢ A ∈ UHGraph ∧ B ∈ UHGraph ∧ C ∈ X ∧ f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ v : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ C ∧ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ∧ w : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ C ∧ ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k ∧ j ∈ dom ⁡ iEdg ⁡ A → w ∘ g ⁡ j = w ⁡ g ⁡ j
32 31 eqcomd ⊢ A ∈ UHGraph ∧ B ∈ UHGraph ∧ C ∈ X ∧ f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ v : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ C ∧ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ∧ w : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ C ∧ ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k ∧ j ∈ dom ⁡ iEdg ⁡ A → w ⁡ g ⁡ j = w ∘ g ⁡ j
33 32 fveq2d ⊢ A ∈ UHGraph ∧ B ∈ UHGraph ∧ C ∈ X ∧ f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ v : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ C ∧ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ∧ w : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ C ∧ ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k ∧ j ∈ dom ⁡ iEdg ⁡ A → iEdg ⁡ C ⁡ w ⁡ g ⁡ j = iEdg ⁡ C ⁡ w ∘ g ⁡ j
34 2 26 33 3eqtrd ⊢ A ∈ UHGraph ∧ B ∈ UHGraph ∧ C ∈ X ∧ f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ v : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ C ∧ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ∧ w : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ C ∧ ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k ∧ j ∈ dom ⁡ iEdg ⁡ A → v ∘ f iEdg ⁡ A ⁡ j = iEdg ⁡ C ⁡ w ∘ g ⁡ j
35 34 ralrimiva ⊢ A ∈ UHGraph ∧ B ∈ UHGraph ∧ C ∈ X ∧ f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ v : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ C ∧ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ∧ w : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ C ∧ ∀ k ∈ dom ⁡ iEdg ⁡ B v iEdg ⁡ B ⁡ k = iEdg ⁡ C ⁡ w ⁡ k → ∀ j ∈ dom ⁡ iEdg ⁡ A v ∘ f iEdg ⁡ A ⁡ j = iEdg ⁡ C ⁡ w ∘ g ⁡ j