This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem upgr1eopALT

Description: Alternate proof of upgr1eop , using the general theorem gropeld to transform a theorem for an arbitrary representation of a graph into a theorem for a graph represented as ordered pair. This general approach causes some overhead, which makes the proof longer than necessary (see proof of upgr1eop ). (Contributed by AV, 11-Oct-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion upgr1eopALT ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ∈ UPGraph )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝑔 )
2 simpllr ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) ) → 𝐴 ∈ 𝑋 )
3 simplrl ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) ) → 𝐵 ∈ 𝑉 )
4 eleq2 ⊢ ( ( Vtx ‘ 𝑔 ) = 𝑉 → ( 𝐵 ∈ ( Vtx ‘ 𝑔 ) ↔ 𝐵 ∈ 𝑉 ) )
5 4 ad2antrl ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) ) → ( 𝐵 ∈ ( Vtx ‘ 𝑔 ) ↔ 𝐵 ∈ 𝑉 ) )
6 3 5 mpbird ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) ) → 𝐵 ∈ ( Vtx ‘ 𝑔 ) )
7 simplrr ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) ) → 𝐶 ∈ 𝑉 )
8 eleq2 ⊢ ( ( Vtx ‘ 𝑔 ) = 𝑉 → ( 𝐶 ∈ ( Vtx ‘ 𝑔 ) ↔ 𝐶 ∈ 𝑉 ) )
9 8 ad2antrl ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) ) → ( 𝐶 ∈ ( Vtx ‘ 𝑔 ) ↔ 𝐶 ∈ 𝑉 ) )
10 7 9 mpbird ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) ) → 𝐶 ∈ ( Vtx ‘ 𝑔 ) )
11 simprr ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) ) → ( iEdg ‘ 𝑔 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
12 1 2 6 10 11 upgr1e ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) ) → 𝑔 ∈ UPGraph )
13 12 ex ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → 𝑔 ∈ UPGraph ) )
14 13 alrimiv ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → 𝑔 ∈ UPGraph ) )
15 simpll ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝑉 ∈ 𝑊 )
16 snex ⊢ { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ∈ V
17 16 a1i ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ∈ V )
18 14 15 17 gropeld ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ⟨ 𝑉 , { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ⟩ ∈ UPGraph )