Metamath Proof Explorer


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 )