| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | clnbgrgrimlem.e | . . . . . . . . . . . . . . 15
⊢ 𝐸 = (Edg‘𝐻) | 
| 2 | 1 | eleq2i 2832 | . . . . . . . . . . . . . 14
⊢ (𝐾 ∈ 𝐸 ↔ 𝐾 ∈ (Edg‘𝐻)) | 
| 3 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(iEdg‘𝐻) =
(iEdg‘𝐻) | 
| 4 | 3 | uhgredgiedgb 29144 | . . . . . . . . . . . . . 14
⊢ (𝐻 ∈ UHGraph → (𝐾 ∈ (Edg‘𝐻) ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘))) | 
| 5 | 2, 4 | bitrid 283 | . . . . . . . . . . . . 13
⊢ (𝐻 ∈ UHGraph → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘))) | 
| 6 | 5 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘))) | 
| 7 | 6 | 3ad2ant3 1135 | . . . . . . . . . . 11
⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘))) | 
| 8 | 7 | adantr 480 | . . . . . . . . . 10
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐾 ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘))) | 
| 9 |  | sseq2 4009 | . . . . . . . . . . . . . 14
⊢ (𝐾 = ((iEdg‘𝐻)‘𝑘) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 ↔ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘))) | 
| 10 | 9 | adantl 481 | . . . . . . . . . . . . 13
⊢
(((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝐾 = ((iEdg‘𝐻)‘𝑘)) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 ↔ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘))) | 
| 11 |  | simp1 1136 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → 𝐹:𝑉–1-1-onto→𝑊) | 
| 12 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑌 ∈ 𝑊) | 
| 13 | 11, 12 | anim12i 613 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊)) | 
| 14 |  | f1ocnvdm 7306 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊) → (◡𝐹‘𝑌) ∈ 𝑉) | 
| 15 | 13, 14 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (◡𝐹‘𝑌) ∈ 𝑉) | 
| 16 |  | simpl 482 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → 𝑋 ∈ 𝑉) | 
| 17 | 16 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → 𝑋 ∈ 𝑉) | 
| 18 | 15, 17 | jca 511 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → ((◡𝐹‘𝑌) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) | 
| 19 | 18 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ((◡𝐹‘𝑌) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) | 
| 20 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) | 
| 21 | 20 | uhgrfun 29084 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) | 
| 22 | 21 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → Fun
(iEdg‘𝐺)) | 
| 23 | 22 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) → Fun
(iEdg‘𝐺)) | 
| 24 | 23 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → Fun (iEdg‘𝐺)) | 
| 25 |  | simpl2l 1226 | . . . . . . . . . . . . . . . . . . . . . 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 7306 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) | 
| 27 | 25, 26 | sylan 580 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) | 
| 28 | 24, 27 | jca 511 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (Fun (iEdg‘𝐺) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺))) | 
| 29 | 20 | iedgedg 29068 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((Fun
(iEdg‘𝐺) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(◡𝑗‘𝑘)) ∈ (Edg‘𝐺)) | 
| 30 | 28, 29 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐺)‘(◡𝑗‘𝑘)) ∈ (Edg‘𝐺)) | 
| 31 | 30 | adantr 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 4009 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = ((iEdg‘𝐺)‘(◡𝑗‘𝑘)) → ({𝑋, (◡𝐹‘𝑌)} ⊆ 𝑒 ↔ {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) | 
| 33 | 32 | adantl 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 6910 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑖 = (◡𝑗‘𝑘) → ((iEdg‘𝐻)‘(𝑗‘𝑖)) = ((iEdg‘𝐻)‘(𝑗‘(◡𝑗‘𝑘)))) | 
| 35 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑖 = (◡𝑗‘𝑘) → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) | 
| 36 | 35 | imaeq2d 6077 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑖 = (◡𝑗‘𝑘) → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) | 
| 37 | 34, 36 | eqeq12d 2752 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 = (◡𝑗‘𝑘) → (((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘(◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) | 
| 38 | 37 | rspcv 3617 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗‘(◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) | 
| 39 | 38 | adantl 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 1136 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → 𝑘 ∈ dom (iEdg‘𝐻)) | 
| 42 | 40, 41 | anim12i 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‘𝐻))) | 
| 43 | 42 | adantr 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 7298 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝑗‘(◡𝑗‘𝑘)) = 𝑘) | 
| 45 | 43, 44 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝑗‘(◡𝑗‘𝑘)) = 𝑘) | 
| 46 | 45 | fveqeq2d 6913 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐻)‘(𝑗‘(◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) ↔ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) | 
| 47 |  | sseq2 4009 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) ↔ {(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) | 
| 48 | 47 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) ↔ {(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) | 
| 49 |  | f1ofn 6848 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹 Fn 𝑉) | 
| 50 | 49 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → 𝐹 Fn 𝑉) | 
| 51 |  | simpr3l 1234 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 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→𝑊) | 
| 53 | 12 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑘 ∈ dom (iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → 𝑌 ∈ 𝑊) | 
| 54 | 52, 53 | anim12i 613 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊)) | 
| 55 | 54, 14 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → (◡𝐹‘𝑌) ∈ 𝑉) | 
| 56 | 50, 51, 55 | 3jca 1128 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → (𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ (◡𝐹‘𝑌) ∈ 𝑉)) | 
| 57 | 56 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ (◡𝐹‘𝑌) ∈ 𝑉)) | 
| 58 |  | fnimapr 6991 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ (◡𝐹‘𝑌) ∈ 𝑉) → (𝐹 “ {𝑋, (◡𝐹‘𝑌)}) = {(𝐹‘𝑋), (𝐹‘(◡𝐹‘𝑌))}) | 
| 59 | 57, 58 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹 “ {𝑋, (◡𝐹‘𝑌)}) = {(𝐹‘𝑋), (𝐹‘(◡𝐹‘𝑌))}) | 
| 60 | 54 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊)) | 
| 61 |  | f1ocnvfv2 7298 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊) → (𝐹‘(◡𝐹‘𝑌)) = 𝑌) | 
| 62 | 60, 61 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (𝐹‘(◡𝐹‘𝑌)) = 𝑌) | 
| 63 | 62 | preq2d 4739 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → {(𝐹‘𝑋), (𝐹‘(◡𝐹‘𝑌))} = {(𝐹‘𝑋), 𝑌}) | 
| 64 | 59, 63 | eqtr2d 2777 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → {(𝐹‘𝑋), 𝑌} = (𝐹 “ {𝑋, (◡𝐹‘𝑌)})) | 
| 65 | 64 | sseq1d 4014 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ({(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) ↔ (𝐹 “ {𝑋, (◡𝐹‘𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) | 
| 66 |  | f1of1 6846 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹:𝑉–1-1→𝑊) | 
| 67 | 66 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) →
𝐹:𝑉–1-1→𝑊) | 
| 68 | 67 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → 𝐹:𝑉–1-1→𝑊) | 
| 69 | 51, 55 | prssd 4821 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → {𝑋, (◡𝐹‘𝑌)} ⊆ 𝑉) | 
| 70 | 69 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → {𝑋, (◡𝐹‘𝑌)} ⊆ 𝑉) | 
| 71 |  | simpr2l 1232 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → 𝐺 ∈ UHGraph) | 
| 72 |  | clnbgrgrim.v | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ 𝑉 = (Vtx‘𝐺) | 
| 73 | 72, 20 | uhgrss 29082 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐺 ∈ UHGraph ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(◡𝑗‘𝑘)) ⊆ 𝑉) | 
| 74 | 71, 73 | sylan 580 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(◡𝑗‘𝑘)) ⊆ 𝑉) | 
| 75 |  | f1imass 7285 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝐹:𝑉–1-1→𝑊 ∧ ({𝑋, (◡𝐹‘𝑌)} ⊆ 𝑉 ∧ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)) ⊆ 𝑉)) → ((𝐹 “ {𝑋, (◡𝐹‘𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) ↔ {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) | 
| 76 | 68, 70, 74, 75 | syl12anc 836 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((𝐹 “ {𝑋, (◡𝐹‘𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) ↔ {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) | 
| 77 | 76 | biimpd 229 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ((𝐹 “ {𝑋, (◡𝐹‘𝑌)}) ⊆ (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) → {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) | 
| 78 | 65, 77 | sylbid 240 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → ({(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) → {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) | 
| 79 | 78 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) → ({(𝐹‘𝑋), 𝑌} ⊆ (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) → {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) | 
| 80 | 48, 79 | sylbid 240 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) | 
| 81 | 80 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) | 
| 82 | 46, 81 | sylbid 240 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐻)‘(𝑗‘(◡𝑗‘𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) | 
| 83 | 39, 82 | syld 47 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) ∧ (◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) | 
| 84 | 83 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → ((◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))))) | 
| 85 | 84 | com23 86 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) ∧
(𝑘 ∈ dom
(iEdg‘𝐻) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊))) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))))) | 
| 86 | 85 | 3exp2 1354 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) →
(𝑘 ∈ dom
(iEdg‘𝐻) →
((𝐺 ∈ UHGraph ∧
𝐻 ∈ UHGraph) →
((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))))))) | 
| 87 | 86 | com25 99 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻)) →
(∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (𝑘 ∈ dom (iEdg‘𝐻) → ((◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))))))) | 
| 88 | 87 | expimpd 453 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:𝑉–1-1-onto→𝑊 → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (𝑘 ∈ dom (iEdg‘𝐻) → ((◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))))))) | 
| 89 | 88 | 3imp1 1347 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝑘 ∈ dom (iEdg‘𝐻) → ((◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))))) | 
| 90 | 89 | imp 406 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((◡𝑗‘𝑘) ∈ dom (iEdg‘𝐺) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))))) | 
| 91 | 27, 90 | mpd 15 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘)))) | 
| 92 | 91 | imp 406 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → {𝑋, (◡𝐹‘𝑌)} ⊆ ((iEdg‘𝐺)‘(◡𝑗‘𝑘))) | 
| 93 | 31, 33, 92 | rspcedvd 3623 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ∃𝑒 ∈ (Edg‘𝐺){𝑋, (◡𝐹‘𝑌)} ⊆ 𝑒) | 
| 94 | 93 | olcd 874 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → ((◡𝐹‘𝑌) = 𝑋 ∨ ∃𝑒 ∈ (Edg‘𝐺){𝑋, (◡𝐹‘𝑌)} ⊆ 𝑒)) | 
| 95 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(Edg‘𝐺) =
(Edg‘𝐺) | 
| 96 | 72, 95 | clnbgrel 47820 | . . . . . . . . . . . . . . . 16
⊢ ((◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋) ↔ (((◡𝐹‘𝑌) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ ((◡𝐹‘𝑌) = 𝑋 ∨ ∃𝑒 ∈ (Edg‘𝐺){𝑋, (◡𝐹‘𝑌)} ⊆ 𝑒))) | 
| 97 | 19, 94, 96 | sylanbrc 583 | . . . . . . . . . . . . . . 15
⊢
(((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ {(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘)) → (◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)) | 
| 98 | 97 | ex 412 | . . . . . . . . . . . . . 14
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → (◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))) | 
| 99 | 98 | adantr 480 | . . . . . . . . . . . . 13
⊢
(((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝐾 = ((iEdg‘𝐻)‘𝑘)) → ({(𝐹‘𝑋), 𝑌} ⊆ ((iEdg‘𝐻)‘𝑘) → (◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))) | 
| 100 | 10, 99 | sylbid 240 | . . . . . . . . . . . 12
⊢
(((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝐾 = ((iEdg‘𝐻)‘𝑘)) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 → (◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))) | 
| 101 | 100 | ex 412 | . . . . . . . . . . 11
⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝐾 = ((iEdg‘𝐻)‘𝑘) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 → (◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))) | 
| 102 | 101 | rexlimdva 3154 | . . . . . . . . . 10
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (∃𝑘 ∈ dom (iEdg‘𝐻)𝐾 = ((iEdg‘𝐻)‘𝑘) → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 → (◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))) | 
| 103 | 8, 102 | sylbid 240 | . . . . . . . . 9
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐾 ∈ 𝐸 → ({(𝐹‘𝑋), 𝑌} ⊆ 𝐾 → (◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))) | 
| 104 | 103 | impd 410 | . . . . . . . 8
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ∧ (𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))) | 
| 105 | 104 | 3exp1 1352 | . . . . . . 7
⊢ (𝐹:𝑉–1-1-onto→𝑊 → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))))) | 
| 106 | 105 | exlimdv 1932 | . . . . . 6
⊢ (𝐹:𝑉–1-1-onto→𝑊 → (∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)))))) | 
| 107 | 106 | imp 406 | . . . . 5
⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))) | 
| 108 |  | clnbgrgrimlem.w | . . . . . 6
⊢ 𝑊 = (Vtx‘𝐻) | 
| 109 | 72, 108, 20, 3 | grimprop 47874 | . . . . 5
⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))))) | 
| 110 | 107, 109 | syl11 33 | . . . 4
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝐹 ∈ (𝐺 GraphIso 𝐻) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → (◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋))))) | 
| 111 | 110 | 3imp1 1347 | . . 3
⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) → (◡𝐹‘𝑌) ∈ (𝐺 ClNeighbVtx 𝑋)) | 
| 112 |  | fveqeq2 6914 | . . . 4
⊢ (𝑛 = (◡𝐹‘𝑌) → ((𝐹‘𝑛) = 𝑌 ↔ (𝐹‘(◡𝐹‘𝑌)) = 𝑌)) | 
| 113 | 112 | adantl 481 | . . 3
⊢
(((((𝐺 ∈
UHGraph ∧ 𝐻 ∈
UHGraph) ∧ 𝐹 ∈
(𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) ∧ 𝑛 = (◡𝐹‘𝑌)) → ((𝐹‘𝑛) = 𝑌 ↔ (𝐹‘(◡𝐹‘𝑌)) = 𝑌)) | 
| 114 | 72, 108 | grimf1o 47875 | . . . . . . 7
⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:𝑉–1-1-onto→𝑊) | 
| 115 | 114, 12 | anim12i 613 | . . . . . 6
⊢ ((𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊)) | 
| 116 | 115 | 3adant1 1130 | . . . . 5
⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊)) | 
| 117 | 116 | adantr 480 | . . . 4
⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ 𝑌 ∈ 𝑊)) | 
| 118 | 117, 61 | syl 17 | . . 3
⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) → (𝐹‘(◡𝐹‘𝑌)) = 𝑌) | 
| 119 | 111, 113,
118 | rspcedvd 3623 | . 2
⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) ∧ (𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾)) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑌) | 
| 120 | 119 | ex 412 | 1
⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑌)) |