Metamath Proof Explorer

Theorem uspgrlimlem4

Description: Lemma 4 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 uspgrlimlem4 ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G ⁡ i

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 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
10 9 uspgrf1oedg ⊢ G ∈ USHGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto Edg ⁡ G
11 f1of ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto Edg ⁡ G → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ Edg ⁡ G
12 10 11 syl ⊢ G ∈ USHGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ Edg ⁡ G
13 12 ad2antrr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ Edg ⁡ G
14 simpl ⊢ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → i ∈ dom ⁡ iEdg ⁡ G
15 fvco3 ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ Edg ⁡ G ∧ i ∈ dom ⁡ iEdg ⁡ G → iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G ⁡ i = iEdg ⁡ H -1 ∘ g ⁡ iEdg ⁡ G ⁡ i
16 15 fveq2d ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ Edg ⁡ G ∧ i ∈ dom ⁡ iEdg ⁡ G → iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ⁡ iEdg ⁡ G ⁡ i
17 13 14 16 syl2an ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ⁡ iEdg ⁡ G ⁡ i
18 eqid ⊢ iEdg ⁡ H = iEdg ⁡ H
19 18 uspgrf1oedg ⊢ H ∈ USHGraph → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 onto Edg ⁡ H
20 19 ad3antlr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 onto Edg ⁡ H
21 ssrab2 ⊢ x ∈ J | x ⊆ M ⊆ J
22 6 eqcomi ⊢ Edg ⁡ H = J
23 21 8 22 3sstr4i ⊢ L ⊆ Edg ⁡ H
24 f1of ⊢ g : K ⟶ 1-1 onto L → g : K ⟶ L
25 24 adantr ⊢ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → g : K ⟶ L
26 25 adantl ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → g : K ⟶ L
27 26 adantr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → g : K ⟶ L
28 13 ffund ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → Fun ⁡ iEdg ⁡ G
29 9 iedgedg ⊢ Fun ⁡ iEdg ⁡ G ∧ i ∈ dom ⁡ iEdg ⁡ G → iEdg ⁡ G ⁡ i ∈ Edg ⁡ G
30 28 14 29 syl2an ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → iEdg ⁡ G ⁡ i ∈ Edg ⁡ G
31 30 5 eleqtrrdi ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → iEdg ⁡ G ⁡ i ∈ I
32 simprr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → iEdg ⁡ G ⁡ i ⊆ N
33 sseq1 ⊢ x = iEdg ⁡ G ⁡ i → x ⊆ N ↔ iEdg ⁡ G ⁡ i ⊆ N
34 33 7 elrab2 ⊢ iEdg ⁡ G ⁡ i ∈ K ↔ iEdg ⁡ G ⁡ i ∈ I ∧ iEdg ⁡ G ⁡ i ⊆ N
35 31 32 34 sylanbrc ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → iEdg ⁡ G ⁡ i ∈ K
36 27 35 ffvelcdmd ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → g ⁡ iEdg ⁡ G ⁡ i ∈ L
37 23 36 sselid ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → g ⁡ iEdg ⁡ G ⁡ i ∈ Edg ⁡ H
38 f1ocnvfv2 ⊢ iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 onto Edg ⁡ H ∧ g ⁡ iEdg ⁡ G ⁡ i ∈ Edg ⁡ H → iEdg ⁡ H ⁡ iEdg ⁡ H -1 ⁡ g ⁡ iEdg ⁡ G ⁡ i = g ⁡ iEdg ⁡ G ⁡ i
39 20 37 38 syl2anc ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → iEdg ⁡ H ⁡ iEdg ⁡ H -1 ⁡ g ⁡ iEdg ⁡ G ⁡ i = g ⁡ iEdg ⁡ G ⁡ i
40 fvco3 ⊢ g : K ⟶ L ∧ iEdg ⁡ G ⁡ i ∈ K → iEdg ⁡ H -1 ∘ g ⁡ iEdg ⁡ G ⁡ i = iEdg ⁡ H -1 ⁡ g ⁡ iEdg ⁡ G ⁡ i
41 40 fveq2d ⊢ g : K ⟶ L ∧ iEdg ⁡ G ⁡ i ∈ K → iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ⁡ iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ iEdg ⁡ H -1 ⁡ g ⁡ iEdg ⁡ G ⁡ i
42 27 35 41 syl2anc ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ⁡ iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ iEdg ⁡ H -1 ⁡ g ⁡ iEdg ⁡ G ⁡ i
43 5 eqcomi ⊢ Edg ⁡ G = I
44 feq3 ⊢ Edg ⁡ G = I → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ Edg ⁡ G ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ I
45 43 44 ax-mp ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ Edg ⁡ G ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ I
46 45 biimpi ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ Edg ⁡ G → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ I
47 10 11 46 3syl ⊢ G ∈ USHGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ I
48 47 ad2antrr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ I
49 14 adantl ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → i ∈ dom ⁡ iEdg ⁡ G
50 48 49 ffvelcdmd ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → iEdg ⁡ G ⁡ i ∈ I
51 simprr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → iEdg ⁡ G ⁡ i ⊆ N
52 50 51 34 sylanbrc ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → iEdg ⁡ G ⁡ i ∈ K
53 imaeq2 ⊢ e = iEdg ⁡ G ⁡ i → f e = f iEdg ⁡ G ⁡ i
54 fveq2 ⊢ e = iEdg ⁡ G ⁡ i → g ⁡ e = g ⁡ iEdg ⁡ G ⁡ i
55 53 54 eqeq12d ⊢ e = iEdg ⁡ G ⁡ i → f e = g ⁡ e ↔ f iEdg ⁡ G ⁡ i = g ⁡ iEdg ⁡ G ⁡ i
56 55 rspcv ⊢ iEdg ⁡ G ⁡ i ∈ K → ∀ e ∈ K f e = g ⁡ e → f iEdg ⁡ G ⁡ i = g ⁡ iEdg ⁡ G ⁡ i
57 52 56 syl ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → ∀ e ∈ K f e = g ⁡ e → f iEdg ⁡ G ⁡ i = g ⁡ iEdg ⁡ G ⁡ i
58 57 ex ⊢ G ∈ USHGraph ∧ H ∈ USHGraph → i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → ∀ e ∈ K f e = g ⁡ e → f iEdg ⁡ G ⁡ i = g ⁡ iEdg ⁡ G ⁡ i
59 58 com23 ⊢ G ∈ USHGraph ∧ H ∈ USHGraph → ∀ e ∈ K f e = g ⁡ e → i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → f iEdg ⁡ G ⁡ i = g ⁡ iEdg ⁡ G ⁡ i
60 59 adantld ⊢ G ∈ USHGraph ∧ H ∈ USHGraph → g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → f iEdg ⁡ G ⁡ i = g ⁡ iEdg ⁡ G ⁡ i
61 60 imp31 ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → f iEdg ⁡ G ⁡ i = g ⁡ iEdg ⁡ G ⁡ i
62 39 42 61 3eqtr4d ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ⁡ iEdg ⁡ G ⁡ i = f iEdg ⁡ G ⁡ i
63 17 62 eqtr2d ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G ⁡ i
64 63 ex ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G ⁡ i