Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  uspgrlimlem3 Structured version   Visualization version   GIF version

Theorem uspgrlimlem3 47815
Description: Lemma 3 for uspgrlim 47817. (Contributed by AV, 16-Aug-2025.)
Hypotheses
Ref Expression
uspgrlim.v 𝑉 = (Vtx‘𝐺)
uspgrlim.w 𝑊 = (Vtx‘𝐻)
uspgrlim.n 𝑁 = (𝐺 ClNeighbVtx 𝑣)
uspgrlim.m 𝑀 = (𝐻 ClNeighbVtx (𝐹𝑣))
uspgrlim.i 𝐼 = (Edg‘𝐺)
uspgrlim.j 𝐽 = (Edg‘𝐻)
uspgrlim.k 𝐾 = {𝑥𝐼𝑥𝑁}
uspgrlim.l 𝐿 = {𝑥𝐽𝑥𝑀}
Assertion
Ref Expression
uspgrlimlem3 ((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅 ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖))) → (𝑒𝐾 → (𝑓𝑒) = ((((iEdg‘𝐻) ∘ ) ∘ (iEdg‘𝐺))‘𝑒)))
Distinct variable groups:   𝑖,𝐺,𝑥   𝑖,𝐻,𝑥   𝑥,𝐼   𝑥,𝐽   𝑥,𝑀   𝑖,𝑁,𝑥   𝑒,𝑖,𝑥   𝑓,𝑖   ,𝑖
Allowed substitution hints:   𝑅(𝑥,𝑣,𝑒,𝑓,,𝑖)   𝐹(𝑥,𝑣,𝑒,𝑓,,𝑖)   𝐺(𝑣,𝑒,𝑓,)   𝐻(𝑣,𝑒,𝑓,)   𝐼(𝑣,𝑒,𝑓,,𝑖)   𝐽(𝑣,𝑒,𝑓,,𝑖)   𝐾(𝑥,𝑣,𝑒,𝑓,,𝑖)   𝐿(𝑥,𝑣,𝑒,𝑓,,𝑖)   𝑀(𝑣,𝑒,𝑓,,𝑖)   𝑁(𝑣,𝑒,𝑓,)   𝑉(𝑥,𝑣,𝑒,𝑓,,𝑖)   𝑊(𝑥,𝑣,𝑒,𝑓,,𝑖)

