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 )