Theorem upgredgpr

Description: If a proper pair (of vertices) is a subset of an edge in a pseudograph, the pair is the edge. (Contributed by AV, 30-Dec-2020)

	Ref	Expression
Hypotheses	upgredg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	upgredg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	upgredgpr	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ) → { 𝐴 , 𝐵 } = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		upgredg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		upgredg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1 2	upgredg	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝑎 , 𝑏 } )
4	3	3adant3	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝑎 , 𝑏 } )
5		ssprsseq	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } ⊆ { 𝑎 , 𝑏 } ↔ { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
6	5	biimpd	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } ⊆ { 𝑎 , 𝑏 } → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
7		sseq2	⊢ ( 𝐶 = { 𝑎 , 𝑏 } → ( { 𝐴 , 𝐵 } ⊆ 𝐶 ↔ { 𝐴 , 𝐵 } ⊆ { 𝑎 , 𝑏 } ) )
8		eqeq2	⊢ ( 𝐶 = { 𝑎 , 𝑏 } → ( { 𝐴 , 𝐵 } = 𝐶 ↔ { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
9	7 8	imbi12d	⊢ ( 𝐶 = { 𝑎 , 𝑏 } → ( ( { 𝐴 , 𝐵 } ⊆ 𝐶 → { 𝐴 , 𝐵 } = 𝐶 ) ↔ ( { 𝐴 , 𝐵 } ⊆ { 𝑎 , 𝑏 } → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) ) )
10	6 9	imbitrrid	⊢ ( 𝐶 = { 𝑎 , 𝑏 } → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } ⊆ 𝐶 → { 𝐴 , 𝐵 } = 𝐶 ) ) )
11	10	com23	⊢ ( 𝐶 = { 𝑎 , 𝑏 } → ( { 𝐴 , 𝐵 } ⊆ 𝐶 → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) ) )
12	11	a1i	⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝐶 = { 𝑎 , 𝑏 } → ( { 𝐴 , 𝐵 } ⊆ 𝐶 → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) ) ) )
13	12	rexlimivv	⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝑎 , 𝑏 } → ( { 𝐴 , 𝐵 } ⊆ 𝐶 → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) ) )
14	13	com12	⊢ ( { 𝐴 , 𝐵 } ⊆ 𝐶 → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝑎 , 𝑏 } → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) ) )
15	14	3ad2ant3	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝐶 = { 𝑎 , 𝑏 } → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) ) )
16	4 15	mpd	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) )
17	16	imp	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ) → { 𝐴 , 𝐵 } = 𝐶 )