Theorem uhgr2edg 26998

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 1194	. . 3 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐺 ∈ UHGraph)
2		simp1r 1195	. . 3 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐴 ≠ 𝐵)
3		simp23 1205	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝑁 ∈ 𝑉)
4		simp21 1203	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐴 ∈ 𝑉)
5		3simpc 1147	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))
6	5	3ad2ant2 1131	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))
7	3, 4, 6	jca31 518	. . 3 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)))
8	1, 2, 7	jca31 518	. 2 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))))
9		simp3 1135	. 2 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸))
10		usgrf1oedg.e	. . . . . . . . 9 ⊢ 𝐸 = (Edg‘𝐺)
11	10	a1i 11	. . . . . . . 8 ⊢ (𝐺 ∈ UHGraph → 𝐸 = (Edg‘𝐺))
12		edgval 26842	. . . . . . . . 9 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
13	12	a1i 11	. . . . . . . 8 ⊢ (𝐺 ∈ UHGraph → (Edg‘𝐺) = ran (iEdg‘𝐺))
14		usgrf1oedg.i	. . . . . . . . . . 11 ⊢ 𝐼 = (iEdg‘𝐺)
15	14	eqcomi 2807	. . . . . . . . . 10 ⊢ (iEdg‘𝐺) = 𝐼
16	15	a1i 11	. . . . . . . . 9 ⊢ (𝐺 ∈ UHGraph → (iEdg‘𝐺) = 𝐼)
17	16	rneqd 5772	. . . . . . . 8 ⊢ (𝐺 ∈ UHGraph → ran (iEdg‘𝐺) = ran 𝐼)
18	11, 13, 17	3eqtrd 2837	. . . . . . 7 ⊢ (𝐺 ∈ UHGraph → 𝐸 = ran 𝐼)
19	18	eleq2d 2875	. . . . . 6 ⊢ (𝐺 ∈ UHGraph → ({𝑁, 𝐴} ∈ 𝐸 ↔ {𝑁, 𝐴} ∈ ran 𝐼))
20	18	eleq2d 2875	. . . . . 6 ⊢ (𝐺 ∈ UHGraph → ({𝐵, 𝑁} ∈ 𝐸 ↔ {𝐵, 𝑁} ∈ ran 𝐼))
21	19, 20	anbi12d 633	. . . . 5 ⊢ (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ ({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼)))
22	14	uhgrfun 26859	. . . . . . 7 ⊢ (𝐺 ∈ UHGraph → Fun 𝐼)
23	22	funfnd 6355	. . . . . 6 ⊢ (𝐺 ∈ UHGraph → 𝐼 Fn dom 𝐼)
24		fvelrnb 6701	. . . . . . 7 ⊢ (𝐼 Fn dom 𝐼 → ({𝑁, 𝐴} ∈ ran 𝐼 ↔ ∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴}))
25		fvelrnb 6701	. . . . . . 7 ⊢ (𝐼 Fn dom 𝐼 → ({𝐵, 𝑁} ∈ ran 𝐼 ↔ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁}))
26	24, 25	anbi12d 633	. . . . . 6 ⊢ (𝐼 Fn dom 𝐼 → (({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁})))
27	23, 26	syl 17	. . . . 5 ⊢ (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁})))
28	21, 27	bitrd 282	. . . 4 ⊢ (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁})))
29	28	ad2antrr 725	. . 3 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁})))
30		reeanv 3320	. . . 4 ⊢ (∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁}))
31		fveqeq2 6654	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝐼‘𝑥) = {𝑁, 𝐴} ↔ (𝐼‘𝑦) = {𝑁, 𝐴}))
32	31	anbi1d 632	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) ↔ ((𝐼‘𝑦) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})))
33		eqtr2 2819	. . . . . . . . . . . 12 ⊢ (((𝐼‘𝑦) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → {𝑁, 𝐴} = {𝐵, 𝑁})
34		prcom 4628	. . . . . . . . . . . . . 14 ⊢ {𝐵, 𝑁} = {𝑁, 𝐵}
35	34	eqeq2i 2811	. . . . . . . . . . . . 13 ⊢ ({𝑁, 𝐴} = {𝐵, 𝑁} ↔ {𝑁, 𝐴} = {𝑁, 𝐵})
36		preq12bg 4744	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑁 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} ↔ ((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) ∨ (𝑁 = 𝐵 ∧ 𝐴 = 𝑁))))
37	36	ancom2s 649	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} ↔ ((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) ∨ (𝑁 = 𝐵 ∧ 𝐴 = 𝑁))))
38		eqneqall 2998	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦))
39	38	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) → (𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦))
40		eqtr 2818	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 = 𝑁 ∧ 𝑁 = 𝐵) → 𝐴 = 𝐵)
41	40	ancoms 462	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 = 𝐵 ∧ 𝐴 = 𝑁) → 𝐴 = 𝐵)
42	41, 38	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 = 𝐵 ∧ 𝐴 = 𝑁) → (𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦))
43	39, 42	jaoi 854	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) ∨ (𝑁 = 𝐵 ∧ 𝐴 = 𝑁)) → (𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦))
44	43	adantld 494	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) ∨ (𝑁 = 𝐵 ∧ 𝐴 = 𝑁)) → ((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) → 𝑥 ≠ 𝑦))
45	37, 44	syl6bi 256	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} → ((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) → 𝑥 ≠ 𝑦)))
46	45	com3l 89	. . . . . . . . . . . . . 14 ⊢ ({𝑁, 𝐴} = {𝑁, 𝐵} → ((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) → (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → 𝑥 ≠ 𝑦)))
47	46	impd 414	. . . . . . . . . . . . 13 ⊢ ({𝑁, 𝐴} = {𝑁, 𝐵} → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑥 ≠ 𝑦))
48	35, 47	sylbi 220	. . . . . . . . . . . 12 ⊢ ({𝑁, 𝐴} = {𝐵, 𝑁} → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑥 ≠ 𝑦))
49	33, 48	syl 17	. . . . . . . . . . 11 ⊢ (((𝐼‘𝑦) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑥 ≠ 𝑦))
50	32, 49	syl6bi 256	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑥 ≠ 𝑦)))
51	50	impcomd 415	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑥 ≠ 𝑦))
52		ax-1 6	. . . . . . . . 9 ⊢ (𝑥 ≠ 𝑦 → ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑥 ≠ 𝑦))
53	51, 52	pm2.61ine 3070	. . . . . . . 8 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑥 ≠ 𝑦)
54		prid1g 4656	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ 𝑉 → 𝑁 ∈ {𝑁, 𝐴})
55	54	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → 𝑁 ∈ {𝑁, 𝐴})
56	55	adantl 485	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ {𝑁, 𝐴})
57		eleq2 2878	. . . . . . . . . . 11 ⊢ ((𝐼‘𝑥) = {𝑁, 𝐴} → (𝑁 ∈ (𝐼‘𝑥) ↔ 𝑁 ∈ {𝑁, 𝐴}))
58	56, 57	syl5ibr 249	. . . . . . . . . 10 ⊢ ((𝐼‘𝑥) = {𝑁, 𝐴} → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ (𝐼‘𝑥)))
59	58	adantr 484	. . . . . . . . 9 ⊢ (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ (𝐼‘𝑥)))
60	59	impcom 411	. . . . . . . 8 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑁 ∈ (𝐼‘𝑥))
61		prid2g 4657	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ 𝑉 → 𝑁 ∈ {𝐵, 𝑁})
62	61	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → 𝑁 ∈ {𝐵, 𝑁})
63	62	adantl 485	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ {𝐵, 𝑁})
64		eleq2 2878	. . . . . . . . . . 11 ⊢ ((𝐼‘𝑦) = {𝐵, 𝑁} → (𝑁 ∈ (𝐼‘𝑦) ↔ 𝑁 ∈ {𝐵, 𝑁}))
65	63, 64	syl5ibr 249	. . . . . . . . . 10 ⊢ ((𝐼‘𝑦) = {𝐵, 𝑁} → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ (𝐼‘𝑦)))
66	65	adantl 485	. . . . . . . . 9 ⊢ (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ (𝐼‘𝑦)))
67	66	impcom 411	. . . . . . . 8 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑁 ∈ (𝐼‘𝑦))
68	53, 60, 67	3jca 1125	. . . . . . 7 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → (𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦)))
69	68	ex 416	. . . . . 6 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))))
70	69	reximdv 3232	. . . . 5 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (∃𝑦 ∈ dom 𝐼((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → ∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))))
71	70	reximdv 3232	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))))
72	30, 71	syl5bir 246	. . 3 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → ((∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁}) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))))
73	29, 72	sylbid 243	. 2 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))))
74	8, 9, 73	sylc 65	1 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∃wrex 3107  {cpr 4527  dom cdm 5519  ran crn 5520   Fn wfn 6319  ‘cfv 6324  Vtxcvtx 26789  iEdgciedg 26790  Edgcedg 26840  UHGraphcuhgr 26849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fv 6332  df-edg 26841  df-uhgr 26851

This theorem is referenced by:  umgr2edg  26999