Metamath Proof Explorer

Theorem upgr1e

Description: A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1e . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 16-Oct-2020) (Revised by AV, 21-Mar-2021) (Proof shortened by AV, 17-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 upgr1e.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 upgr1e.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
3 upgr1e.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4 upgr1e.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5 upgr1e.e ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
6 prex ⊢ { 𝐵 , 𝐶 } ∈ V
7 6 snid ⊢ { 𝐵 , 𝐶 } ∈ { { 𝐵 , 𝐶 } }
8 7 a1i ⊢ ( 𝜑 → { 𝐵 , 𝐶 } ∈ { { 𝐵 , 𝐶 } } )
9 2 8 fsnd ⊢ ( 𝜑 → { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : { 𝐴 } ⟶ { { 𝐵 , 𝐶 } } )
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 9 14 fssd ⊢ ( 𝜑 → { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : { 𝐴 } ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
16 15 ffdmd ⊢ ( 𝜑 → { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
17 5 dmeqd ⊢ ( 𝜑 → dom ( iEdg ‘ 𝐺 ) = dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
18 5 17 feq12d ⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ↔ { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } : dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
19 16 18 mpbird ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
20 1 1vgrex ⊢ ( 𝐵 ∈ 𝑉 → 𝐺 ∈ V )
21 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
22 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
23 21 22 isupgr ⊢ ( 𝐺 ∈ V → ( 𝐺 ∈ UPGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
24 3 20 23 3syl ⊢ ( 𝜑 → ( 𝐺 ∈ UPGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
25 19 24 mpbird ⊢ ( 𝜑 → 𝐺 ∈ UPGraph )