Theorem usgr1e

Description: A simple graph with one edge (with additional assumption that B =/= C since otherwise the edge is a loop!). (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 18-Oct-2020)

	Ref	Expression
Hypotheses	uspgr1e.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	uspgr1e.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
	uspgr1e.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	uspgr1e.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	uspgr1e.e	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
	usgr1e.e	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
Assertion	usgr1e	⊢ ( 𝜑 → 𝐺 ∈ USGraph )

Proof

Step	Hyp	Ref	Expression
1		uspgr1e.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		uspgr1e.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
3		uspgr1e.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4		uspgr1e.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5		uspgr1e.e	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
6		usgr1e.e	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
7	1 2 3 4 5	uspgr1e	⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
8		hashprg	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐵 ≠ 𝐶 ↔ ( ♯ ‘ { 𝐵 , 𝐶 } ) = 2 ) )
9	3 4 8	syl2anc	⊢ ( 𝜑 → ( 𝐵 ≠ 𝐶 ↔ ( ♯ ‘ { 𝐵 , 𝐶 } ) = 2 ) )
10	6 9	mpbid	⊢ ( 𝜑 → ( ♯ ‘ { 𝐵 , 𝐶 } ) = 2 )
11		prex	⊢ { 𝐵 , 𝐶 } ∈ V
12		fveqeq2	⊢ ( 𝑥 = { 𝐵 , 𝐶 } → ( ( ♯ ‘ 𝑥 ) = 2 ↔ ( ♯ ‘ { 𝐵 , 𝐶 } ) = 2 ) )
13	11 12	ralsn	⊢ ( ∀ 𝑥 ∈ { { 𝐵 , 𝐶 } } ( ♯ ‘ 𝑥 ) = 2 ↔ ( ♯ ‘ { 𝐵 , 𝐶 } ) = 2 )
14	10 13	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ { { 𝐵 , 𝐶 } } ( ♯ ‘ 𝑥 ) = 2 )
15		edgval	⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
16	15	a1i	⊢ ( 𝜑 → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
17	5	rneqd	⊢ ( 𝜑 → ran ( iEdg ‘ 𝐺 ) = ran { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
18		rnsnopg	⊢ ( 𝐴 ∈ 𝑋 → ran { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } = { { 𝐵 , 𝐶 } } )
19	2 18	syl	⊢ ( 𝜑 → ran { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } = { { 𝐵 , 𝐶 } } )
20	16 17 19	3eqtrd	⊢ ( 𝜑 → ( Edg ‘ 𝐺 ) = { { 𝐵 , 𝐶 } } )
21	20	raleqdv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑥 ) = 2 ↔ ∀ 𝑥 ∈ { { 𝐵 , 𝐶 } } ( ♯ ‘ 𝑥 ) = 2 ) )
22	14 21	mpbird	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑥 ) = 2 )
23		usgruspgrb	⊢ ( 𝐺 ∈ USGraph ↔ ( 𝐺 ∈ USPGraph ∧ ∀ 𝑥 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑥 ) = 2 ) )
24	7 22 23	sylanbrc	⊢ ( 𝜑 → 𝐺 ∈ USGraph )