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 )