1egrvtxdg1

Description: The vertex degree of a one-edge graph, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 22-Dec-2017) (Revised by AV, 21-Feb-2021)

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

Proof

Step	Hyp	Ref	Expression
1		1egrvtxdg1.v	⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
2		1egrvtxdg1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
3		1egrvtxdg1.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4		1egrvtxdg1.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5		1egrvtxdg1.n	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
6		1egrvtxdg1.i	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
7		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
8	3 1	eleqtrrd	⊢ ( 𝜑 → 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
9	4 1	eleqtrrd	⊢ ( 𝜑 → 𝐶 ∈ ( Vtx ‘ 𝐺 ) )
10	7 2 8 9 6 5	usgr1e	⊢ ( 𝜑 → 𝐺 ∈ USGraph )
11		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
12		eqid	⊢ dom ( iEdg ‘ 𝐺 ) = dom ( iEdg ‘ 𝐺 )
13		eqid	⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
14	7 11 12 13	vtxdusgrval	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐵 ) = ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝐵 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
15	10 8 14	syl2anc	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐵 ) = ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝐵 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
16		dmeq	⊢ ( ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } → dom ( iEdg ‘ 𝐺 ) = dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
17	16	adantl	⊢ ( ( 𝜑 ∧ ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → dom ( iEdg ‘ 𝐺 ) = dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
18		prex	⊢ { 𝐵 , 𝐶 } ∈ V
19		dmsnopg	⊢ ( { 𝐵 , 𝐶 } ∈ V → dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } = { 𝐴 } )
20	18 19	mp1i	⊢ ( ( 𝜑 ∧ ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } = { 𝐴 } )
21	17 20	eqtrd	⊢ ( ( 𝜑 ∧ ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → dom ( iEdg ‘ 𝐺 ) = { 𝐴 } )
22		fveq1	⊢ ( ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) )
23	22	eleq2d	⊢ ( ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } → ( 𝐵 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) ) )
24	23	adantl	⊢ ( ( 𝜑 ∧ ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → ( 𝐵 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) ) )
25	21 24	rabeqbidv	⊢ ( ( 𝜑 ∧ ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝐵 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } = { 𝑥 ∈ { 𝐴 } ∣ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) } )
26	25	fveq2d	⊢ ( ( 𝜑 ∧ ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝐵 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) = ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) } ) )
27		fveq2	⊢ ( 𝑥 = 𝐴 → ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) = ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝐴 ) )
28	27	eleq2d	⊢ ( 𝑥 = 𝐴 → ( 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) ↔ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝐴 ) ) )
29	28	rabsnif	⊢ { 𝑥 ∈ { 𝐴 } ∣ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) } = if ( 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝐴 ) , { 𝐴 } , ∅ )
30		prid1g	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ { 𝐵 , 𝐶 } )
31	3 30	syl	⊢ ( 𝜑 → 𝐵 ∈ { 𝐵 , 𝐶 } )
32		fvsng	⊢ ( ( 𝐴 ∈ 𝑋 ∧ { 𝐵 , 𝐶 } ∈ V ) → ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝐴 ) = { 𝐵 , 𝐶 } )
33	2 18 32	sylancl	⊢ ( 𝜑 → ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝐴 ) = { 𝐵 , 𝐶 } )
34	31 33	eleqtrrd	⊢ ( 𝜑 → 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝐴 ) )
35	34	iftrued	⊢ ( 𝜑 → if ( 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝐴 ) , { 𝐴 } , ∅ ) = { 𝐴 } )
36	29 35	eqtrid	⊢ ( 𝜑 → { 𝑥 ∈ { 𝐴 } ∣ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) } = { 𝐴 } )
37	36	fveq2d	⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) } ) = ( ♯ ‘ { 𝐴 } ) )
38		hashsng	⊢ ( 𝐴 ∈ 𝑋 → ( ♯ ‘ { 𝐴 } ) = 1 )
39	2 38	syl	⊢ ( 𝜑 → ( ♯ ‘ { 𝐴 } ) = 1 )
40	37 39	eqtrd	⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) } ) = 1 )
41	40	adantr	⊢ ( ( 𝜑 ∧ ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) } ) = 1 )
42	26 41	eqtrd	⊢ ( ( 𝜑 ∧ ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝐵 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 1 )
43	6 42	mpdan	⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝐵 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 1 )
44	15 43	eqtrd	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐵 ) = 1 )

Metamath Proof Explorer

Theorem 1egrvtxdg1

Proof