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

Metamath Proof Explorer

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 ∧ 𝐶 ∈ 𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ) → { 𝐴 , 𝐵 } = 𝐶 )