Proof of Theorem uspgrlimlem3
StepHypRef Expression
1 sseq1 4021 . . 3 (𝑥 = 𝑒 → (𝑥𝑁𝑒𝑁))
2 uspgrlim.k . . 3 𝐾 = {𝑥𝐼𝑥𝑁}
31, 2elrab2 3698 . 2 (𝑒𝐾 ↔ (𝑒𝐼𝑒𝑁))
4 eqid 2733 . . . . . . . 8 (iEdg‘𝐺) = (iEdg‘𝐺)
54uspgrf1oedg 29186 . . . . . . 7 (𝐺 ∈ USPGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→(Edg‘𝐺))
6 f1ocnv 6855 . . . . . . 7 ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→(Edg‘𝐺) → (iEdg‘𝐺):(Edg‘𝐺)–1-1-onto→dom (iEdg‘𝐺))
7 f1of 6843 . . . . . . 7 ((iEdg‘𝐺):(Edg‘𝐺)–1-1-onto→dom (iEdg‘𝐺) → (iEdg‘𝐺):(Edg‘𝐺)⟶dom (iEdg‘𝐺))
85, 6, 73syl 18 . . . . . 6 (𝐺 ∈ USPGraph → (iEdg‘𝐺):(Edg‘𝐺)⟶dom (iEdg‘𝐺))
983ad2ant1 1131 . . . . 5 ((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅 ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖))) → (iEdg‘𝐺):(Edg‘𝐺)⟶dom (iEdg‘𝐺))
10 uspgrlim.i . . . . . . . 8 𝐼 = (Edg‘𝐺)
1110eleq2i 2829 . . . . . . 7 (𝑒𝐼𝑒 ∈ (Edg‘𝐺))
1211biimpi 216 . . . . . 6 (𝑒𝐼𝑒 ∈ (Edg‘𝐺))
1312adantr 480 . . . . 5 ((𝑒𝐼𝑒𝑁) → 𝑒 ∈ (Edg‘𝐺))
14 fvco3 7002 . . . . 5 (((iEdg‘𝐺):(Edg‘𝐺)⟶dom (iEdg‘𝐺) ∧ 𝑒 ∈ (Edg‘𝐺)) → ((((iEdg‘𝐻) ∘ ) ∘ (iEdg‘𝐺))‘𝑒) = (((iEdg‘𝐻) ∘ )‘((iEdg‘𝐺)‘𝑒)))
159, 13, 14syl2an 595 . . . 4 (((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅 ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖))) ∧ (𝑒𝐼𝑒𝑁)) → ((((iEdg‘𝐻) ∘ ) ∘ (iEdg‘𝐺))‘𝑒) = (((iEdg‘𝐻) ∘ )‘((iEdg‘𝐺)‘𝑒)))
16 f1ocnvdm 7298 . . . . . . . . . . . . . 14 (((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→(Edg‘𝐺) ∧ 𝑒 ∈ (Edg‘𝐺)) → ((iEdg‘𝐺)‘𝑒) ∈ dom (iEdg‘𝐺))
175, 13, 16syl2an 595 . . . . . . . . . . . . 13 ((𝐺 ∈ USPGraph ∧ (𝑒𝐼𝑒𝑁)) → ((iEdg‘𝐺)‘𝑒) ∈ dom (iEdg‘𝐺))
18 f1ocnvfv2 7290 . . . . . . . . . . . . . . 15 (((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→(Edg‘𝐺) ∧ 𝑒 ∈ (Edg‘𝐺)) → ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒)) = 𝑒)
195, 13, 18syl2an 595 . . . . . . . . . . . . . 14 ((𝐺 ∈ USPGraph ∧ (𝑒𝐼𝑒𝑁)) → ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒)) = 𝑒)
20 simprr 772 . . . . . . . . . . . . . 14 ((𝐺 ∈ USPGraph ∧ (𝑒𝐼𝑒𝑁)) → 𝑒𝑁)
2119, 20eqsstrd 4034 . . . . . . . . . . . . 13 ((𝐺 ∈ USPGraph ∧ (𝑒𝐼𝑒𝑁)) → ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒)) ⊆ 𝑁)
2217, 21jca 511 . . . . . . . . . . . 12 ((𝐺 ∈ USPGraph ∧ (𝑒𝐼𝑒𝑁)) → (((iEdg‘𝐺)‘𝑒) ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒)) ⊆ 𝑁))
2322adantlr 714 . . . . . . . . . . 11 (((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅) ∧ (𝑒𝐼𝑒𝑁)) → (((iEdg‘𝐺)‘𝑒) ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒)) ⊆ 𝑁))
24 fveq2 6901 . . . . . . . . . . . . 13 (𝑥 = ((iEdg‘𝐺)‘𝑒) → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒)))
2524sseq1d 4027 . . . . . . . . . . . 12 (𝑥 = ((iEdg‘𝐺)‘𝑒) → (((iEdg‘𝐺)‘𝑥) ⊆ 𝑁 ↔ ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒)) ⊆ 𝑁))
2625elrab 3695 . . . . . . . . . . 11 (((iEdg‘𝐺)‘𝑒) ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} ↔ (((iEdg‘𝐺)‘𝑒) ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒)) ⊆ 𝑁))
2723, 26sylibr 234 . . . . . . . . . 10 (((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅) ∧ (𝑒𝐼𝑒𝑁)) → ((iEdg‘𝐺)‘𝑒) ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁})
28 fveq2 6901 . . . . . . . . . . . . 13 (𝑖 = ((iEdg‘𝐺)‘𝑒) → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒)))
2928imaeq2d 6074 . . . . . . . . . . . 12 (𝑖 = ((iEdg‘𝐺)‘𝑒) → (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = (𝑓 “ ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒))))
30 2fveq3 6906 . . . . . . . . . . . 12 (𝑖 = ((iEdg‘𝐺)‘𝑒) → ((iEdg‘𝐻)‘(𝑖)) = ((iEdg‘𝐻)‘(‘((iEdg‘𝐺)‘𝑒))))
3129, 30eqeq12d 2749 . . . . . . . . . . 11 (𝑖 = ((iEdg‘𝐺)‘𝑒) → ((𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖)) ↔ (𝑓 “ ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒))) = ((iEdg‘𝐻)‘(‘((iEdg‘𝐺)‘𝑒)))))
3231rspcv 3618 . . . . . . . . . 10 (((iEdg‘𝐺)‘𝑒) ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖)) → (𝑓 “ ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒))) = ((iEdg‘𝐻)‘(‘((iEdg‘𝐺)‘𝑒)))))
3327, 32syl 17 . . . . . . . . 9 (((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅) ∧ (𝑒𝐼𝑒𝑁)) → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖)) → (𝑓 “ ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒))) = ((iEdg‘𝐻)‘(‘((iEdg‘𝐺)‘𝑒)))))
34 eqcom 2740 . . . . . . . . . 10 ((𝑓 “ ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒))) = ((iEdg‘𝐻)‘(‘((iEdg‘𝐺)‘𝑒))) ↔ ((iEdg‘𝐻)‘(‘((iEdg‘𝐺)‘𝑒))) = (𝑓 “ ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒))))
35 f1of 6843 . . . . . . . . . . . . . . 15 (:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶𝑅)
3635ad2antlr 726 . . . . . . . . . . . . . 14 (((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅) ∧ (𝑒𝐼𝑒𝑁)) → :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}⟶𝑅)
3736, 27fvco3d 7003 . . . . . . . . . . . . 13 (((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅) ∧ (𝑒𝐼𝑒𝑁)) → (((iEdg‘𝐻) ∘ )‘((iEdg‘𝐺)‘𝑒)) = ((iEdg‘𝐻)‘(‘((iEdg‘𝐺)‘𝑒))))
3837eqcomd 2739 . . . . . . . . . . . 12 (((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅) ∧ (𝑒𝐼𝑒𝑁)) → ((iEdg‘𝐻)‘(‘((iEdg‘𝐺)‘𝑒))) = (((iEdg‘𝐻) ∘ )‘((iEdg‘𝐺)‘𝑒)))
395adantr 480 . . . . . . . . . . . . . 14 ((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→(Edg‘𝐺))
4039, 13, 18syl2an 595 . . . . . . . . . . . . 13 (((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅) ∧ (𝑒𝐼𝑒𝑁)) → ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒)) = 𝑒)
4140imaeq2d 6074 . . . . . . . . . . . 12 (((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅) ∧ (𝑒𝐼𝑒𝑁)) → (𝑓 “ ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒))) = (𝑓𝑒))
4238, 41eqeq12d 2749 . . . . . . . . . . 11 (((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅) ∧ (𝑒𝐼𝑒𝑁)) → (((iEdg‘𝐻)‘(‘((iEdg‘𝐺)‘𝑒))) = (𝑓 “ ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒))) ↔ (((iEdg‘𝐻) ∘ )‘((iEdg‘𝐺)‘𝑒)) = (𝑓𝑒)))
4342biimpd 229 . . . . . . . . . 10 (((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅) ∧ (𝑒𝐼𝑒𝑁)) → (((iEdg‘𝐻)‘(‘((iEdg‘𝐺)‘𝑒))) = (𝑓 “ ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒))) → (((iEdg‘𝐻) ∘ )‘((iEdg‘𝐺)‘𝑒)) = (𝑓𝑒)))
4434, 43biimtrid 242 . . . . . . . . 9 (((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅) ∧ (𝑒𝐼𝑒𝑁)) → ((𝑓 “ ((iEdg‘𝐺)‘((iEdg‘𝐺)‘𝑒))) = ((iEdg‘𝐻)‘(‘((iEdg‘𝐺)‘𝑒))) → (((iEdg‘𝐻) ∘ )‘((iEdg‘𝐺)‘𝑒)) = (𝑓𝑒)))
4533, 44syld 47 . . . . . . . 8 (((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅) ∧ (𝑒𝐼𝑒𝑁)) → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖)) → (((iEdg‘𝐻) ∘ )‘((iEdg‘𝐺)‘𝑒)) = (𝑓𝑒)))
4645ex 412 . . . . . . 7 ((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅) → ((𝑒𝐼𝑒𝑁) → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖)) → (((iEdg‘𝐻) ∘ )‘((iEdg‘𝐺)‘𝑒)) = (𝑓𝑒))))
4746com23 86 . . . . . 6 ((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅) → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖)) → ((𝑒𝐼𝑒𝑁) → (((iEdg‘𝐻) ∘ )‘((iEdg‘𝐺)‘𝑒)) = (𝑓𝑒))))
4847ex 412 . . . . 5 (𝐺 ∈ USPGraph → (:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅 → (∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖)) → ((𝑒𝐼𝑒𝑁) → (((iEdg‘𝐻) ∘ )‘((iEdg‘𝐺)‘𝑒)) = (𝑓𝑒)))))
49483imp1 1345 . . . 4 (((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅 ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖))) ∧ (𝑒𝐼𝑒𝑁)) → (((iEdg‘𝐻) ∘ )‘((iEdg‘𝐺)‘𝑒)) = (𝑓𝑒))
5015, 49eqtr2d 2774 . . 3 (((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅 ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖))) ∧ (𝑒𝐼𝑒𝑁)) → (𝑓𝑒) = ((((iEdg‘𝐻) ∘ ) ∘ (iEdg‘𝐺))‘𝑒))
5150ex 412 . 2 ((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅 ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖))) → ((𝑒𝐼𝑒𝑁) → (𝑓𝑒) = ((((iEdg‘𝐻) ∘ ) ∘ (iEdg‘𝐺))‘𝑒)))
523, 51biimtrid 242 1 ((𝐺 ∈ USPGraph ∧ :{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto𝑅 ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑖))) → (𝑒𝐾 → (𝑓𝑒) = ((((iEdg‘𝐻) ∘ ) ∘ (iEdg‘𝐺))‘𝑒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1085   = wceq 1535  wcel 2104  wral 3057  {crab 3432  wss 3963  ccnv 5682  dom cdm 5683  cima 5686  ccom 5687  wf 6554  1-1-ontowf1o 6557  cfv 6558  (class class class)co 7425  Vtxcvtx 29009  iEdgciedg 29010  Edgcedg 29060  USPGraphcuspgr 29161   ClNeighbVtx cclnbgr 47693
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1963  ax-7 2003  ax-8 2106  ax-9 2114  ax-10 2137  ax-11 2153  ax-12 2173  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5430  ax-un 7747
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1087  df-tru 1538  df-fal 1548  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2536  df-eu 2565  df-clab 2711  df-cleq 2725  df-clel 2812  df-nfc 2888  df-ne 2937  df-ral 3058  df-rex 3067  df-rab 3433  df-v 3479  df-sbc 3792  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4915  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-iota 6510  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-edg 29061  df-uspgr 29163
This theorem is referenced by:  uspgrlim  47817
  Copyright terms: Public domain W3C validator