Theorem uhgr2edg 27478

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.)

Hypotheses

Ref	Expression
usgrf1oedg.i	⊢ 𝐼 = (iEdg‘𝐺)
usgrf1oedg.e	⊢ 𝐸 = (Edg‘𝐺)
uhgr2edg.v	⊢ 𝑉 = (Vtx‘𝐺)

Assertion

Ref	Expression
uhgr2edg	⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦)))

Distinct variable groups:   𝑥,𝐺   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑦,𝐺   𝑥,𝐼,𝑦   𝑥,𝑁,𝑦   𝑥,𝑉,𝑦

Allowed substitution hints:   𝐸(𝑥,𝑦)

Proof of Theorem uhgr2edg

Step	Hyp	Ref	Expression
1		simp1l 1195	. . 3 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐺 ∈ UHGraph)
2		simp1r 1196	. . 3 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐴 ≠ 𝐵)
3		simp23 1206	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝑁 ∈ 𝑉)
4		simp21 1204	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐴 ∈ 𝑉)
5		3simpc 1148	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))
6	5	3ad2ant2 1132	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))
7	3, 4, 6	jca31 514	. . 3 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)))
8	1, 2, 7	jca31 514	. 2 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))))
9		simp3 1136	. 2 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸))
10		usgrf1oedg.e	. . . . . . . . 9 ⊢ 𝐸 = (Edg‘𝐺)
11	10	a1i 11	. . . . . . . 8 ⊢ (𝐺 ∈ UHGraph → 𝐸 = (Edg‘𝐺))
12		edgval 27322	. . . . . . . . 9 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
13	12	a1i 11	. . . . . . . 8 ⊢ (𝐺 ∈ UHGraph → (Edg‘𝐺) = ran (iEdg‘𝐺))
14		usgrf1oedg.i	. . . . . . . . . . 11 ⊢ 𝐼 = (iEdg‘𝐺)
15	14	eqcomi 2747	. . . . . . . . . 10 ⊢ (iEdg‘𝐺) = 𝐼
16	15	a1i 11	. . . . . . . . 9 ⊢ (𝐺 ∈ UHGraph → (iEdg‘𝐺) = 𝐼)
17	16	rneqd 5836	. . . . . . . 8 ⊢ (𝐺 ∈ UHGraph → ran (iEdg‘𝐺) = ran 𝐼)
18	11, 13, 17	3eqtrd 2782	. . . . . . 7 ⊢ (𝐺 ∈ UHGraph → 𝐸 = ran 𝐼)
19	18	eleq2d 2824	. . . . . 6 ⊢ (𝐺 ∈ UHGraph → ({𝑁, 𝐴} ∈ 𝐸 ↔ {𝑁, 𝐴} ∈ ran 𝐼))
20	18	eleq2d 2824	. . . . . 6 ⊢ (𝐺 ∈ UHGraph → ({𝐵, 𝑁} ∈ 𝐸 ↔ {𝐵, 𝑁} ∈ ran 𝐼))
21	19, 20	anbi12d 630	. . . . 5 ⊢ (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ ({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼)))
22	14	uhgrfun 27339	. . . . . . 7 ⊢ (𝐺 ∈ UHGraph → Fun 𝐼)
23	22	funfnd 6449	. . . . . 6 ⊢ (𝐺 ∈ UHGraph → 𝐼 Fn dom 𝐼)
24		fvelrnb 6812	. . . . . . 7 ⊢ (𝐼 Fn dom 𝐼 → ({𝑁, 𝐴} ∈ ran 𝐼 ↔ ∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴}))
25		fvelrnb 6812	. . . . . . 7 ⊢ (𝐼 Fn dom 𝐼 → ({𝐵, 𝑁} ∈ ran 𝐼 ↔ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁}))
26	24, 25	anbi12d 630	. . . . . 6 ⊢ (𝐼 Fn dom 𝐼 → (({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁})))
27	23, 26	syl 17	. . . . 5 ⊢ (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁})))
28	21, 27	bitrd 278	. . . 4 ⊢ (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁})))
29	28	ad2antrr 722	. . 3 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁})))
30		reeanv 3292	. . . 4 ⊢ (∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁}))
31		fveqeq2 6765	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝐼‘𝑥) = {𝑁, 𝐴} ↔ (𝐼‘𝑦) = {𝑁, 𝐴}))
32	31	anbi1d 629	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) ↔ ((𝐼‘𝑦) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})))
33		eqtr2 2762	. . . . . . . . . . . 12 ⊢ (((𝐼‘𝑦) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → {𝑁, 𝐴} = {𝐵, 𝑁})
34		prcom 4665	. . . . . . . . . . . . . 14 ⊢ {𝐵, 𝑁} = {𝑁, 𝐵}
35	34	eqeq2i 2751	. . . . . . . . . . . . 13 ⊢ ({𝑁, 𝐴} = {𝐵, 𝑁} ↔ {𝑁, 𝐴} = {𝑁, 𝐵})
36		preq12bg 4781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑁 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} ↔ ((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) ∨ (𝑁 = 𝐵 ∧ 𝐴 = 𝑁))))
37	36	ancom2s 646	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} ↔ ((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) ∨ (𝑁 = 𝐵 ∧ 𝐴 = 𝑁))))
38		eqneqall 2953	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦))
39	38	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) → (𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦))
40		eqtr 2761	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 = 𝑁 ∧ 𝑁 = 𝐵) → 𝐴 = 𝐵)
41	40	ancoms 458	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 = 𝐵 ∧ 𝐴 = 𝑁) → 𝐴 = 𝐵)
42	41, 38	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 = 𝐵 ∧ 𝐴 = 𝑁) → (𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦))
43	39, 42	jaoi 853	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) ∨ (𝑁 = 𝐵 ∧ 𝐴 = 𝑁)) → (𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦))
44	43	adantld 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) ∨ (𝑁 = 𝐵 ∧ 𝐴 = 𝑁)) → ((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) → 𝑥 ≠ 𝑦))
45	37, 44	syl6bi 252	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} → ((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) → 𝑥 ≠ 𝑦)))
46	45	com3l 89	. . . . . . . . . . . . . 14 ⊢ ({𝑁, 𝐴} = {𝑁, 𝐵} → ((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) → (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → 𝑥 ≠ 𝑦)))
47	46	impd 410	. . . . . . . . . . . . 13 ⊢ ({𝑁, 𝐴} = {𝑁, 𝐵} → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑥 ≠ 𝑦))
48	35, 47	sylbi 216	. . . . . . . . . . . 12 ⊢ ({𝑁, 𝐴} = {𝐵, 𝑁} → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑥 ≠ 𝑦))
49	33, 48	syl 17	. . . . . . . . . . 11 ⊢ (((𝐼‘𝑦) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑥 ≠ 𝑦))
50	32, 49	syl6bi 252	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑥 ≠ 𝑦)))
51	50	impcomd 411	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑥 ≠ 𝑦))
52		ax-1 6	. . . . . . . . 9 ⊢ (𝑥 ≠ 𝑦 → ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑥 ≠ 𝑦))
53	51, 52	pm2.61ine 3027	. . . . . . . 8 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑥 ≠ 𝑦)
54		prid1g 4693	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ 𝑉 → 𝑁 ∈ {𝑁, 𝐴})
55	54	ad2antrr 722	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → 𝑁 ∈ {𝑁, 𝐴})
56	55	adantl 481	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ {𝑁, 𝐴})
57		eleq2 2827	. . . . . . . . . . 11 ⊢ ((𝐼‘𝑥) = {𝑁, 𝐴} → (𝑁 ∈ (𝐼‘𝑥) ↔ 𝑁 ∈ {𝑁, 𝐴}))
58	56, 57	syl5ibr 245	. . . . . . . . . 10 ⊢ ((𝐼‘𝑥) = {𝑁, 𝐴} → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ (𝐼‘𝑥)))
59	58	adantr 480	. . . . . . . . 9 ⊢ (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ (𝐼‘𝑥)))
60	59	impcom 407	. . . . . . . 8 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑁 ∈ (𝐼‘𝑥))
61		prid2g 4694	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ 𝑉 → 𝑁 ∈ {𝐵, 𝑁})
62	61	ad2antrr 722	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → 𝑁 ∈ {𝐵, 𝑁})
63	62	adantl 481	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ {𝐵, 𝑁})
64		eleq2 2827	. . . . . . . . . . 11 ⊢ ((𝐼‘𝑦) = {𝐵, 𝑁} → (𝑁 ∈ (𝐼‘𝑦) ↔ 𝑁 ∈ {𝐵, 𝑁}))
65	63, 64	syl5ibr 245	. . . . . . . . . 10 ⊢ ((𝐼‘𝑦) = {𝐵, 𝑁} → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ (𝐼‘𝑦)))
66	65	adantl 481	. . . . . . . . 9 ⊢ (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ (𝐼‘𝑦)))
67	66	impcom 407	. . . . . . . 8 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑁 ∈ (𝐼‘𝑦))
68	53, 60, 67	3jca 1126	. . . . . . 7 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → (𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦)))
69	68	ex 412	. . . . . 6 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))))
70	69	reximdv 3201	. . . . 5 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (∃𝑦 ∈ dom 𝐼((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → ∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))))
71	70	reximdv 3201	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))))
72	30, 71	syl5bir 242	. . 3 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → ((∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁}) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))))
73	29, 72	sylbid 239	. 2 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))))
74	8, 9, 73	sylc 65	1 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  ∃wrex 3064  {cpr 4560  dom cdm 5580  ran crn 5581   Fn wfn 6413  ‘cfv 6418  Vtxcvtx 27269  iEdgciedg 27270  Edgcedg 27320  UHGraphcuhgr 27329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-edg 27321  df-uhgr 27331

This theorem is referenced by:  umgr2edg  27479