1egrvtxdg0 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 1egrvtxdg0		Structured version Visualization version GIF version

Theorem 1egrvtxdg0 29277

Description: The vertex degree of a one-edge graph, case 1: an edge between two vertices other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.)

**Hypotheses**
Ref	Expression
1egrvtxdg1.v	⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)
1egrvtxdg1.a	⊢ (𝜑 → 𝐴 ∈ 𝑋)
1egrvtxdg1.b	⊢ (𝜑 → 𝐵 ∈ 𝑉)
1egrvtxdg1.c	⊢ (𝜑 → 𝐶 ∈ 𝑉)
1egrvtxdg1.n	⊢ (𝜑 → 𝐵 ≠ 𝐶)
1egrvtxdg0.d	⊢ (𝜑 → 𝐷 ∈ 𝑉)
1egrvtxdg0.n	⊢ (𝜑 → 𝐶 ≠ 𝐷)
1egrvtxdg0.i	⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝐵, 𝐷}⟩})

**Assertion**
Ref	Expression
1egrvtxdg0	⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐶) = 0)

Proof of Theorem 1egrvtxdg0 Dummy variable 𝑒 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		1egrvtxdg1.v	. . . . 5 ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)
2	1	adantl 481	. . . 4 ⊢ ((𝐵 = 𝐷 ∧ 𝜑) → (Vtx‘𝐺) = 𝑉)
3		1egrvtxdg1.a	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
4	3	adantl 481	. . . 4 ⊢ ((𝐵 = 𝐷 ∧ 𝜑) → 𝐴 ∈ 𝑋)
5		1egrvtxdg1.b	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑉)
6	5	adantl 481	. . . 4 ⊢ ((𝐵 = 𝐷 ∧ 𝜑) → 𝐵 ∈ 𝑉)
7		1egrvtxdg0.i	. . . . . 6 ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝐵, 𝐷}⟩})
8	7	adantl 481	. . . . 5 ⊢ ((𝐵 = 𝐷 ∧ 𝜑) → (iEdg‘𝐺) = {⟨𝐴, {𝐵, 𝐷}⟩})
9		preq2 4733	. . . . . . . . . 10 ⊢ (𝐷 = 𝐵 → {𝐵, 𝐷} = {𝐵, 𝐵})
10	9	eqcoms 2734	. . . . . . . . 9 ⊢ (𝐵 = 𝐷 → {𝐵, 𝐷} = {𝐵, 𝐵})
11		dfsn2 4636	. . . . . . . . 9 ⊢ {𝐵} = {𝐵, 𝐵}
12	10, 11	eqtr4di 2784	. . . . . . . 8 ⊢ (𝐵 = 𝐷 → {𝐵, 𝐷} = {𝐵})
13	12	adantr 480	. . . . . . 7 ⊢ ((𝐵 = 𝐷 ∧ 𝜑) → {𝐵, 𝐷} = {𝐵})
14	13	opeq2d 4875	. . . . . 6 ⊢ ((𝐵 = 𝐷 ∧ 𝜑) → ⟨𝐴, {𝐵, 𝐷}⟩ = ⟨𝐴, {𝐵}⟩)
15	14	sneqd 4635	. . . . 5 ⊢ ((𝐵 = 𝐷 ∧ 𝜑) → {⟨𝐴, {𝐵, 𝐷}⟩} = {⟨𝐴, {𝐵}⟩})
16	8, 15	eqtrd 2766	. . . 4 ⊢ ((𝐵 = 𝐷 ∧ 𝜑) → (iEdg‘𝐺) = {⟨𝐴, {𝐵}⟩})
17		1egrvtxdg1.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
18		1egrvtxdg1.n	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
19	18	necomd 2990	. . . . . . 7 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
20	17, 19	jca 511	. . . . . 6 ⊢ (𝜑 → (𝐶 ∈ 𝑉 ∧ 𝐶 ≠ 𝐵))
21		eldifsn 4785	. . . . . 6 ⊢ (𝐶 ∈ (𝑉 ∖ {𝐵}) ↔ (𝐶 ∈ 𝑉 ∧ 𝐶 ≠ 𝐵))
22	20, 21	sylibr 233	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ (𝑉 ∖ {𝐵}))
23	22	adantl 481	. . . 4 ⊢ ((𝐵 = 𝐷 ∧ 𝜑) → 𝐶 ∈ (𝑉 ∖ {𝐵}))
24	2, 4, 6, 16, 23	1loopgrvd0 29270	. . 3 ⊢ ((𝐵 = 𝐷 ∧ 𝜑) → ((VtxDeg‘𝐺)‘𝐶) = 0)
25	24	ex 412	. 2 ⊢ (𝐵 = 𝐷 → (𝜑 → ((VtxDeg‘𝐺)‘𝐶) = 0))
26		necom 2988	. . . . . . . . . 10 ⊢ (𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵)
27		df-ne 2935	. . . . . . . . . 10 ⊢ (𝐶 ≠ 𝐵 ↔ ¬ 𝐶 = 𝐵)
28	26, 27	sylbb 218	. . . . . . . . 9 ⊢ (𝐵 ≠ 𝐶 → ¬ 𝐶 = 𝐵)
29	18, 28	syl 17	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝐶 = 𝐵)
30		1egrvtxdg0.n	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ≠ 𝐷)
31	30	neneqd 2939	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝐶 = 𝐷)
32	29, 31	jca 511	. . . . . . 7 ⊢ (𝜑 → (¬ 𝐶 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
33	32	adantl 481	. . . . . 6 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝜑) → (¬ 𝐶 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
34		ioran 980	. . . . . 6 ⊢ (¬ (𝐶 = 𝐵 ∨ 𝐶 = 𝐷) ↔ (¬ 𝐶 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
35	33, 34	sylibr 233	. . . . 5 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝜑) → ¬ (𝐶 = 𝐵 ∨ 𝐶 = 𝐷))
36		edgval 28817	. . . . . . . . 9 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
37	7	rneqd 5931	. . . . . . . . . 10 ⊢ (𝜑 → ran (iEdg‘𝐺) = ran {⟨𝐴, {𝐵, 𝐷}⟩})
38		rnsnopg 6214	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑋 → ran {⟨𝐴, {𝐵, 𝐷}⟩} = {{𝐵, 𝐷}})
39	3, 38	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ran {⟨𝐴, {𝐵, 𝐷}⟩} = {{𝐵, 𝐷}})
40	37, 39	eqtrd 2766	. . . . . . . . 9 ⊢ (𝜑 → ran (iEdg‘𝐺) = {{𝐵, 𝐷}})
41	36, 40	eqtrid 2778	. . . . . . . 8 ⊢ (𝜑 → (Edg‘𝐺) = {{𝐵, 𝐷}})
42	41	adantl 481	. . . . . . 7 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝜑) → (Edg‘𝐺) = {{𝐵, 𝐷}})
43	42	rexeqdv 3320	. . . . . 6 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝜑) → (∃𝑒 ∈ (Edg‘𝐺)𝐶 ∈ 𝑒 ↔ ∃𝑒 ∈ {{𝐵, 𝐷}}𝐶 ∈ 𝑒))
44		prex 5425	. . . . . . 7 ⊢ {𝐵, 𝐷} ∈ V
45		eleq2 2816	. . . . . . . 8 ⊢ (𝑒 = {𝐵, 𝐷} → (𝐶 ∈ 𝑒 ↔ 𝐶 ∈ {𝐵, 𝐷}))
46	45	rexsng 4673	. . . . . . 7 ⊢ ({𝐵, 𝐷} ∈ V → (∃𝑒 ∈ {{𝐵, 𝐷}}𝐶 ∈ 𝑒 ↔ 𝐶 ∈ {𝐵, 𝐷}))
47	44, 46	mp1i 13	. . . . . 6 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝜑) → (∃𝑒 ∈ {{𝐵, 𝐷}}𝐶 ∈ 𝑒 ↔ 𝐶 ∈ {𝐵, 𝐷}))
48		elprg 4644	. . . . . . . 8 ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ {𝐵, 𝐷} ↔ (𝐶 = 𝐵 ∨ 𝐶 = 𝐷)))
49	17, 48	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐶 ∈ {𝐵, 𝐷} ↔ (𝐶 = 𝐵 ∨ 𝐶 = 𝐷)))
50	49	adantl 481	. . . . . 6 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝜑) → (𝐶 ∈ {𝐵, 𝐷} ↔ (𝐶 = 𝐵 ∨ 𝐶 = 𝐷)))
51	43, 47, 50	3bitrd 305	. . . . 5 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝜑) → (∃𝑒 ∈ (Edg‘𝐺)𝐶 ∈ 𝑒 ↔ (𝐶 = 𝐵 ∨ 𝐶 = 𝐷)))
52	35, 51	mtbird 325	. . . 4 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝜑) → ¬ ∃𝑒 ∈ (Edg‘𝐺)𝐶 ∈ 𝑒)
53		eqid 2726	. . . . . 6 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
54	3	adantl 481	. . . . . 6 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝜑) → 𝐴 ∈ 𝑋)
55	5, 1	eleqtrrd 2830	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ (Vtx‘𝐺))
56	55	adantl 481	. . . . . 6 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝜑) → 𝐵 ∈ (Vtx‘𝐺))
57		1egrvtxdg0.d	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ 𝑉)
58	57, 1	eleqtrrd 2830	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ (Vtx‘𝐺))
59	58	adantl 481	. . . . . 6 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝜑) → 𝐷 ∈ (Vtx‘𝐺))
60	7	adantl 481	. . . . . 6 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝜑) → (iEdg‘𝐺) = {⟨𝐴, {𝐵, 𝐷}⟩})
61		simpl 482	. . . . . 6 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝜑) → 𝐵 ≠ 𝐷)
62	53, 54, 56, 59, 60, 61	usgr1e 29010	. . . . 5 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝜑) → 𝐺 ∈ USGraph)
63	17, 1	eleqtrrd 2830	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ (Vtx‘𝐺))
64	63	adantl 481	. . . . 5 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝜑) → 𝐶 ∈ (Vtx‘𝐺))
65		eqid 2726	. . . . . 6 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
66		eqid 2726	. . . . . 6 ⊢ (VtxDeg‘𝐺) = (VtxDeg‘𝐺)
67	53, 65, 66	vtxdusgr0edgnel 29261	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ 𝐶 ∈ (Vtx‘𝐺)) → (((VtxDeg‘𝐺)‘𝐶) = 0 ↔ ¬ ∃𝑒 ∈ (Edg‘𝐺)𝐶 ∈ 𝑒))
68	62, 64, 67	syl2anc 583	. . . 4 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝜑) → (((VtxDeg‘𝐺)‘𝐶) = 0 ↔ ¬ ∃𝑒 ∈ (Edg‘𝐺)𝐶 ∈ 𝑒))
69	52, 68	mpbird 257	. . 3 ⊢ ((𝐵 ≠ 𝐷 ∧ 𝜑) → ((VtxDeg‘𝐺)‘𝐶) = 0)
70	69	ex 412	. 2 ⊢ (𝐵 ≠ 𝐷 → (𝜑 → ((VtxDeg‘𝐺)‘𝐶) = 0))
71	25, 70	pm2.61ine 3019	1 ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐶) = 0)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 844 = wceq 1533 ∈ wcel 2098 ≠ wne 2934 ∃wrex 3064 Vcvv 3468 ∖ cdif 3940 {csn 4623 {cpr 4625 ⟨cop 4629 ran crn 5670 ‘cfv 6537 0cc0 11112 Vtxcvtx 28764 iEdgciedg 28765 Edgcedg 28815 USGraphcusgr 28917 VtxDegcvtxdg 29231

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2697 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7722 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-nel 3041 df-ral 3056 df-rex 3065 df-reu 3371 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-pss 3962 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-int 4944 df-iun 4992 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6294 df-ord 6361 df-on 6362 df-lim 6363 df-suc 6364 df-iota 6489 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7853 df-1st 7974 df-2nd 7975 df-frecs 8267 df-wrecs 8298 df-recs 8372 df-rdg 8411 df-1o 8467 df-oadd 8471 df-er 8705 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-dju 9898 df-card 9936 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-nn 12217 df-2 12279 df-n0 12477 df-xnn0 12549 df-z 12563 df-uz 12827 df-xadd 13099 df-fz 13491 df-hash 14296 df-edg 28816 df-uhgr 28826 df-upgr 28850 df-uspgr 28918 df-usgr 28919 df-vtxdg 29232

This theorem is referenced by: (None)

W3C validator