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 biimpi ⊢ e ∈ I → e ∈ Edg ⁡ G
19 18 adantr ⊢ e ∈ I ∧ e ⊆ N → e ∈ Edg ⁡ G
20 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
21 16 19 20 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
22 f1ocnvdm ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto Edg ⁡ G ∧ e ∈ Edg ⁡ G → iEdg ⁡ G -1 ⁡ e ∈ dom ⁡ iEdg ⁡ G
23 12 19 22 syl2an ⊢ G ∈ USHGraph ∧ e ∈ I ∧ e ⊆ N → iEdg ⁡ G -1 ⁡ e ∈ dom ⁡ iEdg ⁡ G
24 f1ocnvfv2 ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto Edg ⁡ G ∧ e ∈ Edg ⁡ G → iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e = e
25 12 19 24 syl2an ⊢ G ∈ USHGraph ∧ e ∈ I ∧ e ⊆ N → iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e = e
26 simprr ⊢ G ∈ USHGraph ∧ e ∈ I ∧ e ⊆ N → e ⊆ N
27 25 26 eqsstrd ⊢ G ∈ USHGraph ∧ e ∈ I ∧ e ⊆ N → iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e ⊆ N
28 23 27 jca ⊢ G ∈ USHGraph ∧ e ∈ I ∧ e ⊆ N → iEdg ⁡ G -1 ⁡ e ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e ⊆ N
29 28 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
30 fveq2 ⊢ x = iEdg ⁡ G -1 ⁡ e → iEdg ⁡ G ⁡ x = iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e
31 30 sseq1d ⊢ x = iEdg ⁡ G -1 ⁡ e → iEdg ⁡ G ⁡ x ⊆ N ↔ iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e ⊆ N
32 31 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
33 29 32 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
34 fveq2 ⊢ i = iEdg ⁡ G -1 ⁡ e → iEdg ⁡ G ⁡ i = iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e
35 34 imaeq2d ⊢ i = iEdg ⁡ G -1 ⁡ e → f iEdg ⁡ G ⁡ i = f iEdg ⁡ G ⁡ iEdg ⁡ G -1 ⁡ e
36 2fveq3 ⊢ i = iEdg ⁡ G -1 ⁡ e → iEdg ⁡ H ⁡ h ⁡ i = iEdg ⁡ H ⁡ h ⁡ iEdg ⁡ G -1 ⁡ e
37 35 36 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
38 37 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
39 33 38 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
40 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
41 f1of ⊢ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto R → h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ R
42 41 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
43 42 33 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
44 43 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
45 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
46 45 19 24 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
47 46 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
48 44 47 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
49 48 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
50 40 49 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
51 39 50 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
52 51 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
53 52 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
54 53 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
55 54 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
56 21 55 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
57 56 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
58 10 57 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