Theorem uhgr2edg 29595

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 1216	. . 3 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐺 ∈ UHGraph)
2		simp1r 1217	. . 3 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐴 ≠ 𝐵)
3		simp23 1227	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝑁 ∈ 𝑉)
4		simp21 1225	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐴 ∈ 𝑉)
5		3simpc 1168	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))
6	5	3ad2ant2 1152	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))
7	3, 4, 6	jca31 524	. . 3 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)))
8	1, 2, 7	jca31 524	. 2 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))))
9		simp3 1156	. 2 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸))
10		usgrf1oedg.e	. . . . . . . . 9 ⊢ 𝐸 = (Edg‘𝐺)
11	10	a1i 11	. . . . . . . 8 ⊢ (𝐺 ∈ UHGraph → 𝐸 = (Edg‘𝐺))
12		edgval 29436	. . . . . . . . 9 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
13	12	a1i 11	. . . . . . . 8 ⊢ (𝐺 ∈ UHGraph → (Edg‘𝐺) = ran (iEdg‘𝐺))
14		usgrf1oedg.i	. . . . . . . . . . 11 ⊢ 𝐼 = (iEdg‘𝐺)
15	14	eqcomi 2775	. . . . . . . . . 10 ⊢ (iEdg‘𝐺) = 𝐼
16	15	a1i 11	. . . . . . . . 9 ⊢ (𝐺 ∈ UHGraph → (iEdg‘𝐺) = 𝐼)
17	16	rneqd 5933	. . . . . . . 8 ⊢ (𝐺 ∈ UHGraph → ran (iEdg‘𝐺) = ran 𝐼)
18	11, 13, 17	3eqtrd 2805	. . . . . . 7 ⊢ (𝐺 ∈ UHGraph → 𝐸 = ran 𝐼)
19	18	eleq2d 2852	. . . . . 6 ⊢ (𝐺 ∈ UHGraph → ({𝑁, 𝐴} ∈ 𝐸 ↔ {𝑁, 𝐴} ∈ ran 𝐼))
20	18	eleq2d 2852	. . . . . 6 ⊢ (𝐺 ∈ UHGraph → ({𝐵, 𝑁} ∈ 𝐸 ↔ {𝐵, 𝑁} ∈ ran 𝐼))
21	19, 20	anbi12d 644	. . . . 5 ⊢ (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ ({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼)))
22	14	uhgrfun 29453	. . . . . . 7 ⊢ (𝐺 ∈ UHGraph → Fun 𝐼)
23	22	funfnd 6574	. . . . . 6 ⊢ (𝐺 ∈ UHGraph → 𝐼 Fn dom 𝐼)
24		fvelrnb 6948	. . . . . . 7 ⊢ (𝐼 Fn dom 𝐼 → ({𝑁, 𝐴} ∈ ran 𝐼 ↔ ∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴}))
25		fvelrnb 6948	. . . . . . 7 ⊢ (𝐼 Fn dom 𝐼 → ({𝐵, 𝑁} ∈ ran 𝐼 ↔ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁}))
26	24, 25	anbi12d 644	. . . . . 6 ⊢ (𝐼 Fn dom 𝐼 → (({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁})))
27	23, 26	syl 18	. . . . 5 ⊢ (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁})))
28	21, 27	bitrd 282	. . . 4 ⊢ (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁})))
29	28	ad2antrr 739	. . 3 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁})))
30		reeanv 3240	. . . 4 ⊢ (∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁}))
31		fveqeq2 6897	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝐼‘𝑥) = {𝑁, 𝐴} ↔ (𝐼‘𝑦) = {𝑁, 𝐴}))
32	31	anbi1d 643	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) ↔ ((𝐼‘𝑦) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})))
33		eqtr2 2787	. . . . . . . . . . . 12 ⊢ (((𝐼‘𝑦) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → {𝑁, 𝐴} = {𝐵, 𝑁})
34		prcom 4703	. . . . . . . . . . . . . 14 ⊢ {𝐵, 𝑁} = {𝑁, 𝐵}
35	34	eqeq2i 2779	. . . . . . . . . . . . 13 ⊢ ({𝑁, 𝐴} = {𝐵, 𝑁} ↔ {𝑁, 𝐴} = {𝑁, 𝐵})
36		preq12bg 4823	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑁 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} ↔ ((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) ∨ (𝑁 = 𝐵 ∧ 𝐴 = 𝑁))))
37	36	ancom2s 663	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} ↔ ((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) ∨ (𝑁 = 𝐵 ∧ 𝐴 = 𝑁))))
38		eqneqall 2972	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦))
39	38	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) → (𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦))
40		eqtr 2786	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 = 𝑁 ∧ 𝑁 = 𝐵) → 𝐴 = 𝐵)
41	40	ancoms 464	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 = 𝐵 ∧ 𝐴 = 𝑁) → 𝐴 = 𝐵)
42	41, 38	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 = 𝐵 ∧ 𝐴 = 𝑁) → (𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦))
43	39, 42	jaoi 871	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) ∨ (𝑁 = 𝐵 ∧ 𝐴 = 𝑁)) → (𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦))
44	43	adantld 496	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) ∨ (𝑁 = 𝐵 ∧ 𝐴 = 𝑁)) → ((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) → 𝑥 ≠ 𝑦))
45	37, 44	biimtrdi 256	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} → ((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) → 𝑥 ≠ 𝑦)))
46	45	com3l 90	. . . . . . . . . . . . . 14 ⊢ ({𝑁, 𝐴} = {𝑁, 𝐵} → ((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) → (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → 𝑥 ≠ 𝑦)))
47	46	impd 416	. . . . . . . . . . . . 13 ⊢ ({𝑁, 𝐴} = {𝑁, 𝐵} → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑥 ≠ 𝑦))
48	35, 47	sylbi 220	. . . . . . . . . . . 12 ⊢ ({𝑁, 𝐴} = {𝐵, 𝑁} → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑥 ≠ 𝑦))
49	33, 48	syl 18	. . . . . . . . . . 11 ⊢ (((𝐼‘𝑦) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑥 ≠ 𝑦))
50	32, 49	biimtrdi 256	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑥 ≠ 𝑦)))
51	50	impcomd 417	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑥 ≠ 𝑦))
52		ax-1 6	. . . . . . . . 9 ⊢ (𝑥 ≠ 𝑦 → ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑥 ≠ 𝑦))
53	51, 52	pm2.61ine 3044	. . . . . . . 8 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑥 ≠ 𝑦)
54		prid1g 4731	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ 𝑉 → 𝑁 ∈ {𝑁, 𝐴})
55	54	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → 𝑁 ∈ {𝑁, 𝐴})
56	55	adantl 487	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ {𝑁, 𝐴})
57		eleq2 2855	. . . . . . . . . . 11 ⊢ ((𝐼‘𝑥) = {𝑁, 𝐴} → (𝑁 ∈ (𝐼‘𝑥) ↔ 𝑁 ∈ {𝑁, 𝐴}))
58	56, 57	imbitrrid 249	. . . . . . . . . 10 ⊢ ((𝐼‘𝑥) = {𝑁, 𝐴} → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ (𝐼‘𝑥)))
59	58	adantr 486	. . . . . . . . 9 ⊢ (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ (𝐼‘𝑥)))
60	59	impcom 413	. . . . . . . 8 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑁 ∈ (𝐼‘𝑥))
61		prid2g 4732	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ 𝑉 → 𝑁 ∈ {𝐵, 𝑁})
62	61	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → 𝑁 ∈ {𝐵, 𝑁})
63	62	adantl 487	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ {𝐵, 𝑁})
64		eleq2 2855	. . . . . . . . . . 11 ⊢ ((𝐼‘𝑦) = {𝐵, 𝑁} → (𝑁 ∈ (𝐼‘𝑦) ↔ 𝑁 ∈ {𝐵, 𝑁}))
65	63, 64	imbitrrid 249	. . . . . . . . . 10 ⊢ ((𝐼‘𝑦) = {𝐵, 𝑁} → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ (𝐼‘𝑦)))
66	65	adantl 487	. . . . . . . . 9 ⊢ (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ (𝐼‘𝑦)))
67	66	impcom 413	. . . . . . . 8 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑁 ∈ (𝐼‘𝑦))
68	53, 60, 67	3jca 1146	. . . . . . 7 ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → (𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦)))
69	68	ex 418	. . . . . 6 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))))
70	69	reximdv 3183	. . . . 5 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (∃𝑦 ∈ dom 𝐼((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → ∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))))
71	70	reximdv 3183	. . . 4 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))))
72	30, 71	biimtrrid 246	. . 3 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → ((∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁}) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))))
73	29, 72	sylbid 243	. 2 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))))
74	8, 9, 73	sylc 66	1 ⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   ≠ wne 2961  ∃wrex 3092  {cpr 4596  dom cdm 5666  ran crn 5667   Fn wfn 6538  ‘cfv 6543  Vtxcvtx 29383  iEdgciedg 29384  Edgcedg 29434  UHGraphcuhgr 29443

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-edg 29435  df-uhgr 29445

This theorem is used by:  umgr2edg  29596