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

Theorem clnbgrgrimlem 47839
Description: Lemma for clnbgrgrim 47840: For two isomorphic hypergraphs, if there is an edge connecting the image of a vertex of the first graph with a vertex of the second graph, the vertex of the second graph is the image of a neighbor of the vertex of the first graph. (Contributed by AV, 2-Jun-2025.)
Hypotheses
Ref Expression
clnbgrgrim.v 𝑉 = (Vtx‘𝐺)
clnbgrgrimlem.w 𝑊 = (Vtx‘𝐻)
clnbgrgrimlem.e 𝐸 = (Edg‘𝐻)
Assertion
Ref Expression
clnbgrgrimlem (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋𝑉𝑌𝑊)) → ((𝐾𝐸 ∧ {(𝐹𝑋), 𝑌} ⊆ 𝐾) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹𝑛) = 𝑌))
Distinct variable groups:   𝑛,𝐹   𝑛,𝐺   𝑛,𝐻   𝑛,𝑉   𝑛,𝑋   𝑛,𝐸   𝑛,𝐾   𝑛,𝑊   𝑛,𝑌

Proof of Theorem clnbgrgrimlem
Dummy variables 𝑒 𝑖 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 clnbgrgrimlem.e . . . . . . . . . . . . . . 15 𝐸 = (Edg‘𝐻)
21eleq2i 2831 . . . . . . . . . . . . . 14 (𝐾𝐸𝐾 ∈ (Edg‘𝐻))
3 eqid 2735 . . . . . . . . . . . . . . 15 (iEdg‘𝐻) = (iEdg‘𝐻)
43uhgredgiedgb 29158 . . . . . . . . . . . . . 14 (𝐻 ∈ UHGraph → (𝐾 ∈ (Edg‘𝐻) ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
52, 4bitrid 283 . . . . . . . . . . . . 13 (𝐻 ∈ UHGraph → (𝐾𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
65adantl 481 . . . . . . . . . . . 12 ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝐾𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
763ad2ant3 1134 . . . . . . . . . . 11 ((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → (𝐾𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
87adantr 480 . . . . . . . . . 10 (((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) → (𝐾𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘)))
9 sseq2 4022 . . . . . . . . . . . . . 14 (𝐾 = ((iEdg‘𝐻)‘𝑘) → ({(𝐹𝑋), 𝑌} ⊆ 𝐾 ↔ {(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)))
109adantl 481 . . . . . . . . . . . . 13 (((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝐾 = ((iEdg‘𝐻)‘𝑘)) → ({(𝐹𝑋), 𝑌} ⊆ 𝐾 ↔ {(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)))
11 simp1 1135 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → 𝐹:𝑉1-1-onto𝑊)
12 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝑋𝑉𝑌𝑊) → 𝑌𝑊)
1311, 12anim12i 613 . . . . . . . . . . . . . . . . . . 19 (((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) → (𝐹:𝑉1-1-onto𝑊𝑌𝑊))
14 f1ocnvdm 7305 . . . . . . . . . . . . . . . . . . 19 ((𝐹:𝑉1-1-onto𝑊𝑌𝑊) → (𝐹𝑌) ∈ 𝑉)
1513, 14syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) → (𝐹𝑌) ∈ 𝑉)
16 simpl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝑉𝑌𝑊) → 𝑋𝑉)
1716adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) → 𝑋𝑉)
1815, 17jca 511 . . . . . . . . . . . . . . . . 17 (((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) → ((𝐹𝑌) ∈ 𝑉𝑋𝑉))
1918ad2antrr 726 . . . . . . . . . . . . . . . 16 (((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ((𝐹𝑌) ∈ 𝑉𝑋𝑉))
20 eqid 2735 . . . . . . . . . . . . . . . . . . . . . . . . 25 (iEdg‘𝐺) = (iEdg‘𝐺)
2120uhgrfun 29098 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐺 ∈ UHGraph → Fun (iEdg‘𝐺))
2221adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → Fun (iEdg‘𝐺))
23223ad2ant3 1134 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → Fun (iEdg‘𝐺))
2423ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → Fun (iEdg‘𝐺))
25 simpl2l 1225 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) → 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))
26 f1ocnvdm 7305 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝑗𝑘) ∈ dom (iEdg‘𝐺))
2725, 26sylan 580 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝑗𝑘) ∈ dom (iEdg‘𝐺))
2824, 27jca 511 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (Fun (iEdg‘𝐺) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)))
2920iedgedg 29082 . . . . . . . . . . . . . . . . . . . 20 ((Fun (iEdg‘𝐺) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(𝑗𝑘)) ∈ (Edg‘𝐺))
3028, 29syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐺)‘(𝑗𝑘)) ∈ (Edg‘𝐺))
3130adantr 480 . . . . . . . . . . . . . . . . . 18 (((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ((iEdg‘𝐺)‘(𝑗𝑘)) ∈ (Edg‘𝐺))
32 sseq2 4022 . . . . . . . . . . . . . . . . . . 19 (𝑒 = ((iEdg‘𝐺)‘(𝑗𝑘)) → ({𝑋, (𝐹𝑌)} ⊆ 𝑒 ↔ {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘))))
3332adantl 481 . . . . . . . . . . . . . . . . . 18 ((((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) ∧ 𝑒 = ((iEdg‘𝐺)‘(𝑗𝑘))) → ({𝑋, (𝐹𝑌)} ⊆ 𝑒 ↔ {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘))))
34 2fveq3 6912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 = (𝑗𝑘) → ((iEdg‘𝐻)‘(𝑗𝑖)) = ((iEdg‘𝐻)‘(𝑗‘(𝑗𝑘))))
35 fveq2 6907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 = (𝑗𝑘) → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘(𝑗𝑘)))
3635imaeq2d 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 = (𝑗𝑘) → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))))
3734, 36eqeq12d 2751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 = (𝑗𝑘) → (((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘(𝑗𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))))
3837rspcv 3618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗𝑘) ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘(𝑗𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))))
3938adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘(𝑗𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))))
40 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))
41 simp1 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊)) → 𝑘 ∈ dom (iEdg‘𝐻))
4240, 41anim12i 613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) → (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)))
4342adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)))
44 f1ocnvfv2 7297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝑗‘(𝑗𝑘)) = 𝑘)
4543, 44syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → (𝑗‘(𝑗𝑘)) = 𝑘)
4645fveqeq2d 6915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐻)‘(𝑗‘(𝑗𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) ↔ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))))
47 sseq2 4022 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) → ({(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) ↔ {(𝐹𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))))
4847adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))) → ({(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) ↔ {(𝐹𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))))
49 f1ofn 6850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝐹:𝑉1-1-onto𝑊𝐹 Fn 𝑉)
5049ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) → 𝐹 Fn 𝑉)
51 simpr3l 1233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) → 𝑋𝑉)
52 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝐹:𝑉1-1-onto𝑊)
53123ad2ant3 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊)) → 𝑌𝑊)
5452, 53anim12i 613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) → (𝐹:𝑉1-1-onto𝑊𝑌𝑊))
5554, 14syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) → (𝐹𝑌) ∈ 𝑉)
5650, 51, 553jca 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) → (𝐹 Fn 𝑉𝑋𝑉 ∧ (𝐹𝑌) ∈ 𝑉))
5756adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹 Fn 𝑉𝑋𝑉 ∧ (𝐹𝑌) ∈ 𝑉))
58 fnimapr 6992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐹 Fn 𝑉𝑋𝑉 ∧ (𝐹𝑌) ∈ 𝑉) → (𝐹 “ {𝑋, (𝐹𝑌)}) = {(𝐹𝑋), (𝐹‘(𝐹𝑌))})
5957, 58syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹 “ {𝑋, (𝐹𝑌)}) = {(𝐹𝑋), (𝐹‘(𝐹𝑌))})
6054adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹:𝑉1-1-onto𝑊𝑌𝑊))
61 f1ocnvfv2 7297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐹:𝑉1-1-onto𝑊𝑌𝑊) → (𝐹‘(𝐹𝑌)) = 𝑌)
6260, 61syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹‘(𝐹𝑌)) = 𝑌)
6362preq2d 4745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → {(𝐹𝑋), (𝐹‘(𝐹𝑌))} = {(𝐹𝑋), 𝑌})
6459, 63eqtr2d 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → {(𝐹𝑋), 𝑌} = (𝐹 “ {𝑋, (𝐹𝑌)}))
6564sseq1d 4027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → ({(𝐹𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) ↔ (𝐹 “ {𝑋, (𝐹𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))))
66 f1of1 6848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝐹:𝑉1-1-onto𝑊𝐹:𝑉1-1𝑊)
6766adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝐹:𝑉1-1𝑊)
6867ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → 𝐹:𝑉1-1𝑊)
6951, 55prssd 4827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) → {𝑋, (𝐹𝑌)} ⊆ 𝑉)
7069adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → {𝑋, (𝐹𝑌)} ⊆ 𝑉)
71 simpr2l 1231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) → 𝐺 ∈ UHGraph)
72 clnbgrgrim.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 𝑉 = (Vtx‘𝐺)
7372, 20uhgrss 29096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐺 ∈ UHGraph ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(𝑗𝑘)) ⊆ 𝑉)
7471, 73sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(𝑗𝑘)) ⊆ 𝑉)
75 f1imass 7284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐹:𝑉1-1𝑊 ∧ ({𝑋, (𝐹𝑌)} ⊆ 𝑉 ∧ ((iEdg‘𝐺)‘(𝑗𝑘)) ⊆ 𝑉)) → ((𝐹 “ {𝑋, (𝐹𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) ↔ {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘))))
7668, 70, 74, 75syl12anc 837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → ((𝐹 “ {𝑋, (𝐹𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) ↔ {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘))))
7776biimpd 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → ((𝐹 “ {𝑋, (𝐹𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) → {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘))))
7865, 77sylbid 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → ({(𝐹𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) → {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘))))
7978adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))) → ({(𝐹𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) → {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘))))
8048, 79sylbid 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))) → ({(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘))))
8180ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) → ({(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘)))))
8246, 81sylbid 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐻)‘(𝑗‘(𝑗𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) → ({(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘)))))
8339, 82syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ({(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘)))))
8483ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) → ((𝑗𝑘) ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ({(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘))))))
8584com23 86 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ (𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋𝑉𝑌𝑊))) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((𝑗𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘))))))
86853exp2 1353 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (𝑘 ∈ dom (iEdg‘𝐻) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋𝑉𝑌𝑊) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((𝑗𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘)))))))))
8786com25 99 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹:𝑉1-1-onto𝑊𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋𝑉𝑌𝑊) → (𝑘 ∈ dom (iEdg‘𝐻) → ((𝑗𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘)))))))))
8887expimpd 453 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:𝑉1-1-onto𝑊 → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋𝑉𝑌𝑊) → (𝑘 ∈ dom (iEdg‘𝐻) → ((𝑗𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘)))))))))
89883imp1 1346 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) → (𝑘 ∈ dom (iEdg‘𝐻) → ((𝑗𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘))))))
9089imp 406 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((𝑗𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘)))))
9127, 90mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ({(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘))))
9291imp 406 . . . . . . . . . . . . . . . . . 18 (((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → {𝑋, (𝐹𝑌)} ⊆ ((iEdg‘𝐺)‘(𝑗𝑘)))
9331, 33, 92rspcedvd 3624 . . . . . . . . . . . . . . . . 17 (((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ∃𝑒 ∈ (Edg‘𝐺){𝑋, (𝐹𝑌)} ⊆ 𝑒)
9493olcd 874 . . . . . . . . . . . . . . . 16 (((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ((𝐹𝑌) = 𝑋 ∨ ∃𝑒 ∈ (Edg‘𝐺){𝑋, (𝐹𝑌)} ⊆ 𝑒))
95 eqid 2735 . . . . . . . . . . . . . . . . 17 (Edg‘𝐺) = (Edg‘𝐺)
9672, 95clnbgrel 47753 . . . . . . . . . . . . . . . 16 ((𝐹𝑌) ∈ (𝐺 ClNeighbVtx 𝑋) ↔ (((𝐹𝑌) ∈ 𝑉𝑋𝑉) ∧ ((𝐹𝑌) = 𝑋 ∨ ∃𝑒 ∈ (Edg‘𝐺){𝑋, (𝐹𝑌)} ⊆ 𝑒)))
9719, 94, 96sylanbrc 583 . . . . . . . . . . . . . . 15 (((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → (𝐹𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))
9897ex 412 . . . . . . . . . . . . . 14 ((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ({(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → (𝐹𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))
9998adantr 480 . . . . . . . . . . . . 13 (((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝐾 = ((iEdg‘𝐻)‘𝑘)) → ({(𝐹𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → (𝐹𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))
10010, 99sylbid 240 . . . . . . . . . . . 12 (((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝐾 = ((iEdg‘𝐻)‘𝑘)) → ({(𝐹𝑋), 𝑌} ⊆ 𝐾 → (𝐹𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))
101100ex 412 . . . . . . . . . . 11 ((((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝐾 = ((iEdg‘𝐻)‘𝑘) → ({(𝐹𝑋), 𝑌} ⊆ 𝐾 → (𝐹𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))
102101rexlimdva 3153 . . . . . . . . . 10 (((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) → (∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘) → ({(𝐹𝑋), 𝑌} ⊆ 𝐾 → (𝐹𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))
1038, 102sylbid 240 . . . . . . . . 9 (((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) → (𝐾𝐸 → ({(𝐹𝑋), 𝑌} ⊆ 𝐾 → (𝐹𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))
104103impd 410 . . . . . . . 8 (((𝐹:𝑉1-1-onto𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋𝑉𝑌𝑊)) → ((𝐾𝐸 ∧ {(𝐹𝑋), 𝑌} ⊆ 𝐾) → (𝐹𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))
1051043exp1 1351 . . . . . . 7 (𝐹:𝑉1-1-onto𝑊 → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋𝑉𝑌𝑊) → ((𝐾𝐸 ∧ {(𝐹𝑋), 𝑌} ⊆ 𝐾) → (𝐹𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))))
106105exlimdv 1931 . . . . . 6 (𝐹:𝑉1-1-onto𝑊 → (∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋𝑉𝑌𝑊) → ((𝐾𝐸 ∧ {(𝐹𝑋), 𝑌} ⊆ 𝐾) → (𝐹𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))))
107106imp 406 . . . . 5 ((𝐹:𝑉1-1-onto𝑊 ∧ ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋𝑉𝑌𝑊) → ((𝐾𝐸 ∧ {(𝐹𝑋), 𝑌} ⊆ 𝐾) → (𝐹𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))))
108 clnbgrgrimlem.w . . . . . 6 𝑊 = (Vtx‘𝐻)
10972, 108, 20, 3grimprop 47807 . . . . 5 (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉1-1-onto𝑊 ∧ ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))))
110107, 109syl11 33 . . . 4 ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝐹 ∈ (𝐺 GraphIso 𝐻) → ((𝑋𝑉𝑌𝑊) → ((𝐾𝐸 ∧ {(𝐹𝑋), 𝑌} ⊆ 𝐾) → (𝐹𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))))
1111103imp1 1346 . . 3 ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋𝑉𝑌𝑊)) ∧ (𝐾𝐸 ∧ {(𝐹𝑋), 𝑌} ⊆ 𝐾)) → (𝐹𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))
112 fveqeq2 6916 . . . 4 (𝑛 = (𝐹𝑌) → ((𝐹𝑛) = 𝑌 ↔ (𝐹‘(𝐹𝑌)) = 𝑌))
113112adantl 481 . . 3 (((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋𝑉𝑌𝑊)) ∧ (𝐾𝐸 ∧ {(𝐹𝑋), 𝑌} ⊆ 𝐾)) ∧ 𝑛 = (𝐹𝑌)) → ((𝐹𝑛) = 𝑌 ↔ (𝐹‘(𝐹𝑌)) = 𝑌))
11472, 108grimf1o 47808 . . . . . . 7 (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:𝑉1-1-onto𝑊)
115114, 12anim12i 613 . . . . . 6 ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋𝑉𝑌𝑊)) → (𝐹:𝑉1-1-onto𝑊𝑌𝑊))
1161153adant1 1129 . . . . 5 (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋𝑉𝑌𝑊)) → (𝐹:𝑉1-1-onto𝑊𝑌𝑊))
117116adantr 480 . . . 4 ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋𝑉𝑌𝑊)) ∧ (𝐾𝐸 ∧ {(𝐹𝑋), 𝑌} ⊆ 𝐾)) → (𝐹:𝑉1-1-onto𝑊𝑌𝑊))
118117, 61syl 17 . . 3 ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋𝑉𝑌𝑊)) ∧ (𝐾𝐸 ∧ {(𝐹𝑋), 𝑌} ⊆ 𝐾)) → (𝐹‘(𝐹𝑌)) = 𝑌)
119111, 113, 118rspcedvd 3624 . 2 ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋𝑉𝑌𝑊)) ∧ (𝐾𝐸 ∧ {(𝐹𝑋), 𝑌} ⊆ 𝐾)) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹𝑛) = 𝑌)
120119ex 412 1 (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋𝑉𝑌𝑊)) → ((𝐾𝐸 ∧ {(𝐹𝑋), 𝑌} ⊆ 𝐾) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹𝑛) = 𝑌))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1537  wex 1776  wcel 2106  wral 3059  wrex 3068  wss 3963  {cpr 4633  ccnv 5688  dom cdm 5689  cima 5692  Fun wfun 6557   Fn wfn 6558  1-1wf1 6560  1-1-ontowf1o 6562  cfv 6563  (class class class)co 7431  Vtxcvtx 29028  iEdgciedg 29029  Edgcedg 29079  UHGraphcuhgr 29088   ClNeighbVtx cclnbgr 47743   GraphIso cgrim 47799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-map 8867  df-edg 29080  df-uhgr 29090  df-clnbgr 47744  df-grim 47802
This theorem is referenced by:  clnbgrgrim  47840
  Copyright terms: Public domain W3C validator