Metamath Proof Explorer

Theorem uspgrlimlem3

Description: Lemma 3 for uspgrlim . (Contributed by AV, 16-Aug-2025)

Ref Expression
Hypotheses uspgrlim.v ⊢ V = Vtx ⁡ G
uspgrlim.w ⊢ W = Vtx ⁡ H
uspgrlim.n ⊢ N = G ClNeighbVtx v
uspgrlim.m ⊢ M = H ClNeighbVtx F ⁡ v
uspgrlim.i ⊢ I = Edg ⁡ G
uspgrlim.j ⊢ J = Edg ⁡ H
uspgrlim.k ⊢ K = x ∈ I | x ⊆ N
uspgrlim.l ⊢ L = x ∈ J | x ⊆ M
Assertion uspgrlimlem3 ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → e ∈ K → f e = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 ⁡ e

Proof

Step Hyp Ref Expression
1 uspgrlim.v ⊢ V = Vtx ⁡ G
2 uspgrlim.w ⊢ W = Vtx ⁡ H
3 uspgrlim.n ⊢ N = G ClNeighbVtx v
4 uspgrlim.m ⊢ M = H ClNeighbVtx F ⁡ v
5 uspgrlim.i ⊢ I = Edg ⁡ G
6 uspgrlim.j ⊢ J = Edg ⁡ H
7 uspgrlim.k ⊢ K = x ∈ I | x ⊆ N
8 uspgrlim.l ⊢ L = x ∈ J | x ⊆ M
9 sseq1 ⊢ x = e → x ⊆ N ↔ e ⊆ N
10 9 7 elrab2 ⊢ e ∈ K ↔ e ∈ I ∧ e ⊆ N
11 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
12 11 uspgrf1oedg ⊢ G ∈ USHGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto Edg ⁡ G
13 f1ocnv ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto Edg ⁡ G → iEdg ⁡ G -1 : Edg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ G
14 f1of ⊢ iEdg ⁡ G -1 : Edg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ G → iEdg ⁡ G -1 : Edg ⁡ G ⟶ dom ⁡ iEdg ⁡ G
15 12 13 14 3syl ⊢ G ∈ USHGraph → iEdg ⁡ G -1 : Edg ⁡ G ⟶ dom ⁡ iEdg ⁡ G
16 15 3ad2ant1 ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → iEdg ⁡ G -1 : Edg ⁡ G ⟶ dom ⁡ iEdg ⁡ G
17 5 eleq2i ⊢ e ∈ I ↔ e ∈ Edg ⁡ G
18 17 birani ⊢ e ∈ I ∧ e ⊆ N → e ∈ Edg ⁡ G
19 fvco3 ⊢ iEdg ⁡ G -1 : Edg ⁡ G ⟶ dom ⁡ iEdg ⁡ G ∧ e ∈ Edg ⁡ G → iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 ⁡ e = iEdg ⁡ H ∘ h ⁡ iEdg ⁡ G -1 ⁡ e
20 16 18 19 syl2an ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i ∧ e ∈ I ∧ e ⊆ N → iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 ⁡ e = iEdg ⁡ H ∘ h ⁡ iEdg ⁡ G -1 ⁡ e
21 f1ocnvdm ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto Edg ⁡ G ∧ e ∈ Edg ⁡ G → iEdg ⁡ G -1 ⁡ e ∈ dom ⁡ iEdg ⁡ G
22 12 18 21 syl2an ⊢ G ∈ USHGraph ∧ e ∈ I ∧ e ⊆ N → iEdg ⁡ G -1 ⁡ e ∈ dom ⁡ iEdg ⁡ G
23 f1ocnvfv2 ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto Edg ⁡ G ∧ e ∈ Edg ⁡ G → iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e = e
24 12 18 23 syl2an ⊢ G ∈ USHGraph ∧ e ∈ I ∧ e ⊆ N → iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e = e
25 simprr ⊢ G ∈ USHGraph ∧ e ∈ I ∧ e ⊆ N → e ⊆ N
26 24 25 eqsstrd ⊢ G ∈ USHGraph ∧ e ∈ I ∧ e ⊆ N → iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e ⊆ N
27 22 26 jca ⊢ G ∈ USHGraph ∧ e ∈ I ∧ e ⊆ N → iEdg ⁡ G -1 ⁡ e ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e ⊆ N
28 27 adantlr ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ e ∈ I ∧ e ⊆ N → iEdg ⁡ G -1 ⁡ e ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e ⊆ N
29 fveq2 ⊢ x = iEdg ⁡ G -1 ⁡ e → iEdg ⁡ G ⁡ x = iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e
30 29 sseq1d ⊢ x = iEdg ⁡ G -1 ⁡ e → iEdg ⁡ G ⁡ x ⊆ N ↔ iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e ⊆ N
31 30 elrab ⊢ iEdg ⁡ G -1 ⁡ e ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ↔ iEdg ⁡ G -1 ⁡ e ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e ⊆ N
32 28 31 sylibr ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ e ∈ I ∧ e ⊆ N → iEdg ⁡ G -1 ⁡ e ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N
33 fveq2 ⊢ i = iEdg ⁡ G -1 ⁡ e → iEdg ⁡ G ⁡ i = iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e
34 33 imaeq2d ⊢ i = iEdg ⁡ G -1 ⁡ e → f iEdg ⁡ G ⁡ i = f iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e
35 2fveq3 ⊢ i = iEdg ⁡ G -1 ⁡ e → iEdg ⁡ H ⁡ h ⁡ i = iEdg ⁡ H ⁡ h ⁡ iEdg ⁡ G -1 ⁡ e
36 34 35 eqeq12d ⊢ i = iEdg ⁡ G -1 ⁡ e → f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i ↔ f iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e = iEdg ⁡ H ⁡ h ⁡ iEdg ⁡ G -1 ⁡ e
37 36 rspcv ⊢ iEdg ⁡ G -1 ⁡ e ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N → ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → f iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e = iEdg ⁡ H ⁡ h ⁡ iEdg ⁡ G -1 ⁡ e
38 32 37 syl ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ e ∈ I ∧ e ⊆ N → ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → f iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e = iEdg ⁡ H ⁡ h ⁡ iEdg ⁡ G -1 ⁡ e
39 eqcom ⊢ f iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e = iEdg ⁡ H ⁡ h ⁡ iEdg ⁡ G -1 ⁡ e ↔ iEdg ⁡ H ⁡ h ⁡ iEdg ⁡ G -1 ⁡ e = f iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e
40 f1of ⊢ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R → h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ R
41 40 ad2antlr ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ e ∈ I ∧ e ⊆ N → h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ R
42 41 32 fvco3d ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ e ∈ I ∧ e ⊆ N → iEdg ⁡ H ∘ h ⁡ iEdg ⁡ G -1 ⁡ e = iEdg ⁡ H ⁡ h ⁡ iEdg ⁡ G -1 ⁡ e
43 42 eqcomd ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ e ∈ I ∧ e ⊆ N → iEdg ⁡ H ⁡ h ⁡ iEdg ⁡ G -1 ⁡ e = iEdg ⁡ H ∘ h ⁡ iEdg ⁡ G -1 ⁡ e
44 12 adantr ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto Edg ⁡ G
45 44 18 23 syl2an ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ e ∈ I ∧ e ⊆ N → iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e = e
46 45 imaeq2d ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ e ∈ I ∧ e ⊆ N → f iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e = f e
47 43 46 eqeq12d ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ e ∈ I ∧ e ⊆ N → iEdg ⁡ H ⁡ h ⁡ iEdg ⁡ G -1 ⁡ e = f iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e ↔ iEdg ⁡ H ∘ h ⁡ iEdg ⁡ G -1 ⁡ e = f e
48 47 biimpd ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ e ∈ I ∧ e ⊆ N → iEdg ⁡ H ⁡ h ⁡ iEdg ⁡ G -1 ⁡ e = f iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e → iEdg ⁡ H ∘ h ⁡ iEdg ⁡ G -1 ⁡ e = f e
49 39 48 biimtrid ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ e ∈ I ∧ e ⊆ N → f iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e = iEdg ⁡ H ⁡ h ⁡ iEdg ⁡ G -1 ⁡ e → iEdg ⁡ H ∘ h ⁡ iEdg ⁡ G -1 ⁡ e = f e
50 38 49 syld ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ e ∈ I ∧ e ⊆ N → ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → iEdg ⁡ H ∘ h ⁡ iEdg ⁡ G -1 ⁡ e = f e
51 50 ex ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R → e ∈ I ∧ e ⊆ N → ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → iEdg ⁡ H ∘ h ⁡ iEdg ⁡ G -1 ⁡ e = f e
52 51 com23 ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R → ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → e ∈ I ∧ e ⊆ N → iEdg ⁡ H ∘ h ⁡ iEdg ⁡ G -1 ⁡ e = f e
53 52 ex ⊢ G ∈ USHGraph → h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R → ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → e ∈ I ∧ e ⊆ N → iEdg ⁡ H ∘ h ⁡ iEdg ⁡ G -1 ⁡ e = f e
54 53 3imp1 ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i ∧ e ∈ I ∧ e ⊆ N → iEdg ⁡ H ∘ h ⁡ iEdg ⁡ G -1 ⁡ e = f e
55 20 54 eqtr2d ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i ∧ e ∈ I ∧ e ⊆ N → f e = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 ⁡ e
56 55 ex ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → e ∈ I ∧ e ⊆ N → f e = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 ⁡ e
57 10 56 biimtrid ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → e ∈ K → f e = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 ⁡ e