Metamath Proof Explorer

Theorem upgrpredgv

Description: An edge of a pseudograph always connects two vertices if the edge contains two sets. The two vertices/sets need not necessarily be different (loops are allowed). (Contributed by AV, 18-Nov-2021)

Ref Expression
Hypotheses upgredg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
upgredg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion upgrpredgv ( ( 𝐺 ∈ UPGraph ∧ ( 𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑊 ) ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 upgredg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 upgredg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 upgredg ⊢ ( ( 𝐺 ∈ UPGraph ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ∃ 𝑚 ∈ 𝑉 ∃ 𝑛 ∈ 𝑉 { 𝑀 , 𝑁 } = { 𝑚 , 𝑛 } )
4 3 3adant2 ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑊 ) ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ∃ 𝑚 ∈ 𝑉 ∃ 𝑛 ∈ 𝑉 { 𝑀 , 𝑁 } = { 𝑚 , 𝑛 } )
5 preq12bg ⊢ ( ( ( 𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( { 𝑀 , 𝑁 } = { 𝑚 , 𝑛 } ↔ ( ( 𝑀 = 𝑚 ∧ 𝑁 = 𝑛 ) ∨ ( 𝑀 = 𝑛 ∧ 𝑁 = 𝑚 ) ) ) )
6 5 3ad2antl2 ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑊 ) ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( { 𝑀 , 𝑁 } = { 𝑚 , 𝑛 } ↔ ( ( 𝑀 = 𝑚 ∧ 𝑁 = 𝑛 ) ∨ ( 𝑀 = 𝑛 ∧ 𝑁 = 𝑚 ) ) ) )
7 eleq1 ⊢ ( 𝑚 = 𝑀 → ( 𝑚 ∈ 𝑉 ↔ 𝑀 ∈ 𝑉 ) )
8 7 eqcoms ⊢ ( 𝑀 = 𝑚 → ( 𝑚 ∈ 𝑉 ↔ 𝑀 ∈ 𝑉 ) )
9 8 biimpd ⊢ ( 𝑀 = 𝑚 → ( 𝑚 ∈ 𝑉 → 𝑀 ∈ 𝑉 ) )
10 eleq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 ∈ 𝑉 ↔ 𝑁 ∈ 𝑉 ) )
11 10 eqcoms ⊢ ( 𝑁 = 𝑛 → ( 𝑛 ∈ 𝑉 ↔ 𝑁 ∈ 𝑉 ) )
12 11 biimpd ⊢ ( 𝑁 = 𝑛 → ( 𝑛 ∈ 𝑉 → 𝑁 ∈ 𝑉 ) )
13 9 12 im2anan9 ⊢ ( ( 𝑀 = 𝑚 ∧ 𝑁 = 𝑛 ) → ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
14 13 com12 ⊢ ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( ( 𝑀 = 𝑚 ∧ 𝑁 = 𝑛 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
15 eleq1 ⊢ ( 𝑛 = 𝑀 → ( 𝑛 ∈ 𝑉 ↔ 𝑀 ∈ 𝑉 ) )
16 15 eqcoms ⊢ ( 𝑀 = 𝑛 → ( 𝑛 ∈ 𝑉 ↔ 𝑀 ∈ 𝑉 ) )
17 16 biimpd ⊢ ( 𝑀 = 𝑛 → ( 𝑛 ∈ 𝑉 → 𝑀 ∈ 𝑉 ) )
18 eleq1 ⊢ ( 𝑚 = 𝑁 → ( 𝑚 ∈ 𝑉 ↔ 𝑁 ∈ 𝑉 ) )
19 18 eqcoms ⊢ ( 𝑁 = 𝑚 → ( 𝑚 ∈ 𝑉 ↔ 𝑁 ∈ 𝑉 ) )
20 19 biimpd ⊢ ( 𝑁 = 𝑚 → ( 𝑚 ∈ 𝑉 → 𝑁 ∈ 𝑉 ) )
21 17 20 im2anan9 ⊢ ( ( 𝑀 = 𝑛 ∧ 𝑁 = 𝑚 ) → ( ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
22 21 com12 ⊢ ( ( 𝑛 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ) → ( ( 𝑀 = 𝑛 ∧ 𝑁 = 𝑚 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
23 22 ancoms ⊢ ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( ( 𝑀 = 𝑛 ∧ 𝑁 = 𝑚 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
24 14 23 jaod ⊢ ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( ( ( 𝑀 = 𝑚 ∧ 𝑁 = 𝑛 ) ∨ ( 𝑀 = 𝑛 ∧ 𝑁 = 𝑚 ) ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
25 24 adantl ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑊 ) ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( ( ( 𝑀 = 𝑚 ∧ 𝑁 = 𝑛 ) ∨ ( 𝑀 = 𝑛 ∧ 𝑁 = 𝑚 ) ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
26 6 25 sylbid ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑊 ) ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( { 𝑀 , 𝑁 } = { 𝑚 , 𝑛 } → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
27 26 rexlimdvva ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑊 ) ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ( ∃ 𝑚 ∈ 𝑉 ∃ 𝑛 ∈ 𝑉 { 𝑀 , 𝑁 } = { 𝑚 , 𝑛 } → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) )
28 4 27 mpd ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑊 ) ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )