Metamath Proof Explorer

Theorem usgr1eop

Description: A simple graph with (at least) two different vertices and one edge. If the two vertices were not different, the edge would be a loop. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 18-Oct-2020)

Ref Expression
Assertion usgr1eop ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐵 ≠ 𝐶 → ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ∈ USGraph ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ) = ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ )
2 simpllr ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝐵 ≠ 𝐶 ) → 𝐴 ∈ 𝑋 )
3 simplrl ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝐵 ≠ 𝐶 ) → 𝐵 ∈ 𝑉 )
4 simpl ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) → 𝑉 ∈ 𝑊 )
5 4 adantr ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝑉 ∈ 𝑊 )
6 snex ⊢ { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ∈ V
7 6 a1i ⊢ ( 𝐵 ≠ 𝐶 → { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ∈ V )
8 opvtxfv ⊢ ( ( 𝑉 ∈ 𝑊 ∧ { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ) = 𝑉 )
9 5 7 8 syl2an ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝐵 ≠ 𝐶 ) → ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ) = 𝑉 )
10 3 9 eleqtrrd ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝐵 ≠ 𝐶 ) → 𝐵 ∈ ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ) )
11 simprr ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ∈ 𝑉 )
12 6 a1i ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ∈ V )
13 4 12 8 syl2an ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ) = 𝑉 )
14 11 13 eleqtrrd ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ∈ ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ) )
15 14 adantr ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝐵 ≠ 𝐶 ) → 𝐶 ∈ ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ) )
16 opiedgfv ⊢ ( ( 𝑉 ∈ 𝑊 ∧ { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
17 5 7 16 syl2an ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝐵 ≠ 𝐶 ) → ( iEdg ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
18 simpr ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝐵 ≠ 𝐶 ) → 𝐵 ≠ 𝐶 )
19 1 2 10 15 17 18 usgr1e ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝐵 ≠ 𝐶 ) → ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ∈ USGraph )
20 19 ex ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐵 ≠ 𝐶 → ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ∈ USGraph ) )