Metamath Proof Explorer

Theorem uhgr2edg

Description: If a vertex is adjacent to two different vertices in a hypergraph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 11-Feb-2021)

Ref Expression
Hypotheses usgrf1oedg.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
usgrf1oedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
uhgr2edg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion uhgr2edg ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 usgrf1oedg.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 usgrf1oedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 uhgr2edg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
4 simp1l ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → 𝐺 ∈ UHGraph )
5 simp1r ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → 𝐴 ≠ 𝐵 )
6 simp23 ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → 𝑁 ∈ 𝑉 )
7 simp21 ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → 𝐴 ∈ 𝑉 )
8 3simpc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )
9 8 3ad2ant2 ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )
10 6 7 9 jca31 ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
11 4 5 10 jca31 ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) )
12 simp3 ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) )
13 2 a1i ⊢ ( 𝐺 ∈ UHGraph → 𝐸 = ( Edg ‘ 𝐺 ) )
14 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
15 14 a1i ⊢ ( 𝐺 ∈ UHGraph → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
16 1 eqcomi ⊢ ( iEdg ‘ 𝐺 ) = 𝐼
17 16 a1i ⊢ ( 𝐺 ∈ UHGraph → ( iEdg ‘ 𝐺 ) = 𝐼 )
18 17 rneqd ⊢ ( 𝐺 ∈ UHGraph → ran ( iEdg ‘ 𝐺 ) = ran 𝐼 )
19 13 15 18 3eqtrd ⊢ ( 𝐺 ∈ UHGraph → 𝐸 = ran 𝐼 )
20 19 eleq2d ⊢ ( 𝐺 ∈ UHGraph → ( { 𝑁 , 𝐴 } ∈ 𝐸 ↔ { 𝑁 , 𝐴 } ∈ ran 𝐼 ) )
21 19 eleq2d ⊢ ( 𝐺 ∈ UHGraph → ( { 𝐵 , 𝑁 } ∈ 𝐸 ↔ { 𝐵 , 𝑁 } ∈ ran 𝐼 ) )
22 20 21 anbi12d ⊢ ( 𝐺 ∈ UHGraph → ( ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ↔ ( { 𝑁 , 𝐴 } ∈ ran 𝐼 ∧ { 𝐵 , 𝑁 } ∈ ran 𝐼 ) ) )
23 1 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun 𝐼 )
24 23 funfnd ⊢ ( 𝐺 ∈ UHGraph → 𝐼 Fn dom 𝐼 )
25 fvelrnb ⊢ ( 𝐼 Fn dom 𝐼 → ( { 𝑁 , 𝐴 } ∈ ran 𝐼 ↔ ∃ 𝑥 ∈ dom 𝐼 ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ) )
26 fvelrnb ⊢ ( 𝐼 Fn dom 𝐼 → ( { 𝐵 , 𝑁 } ∈ ran 𝐼 ↔ ∃ 𝑦 ∈ dom 𝐼 ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) )
27 25 26 anbi12d ⊢ ( 𝐼 Fn dom 𝐼 → ( ( { 𝑁 , 𝐴 } ∈ ran 𝐼 ∧ { 𝐵 , 𝑁 } ∈ ran 𝐼 ) ↔ ( ∃ 𝑥 ∈ dom 𝐼 ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ∃ 𝑦 ∈ dom 𝐼 ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) ) )
28 24 27 syl ⊢ ( 𝐺 ∈ UHGraph → ( ( { 𝑁 , 𝐴 } ∈ ran 𝐼 ∧ { 𝐵 , 𝑁 } ∈ ran 𝐼 ) ↔ ( ∃ 𝑥 ∈ dom 𝐼 ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ∃ 𝑦 ∈ dom 𝐼 ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) ) )
29 22 28 bitrd ⊢ ( 𝐺 ∈ UHGraph → ( ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ↔ ( ∃ 𝑥 ∈ dom 𝐼 ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ∃ 𝑦 ∈ dom 𝐼 ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) ) )
30 29 ad2antrr ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) → ( ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ↔ ( ∃ 𝑥 ∈ dom 𝐼 ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ∃ 𝑦 ∈ dom 𝐼 ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) ) )
31 reeanv ⊢ ( ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) ↔ ( ∃ 𝑥 ∈ dom 𝐼 ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ∃ 𝑦 ∈ dom 𝐼 ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) )
32 fveqeq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ↔ ( 𝐼 ‘ 𝑦 ) = { 𝑁 , 𝐴 } ) )
33 32 anbi1d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) ↔ ( ( 𝐼 ‘ 𝑦 ) = { 𝑁 , 𝐴 } ∧ ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) ) )
34 eqtr2 ⊢ ( ( ( 𝐼 ‘ 𝑦 ) = { 𝑁 , 𝐴 } ∧ ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) → { 𝑁 , 𝐴 } = { 𝐵 , 𝑁 } )
35 prcom ⊢ { 𝐵 , 𝑁 } = { 𝑁 , 𝐵 }
36 35 eqeq2i ⊢ ( { 𝑁 , 𝐴 } = { 𝐵 , 𝑁 } ↔ { 𝑁 , 𝐴 } = { 𝑁 , 𝐵 } )
37 preq12bg ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑁 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( { 𝑁 , 𝐴 } = { 𝑁 , 𝐵 } ↔ ( ( 𝑁 = 𝑁 ∧ 𝐴 = 𝐵 ) ∨ ( 𝑁 = 𝐵 ∧ 𝐴 = 𝑁 ) ) ) )
38 37 ancom2s ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) → ( { 𝑁 , 𝐴 } = { 𝑁 , 𝐵 } ↔ ( ( 𝑁 = 𝑁 ∧ 𝐴 = 𝐵 ) ∨ ( 𝑁 = 𝐵 ∧ 𝐴 = 𝑁 ) ) ) )
39 eqneqall ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦 ) )
40 39 adantl ⊢ ( ( 𝑁 = 𝑁 ∧ 𝐴 = 𝐵 ) → ( 𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦 ) )
41 eqtr ⊢ ( ( 𝐴 = 𝑁 ∧ 𝑁 = 𝐵 ) → 𝐴 = 𝐵 )
42 41 ancoms ⊢ ( ( 𝑁 = 𝐵 ∧ 𝐴 = 𝑁 ) → 𝐴 = 𝐵 )
43 42 39 syl ⊢ ( ( 𝑁 = 𝐵 ∧ 𝐴 = 𝑁 ) → ( 𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦 ) )
44 40 43 jaoi ⊢ ( ( ( 𝑁 = 𝑁 ∧ 𝐴 = 𝐵 ) ∨ ( 𝑁 = 𝐵 ∧ 𝐴 = 𝑁 ) ) → ( 𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦 ) )
45 44 adantld ⊢ ( ( ( 𝑁 = 𝑁 ∧ 𝐴 = 𝐵 ) ∨ ( 𝑁 = 𝐵 ∧ 𝐴 = 𝑁 ) ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) → 𝑥 ≠ 𝑦 ) )
46 38 45 biimtrdi ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) → ( { 𝑁 , 𝐴 } = { 𝑁 , 𝐵 } → ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) → 𝑥 ≠ 𝑦 ) ) )
47 46 com3l ⊢ ( { 𝑁 , 𝐴 } = { 𝑁 , 𝐵 } → ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) → 𝑥 ≠ 𝑦 ) ) )
48 47 impd ⊢ ( { 𝑁 , 𝐴 } = { 𝑁 , 𝐵 } → ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) → 𝑥 ≠ 𝑦 ) )
49 36 48 sylbi ⊢ ( { 𝑁 , 𝐴 } = { 𝐵 , 𝑁 } → ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) → 𝑥 ≠ 𝑦 ) )
50 34 49 syl ⊢ ( ( ( 𝐼 ‘ 𝑦 ) = { 𝑁 , 𝐴 } ∧ ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) → ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) → 𝑥 ≠ 𝑦 ) )
51 33 50 biimtrdi ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) → ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) → 𝑥 ≠ 𝑦 ) ) )
52 51 impcomd ⊢ ( 𝑥 = 𝑦 → ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) ∧ ( ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) ) → 𝑥 ≠ 𝑦 ) )
53 ax-1 ⊢ ( 𝑥 ≠ 𝑦 → ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) ∧ ( ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) ) → 𝑥 ≠ 𝑦 ) )
54 52 53 pm2.61ine ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) ∧ ( ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) ) → 𝑥 ≠ 𝑦 )
55 prid1g ⊢ ( 𝑁 ∈ 𝑉 → 𝑁 ∈ { 𝑁 , 𝐴 } )
56 55 ad2antrr ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) → 𝑁 ∈ { 𝑁 , 𝐴 } )
57 56 adantl ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) → 𝑁 ∈ { 𝑁 , 𝐴 } )
58 eleq2 ⊢ ( ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } → ( 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ↔ 𝑁 ∈ { 𝑁 , 𝐴 } ) )
59 57 58 imbitrrid ⊢ ( ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } → ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) → 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ) )
60 59 adantr ⊢ ( ( ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) → ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) → 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ) )
61 60 impcom ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) ∧ ( ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) ) → 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) )
62 prid2g ⊢ ( 𝑁 ∈ 𝑉 → 𝑁 ∈ { 𝐵 , 𝑁 } )
63 62 ad2antrr ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) → 𝑁 ∈ { 𝐵 , 𝑁 } )
64 63 adantl ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) → 𝑁 ∈ { 𝐵 , 𝑁 } )
65 eleq2 ⊢ ( ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } → ( 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ↔ 𝑁 ∈ { 𝐵 , 𝑁 } ) )
66 64 65 imbitrrid ⊢ ( ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } → ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) → 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) )
67 66 adantl ⊢ ( ( ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) → ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) → 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) )
68 67 impcom ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) ∧ ( ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) ) → 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) )
69 54 61 68 3jca ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) ∧ ( ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) ) → ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) )
70 69 ex ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) → ( ( ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) → ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ) )
71 70 reximdv ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) → ( ∃ 𝑦 ∈ dom 𝐼 ( ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) → ∃ 𝑦 ∈ dom 𝐼 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ) )
72 71 reximdv ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) → ( ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) → ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ) )
73 31 72 biimtrrid ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) → ( ( ∃ 𝑥 ∈ dom 𝐼 ( 𝐼 ‘ 𝑥 ) = { 𝑁 , 𝐴 } ∧ ∃ 𝑦 ∈ dom 𝐼 ( 𝐼 ‘ 𝑦 ) = { 𝐵 , 𝑁 } ) → ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ) )
74 30 73 sylbid ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) ) → ( ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) → ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) ) )
75 11 12 74 sylc ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ dom 𝐼 ∃ 𝑦 ∈ dom 𝐼 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑥 ) ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑦 ) ) )