Theorem uspgr1e

Description: A simple pseudograph with one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020) (Revised by AV, 21-Mar-2021) (Proof shortened by AV, 17-Apr-2021)

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

Proof

Step	Hyp	Ref	Expression
1		uspgr1e.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		uspgr1e.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
3		uspgr1e.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4		uspgr1e.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5		uspgr1e.e	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
6		prex	⊢ { 𝐵 , 𝐶 } ∈ V
7	6	snid	⊢ { 𝐵 , 𝐶 } ∈ { { 𝐵 , 𝐶 } }
8		f1sng	⊢ ( ( 𝐴 ∈ 𝑋 ∧ { 𝐵 , 𝐶 } ∈ { { 𝐵 , 𝐶 } } ) → { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : { 𝐴 } –1-1→ { { 𝐵 , 𝐶 } } )
9	2 7 8	sylancl	⊢ ( 𝜑 → { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : { 𝐴 } –1-1→ { { 𝐵 , 𝐶 } } )
10	3 4	prssd	⊢ ( 𝜑 → { 𝐵 , 𝐶 } ⊆ 𝑉 )
11	10 1	sseqtrdi	⊢ ( 𝜑 → { 𝐵 , 𝐶 } ⊆ ( Vtx ‘ 𝐺 ) )
12	6	elpw	⊢ ( { 𝐵 , 𝐶 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) ↔ { 𝐵 , 𝐶 } ⊆ ( Vtx ‘ 𝐺 ) )
13	11 12	sylibr	⊢ ( 𝜑 → { 𝐵 , 𝐶 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) )
14	13 3	upgr1elem	⊢ ( 𝜑 → { { 𝐵 , 𝐶 } } ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
15		f1ss	⊢ ( ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : { 𝐴 } –1-1→ { { 𝐵 , 𝐶 } } ∧ { { 𝐵 , 𝐶 } } ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) → { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : { 𝐴 } –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
16	9 14 15	syl2anc	⊢ ( 𝜑 → { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : { 𝐴 } –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
17	6	a1i	⊢ ( 𝜑 → { 𝐵 , 𝐶 } ∈ V )
18	17 3	upgr1elem	⊢ ( 𝜑 → { { 𝐵 , 𝐶 } } ⊆ { 𝑥 ∈ ( V ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
19		f1ss	⊢ ( ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : { 𝐴 } –1-1→ { { 𝐵 , 𝐶 } } ∧ { { 𝐵 , 𝐶 } } ⊆ { 𝑥 ∈ ( V ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) → { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : { 𝐴 } –1-1→ { 𝑥 ∈ ( V ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
20	9 18 19	syl2anc	⊢ ( 𝜑 → { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : { 𝐴 } –1-1→ { 𝑥 ∈ ( V ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
21		f1dm	⊢ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : { 𝐴 } –1-1→ { 𝑥 ∈ ( V ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } = { 𝐴 } )
22		f1eq2	⊢ ( dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } = { 𝐴 } → ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ↔ { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : { 𝐴 } –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
23	20 21 22	3syl	⊢ ( 𝜑 → ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ↔ { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : { 𝐴 } –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
24	16 23	mpbird	⊢ ( 𝜑 → { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
25	5	dmeqd	⊢ ( 𝜑 → dom ( iEdg ‘ 𝐺 ) = dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
26		eqidd	⊢ ( 𝜑 → { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } = { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
27	5 25 26	f1eq123d	⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ↔ { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
28	24 27	mpbird	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
29	1	1vgrex	⊢ ( 𝐵 ∈ 𝑉 → 𝐺 ∈ V )
30		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
31		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
32	30 31	isuspgr	⊢ ( 𝐺 ∈ V → ( 𝐺 ∈ USPGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
33	3 29 32	3syl	⊢ ( 𝜑 → ( 𝐺 ∈ USPGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
34	28 33	mpbird	⊢ ( 𝜑 → 𝐺 ∈ USPGraph )