This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grlimgredgex

Description: Local isomorphisms between simple pseudographs map an edge onto an edge with an endpoint being the image of one of the endpoints of the first edge under the local isomorphism. (Contributed by AV, 28-Dec-2025)

Ref Expression
Hypotheses grlimgredgex.i ⊢ 𝐼 = ( Edg ‘ 𝐺 )
grlimgredgex.e ⊢ 𝐸 = ( Edg ‘ 𝐻 )
grlimgredgex.v ⊢ 𝑉 = ( Vtx ‘ 𝐻 )
grlimgredgex.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
grlimgredgex.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
grlimgredgex.p ⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ 𝐼 )
grlimgredgex.g ⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
grlimgredgex.h ⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
grlimgredgex.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) )
Assertion grlimgredgex ( 𝜑 → ∃ 𝑣 ∈ 𝑉 { ( 𝐹 ‘ 𝐴 ) , 𝑣 } ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 grlimgredgex.i ⊢ 𝐼 = ( Edg ‘ 𝐺 )
2 grlimgredgex.e ⊢ 𝐸 = ( Edg ‘ 𝐻 )
3 grlimgredgex.v ⊢ 𝑉 = ( Vtx ‘ 𝐻 )
4 grlimgredgex.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
5 grlimgredgex.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
6 grlimgredgex.p ⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ 𝐼 )
7 grlimgredgex.g ⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
8 grlimgredgex.h ⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
9 grlimgredgex.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) )
10 eqid ⊢ ( 𝐺 ClNeighbVtx 𝐴 ) = ( 𝐺 ClNeighbVtx 𝐴 )
11 eqid ⊢ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) }
12 eqid ⊢ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) )
13 eqid ⊢ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } = { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) }
14 10 1 11 12 2 13 grlimprclnbgrvtx ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ∧ ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ) ) )
15 7 8 9 4 5 6 14 syl213anc ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ∧ ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ) ) )
16 f1of ⊢ ( 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) → 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) ⟶ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) ⟶ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) )
18 uspgrupgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph )
19 7 18 syl ⊢ ( 𝜑 → 𝐺 ∈ UPGraph )
20 4 5 jca ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) )
21 19 20 6 3jca ⊢ ( 𝜑 → ( 𝐺 ∈ UPGraph ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) )
22 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
23 22 1 upgrpredgv ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) )
24 simpr ⊢ ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) → 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
25 21 23 24 3syl ⊢ ( 𝜑 → 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
26 simpl ⊢ ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
27 21 23 26 3syl ⊢ ( 𝜑 → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
28 22 1 predgclnbgrel ⊢ ( ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) → 𝐵 ∈ ( 𝐺 ClNeighbVtx 𝐴 ) )
29 25 27 6 28 syl3anc ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐺 ClNeighbVtx 𝐴 ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → 𝐵 ∈ ( 𝐺 ClNeighbVtx 𝐴 ) )
31 17 30 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝐵 ) ∈ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) )
32 3 clnbgrisvtx ⊢ ( ( 𝑓 ‘ 𝐵 ) ∈ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) → ( 𝑓 ‘ 𝐵 ) ∈ 𝑉 )
33 31 32 syl ⊢ ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝐵 ) ∈ 𝑉 )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) ∧ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ) → ( 𝑓 ‘ 𝐵 ) ∈ 𝑉 )
35 preq2 ⊢ ( 𝑣 = ( 𝑓 ‘ 𝐵 ) → { ( 𝐹 ‘ 𝐴 ) , 𝑣 } = { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } )
36 35 eleq1d ⊢ ( 𝑣 = ( 𝑓 ‘ 𝐵 ) → ( { ( 𝐹 ‘ 𝐴 ) , 𝑣 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐸 ) )
37 36 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) ∧ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ) ∧ 𝑣 = ( 𝑓 ‘ 𝐵 ) ) → ( { ( 𝐹 ‘ 𝐴 ) , 𝑣 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐸 ) )
38 sseq1 ⊢ ( 𝑥 = { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } → ( 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ↔ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) )
39 38 elrab ⊢ ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ↔ ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) )
40 39 simplbi ⊢ ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } → { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐸 )
41 40 adantl ⊢ ( ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) ∧ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ) → { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐸 )
42 34 37 41 rspcedvd ⊢ ( ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) ∧ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ) → ∃ 𝑣 ∈ 𝑉 { ( 𝐹 ‘ 𝐴 ) , 𝑣 } ∈ 𝐸 )
43 42 ex ⊢ ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } → ∃ 𝑣 ∈ 𝑉 { ( 𝐹 ‘ 𝐴 ) , 𝑣 } ∈ 𝐸 ) )
44 22 clnbgrvtxel ⊢ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) → 𝐴 ∈ ( 𝐺 ClNeighbVtx 𝐴 ) )
45 27 44 syl ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 ClNeighbVtx 𝐴 ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → 𝐴 ∈ ( 𝐺 ClNeighbVtx 𝐴 ) )
47 17 46 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝐴 ) ∈ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) )
48 3 clnbgrisvtx ⊢ ( ( 𝑓 ‘ 𝐴 ) ∈ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) → ( 𝑓 ‘ 𝐴 ) ∈ 𝑉 )
49 47 48 syl ⊢ ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝐴 ) ∈ 𝑉 )
50 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) ∧ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ) → ( 𝑓 ‘ 𝐴 ) ∈ 𝑉 )
51 preq2 ⊢ ( 𝑣 = ( 𝑓 ‘ 𝐴 ) → { ( 𝐹 ‘ 𝐴 ) , 𝑣 } = { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } )
52 51 eleq1d ⊢ ( 𝑣 = ( 𝑓 ‘ 𝐴 ) → ( { ( 𝐹 ‘ 𝐴 ) , 𝑣 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐸 ) )
53 52 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) ∧ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ) ∧ 𝑣 = ( 𝑓 ‘ 𝐴 ) ) → ( { ( 𝐹 ‘ 𝐴 ) , 𝑣 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐸 ) )
54 sseq1 ⊢ ( 𝑥 = { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } → ( 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ↔ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) )
55 54 elrab ⊢ ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ↔ ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐸 ∧ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) )
56 55 simplbi ⊢ ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } → { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐸 )
57 56 adantl ⊢ ( ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) ∧ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ) → { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐸 )
58 50 53 57 rspcedvd ⊢ ( ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) ∧ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ) → ∃ 𝑣 ∈ 𝑉 { ( 𝐹 ‘ 𝐴 ) , 𝑣 } ∈ 𝐸 )
59 58 ex ⊢ ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } → ∃ 𝑣 ∈ 𝑉 { ( 𝐹 ‘ 𝐴 ) , 𝑣 } ∈ 𝐸 ) )
60 43 59 jaod ⊢ ( ( 𝜑 ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → ( ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ) → ∃ 𝑣 ∈ 𝑉 { ( 𝐹 ‘ 𝐴 ) , 𝑣 } ∈ 𝐸 ) )
61 60 expimpd ⊢ ( 𝜑 → ( ( 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ∧ ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ) ) → ∃ 𝑣 ∈ 𝑉 { ( 𝐹 ‘ 𝐴 ) , 𝑣 } ∈ 𝐸 ) )
62 61 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ∧ ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ { 𝑥 ∈ 𝐸 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ) ) → ∃ 𝑣 ∈ 𝑉 { ( 𝐹 ‘ 𝐴 ) , 𝑣 } ∈ 𝐸 ) )
63 15 62 mpd ⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑉 { ( 𝐹 ‘ 𝐴 ) , 𝑣 } ∈ 𝐸 )