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 ⊢ V = Vtx ⁡ G
upgredg.e ⊢ E = Edg ⁡ G
Assertion upgrpredgv ⊢ G ∈ UPGraph ∧ M ∈ U ∧ N ∈ W ∧ M N ∈ E → M ∈ V ∧ N ∈ V

Proof

Step Hyp Ref Expression
1 upgredg.v ⊢ V = Vtx ⁡ G
2 upgredg.e ⊢ E = Edg ⁡ G
3 1 2 upgredg ⊢ G ∈ UPGraph ∧ M N ∈ E → ∃ m ∈ V ∃ n ∈ V M N = m n
4 3 3adant2 ⊢ G ∈ UPGraph ∧ M ∈ U ∧ N ∈ W ∧ M N ∈ E → ∃ m ∈ V ∃ n ∈ V M N = m n
5 preq12bg ⊢ M ∈ U ∧ N ∈ W ∧ m ∈ V ∧ n ∈ V → M N = m n ↔ M = m ∧ N = n ∨ M = n ∧ N = m
6 5 3ad2antl2 ⊢ G ∈ UPGraph ∧ M ∈ U ∧ N ∈ W ∧ M N ∈ E ∧ m ∈ V ∧ n ∈ V → M N = m n ↔ M = m ∧ N = n ∨ M = n ∧ N = m
7 eleq1 ⊢ m = M → m ∈ V ↔ M ∈ V
8 7 eqcoms ⊢ M = m → m ∈ V ↔ M ∈ V
9 8 biimpd ⊢ M = m → m ∈ V → M ∈ V
10 eleq1 ⊢ n = N → n ∈ V ↔ N ∈ V
11 10 eqcoms ⊢ N = n → n ∈ V ↔ N ∈ V
12 11 biimpd ⊢ N = n → n ∈ V → N ∈ V
13 9 12 im2anan9 ⊢ M = m ∧ N = n → m ∈ V ∧ n ∈ V → M ∈ V ∧ N ∈ V
14 13 com12 ⊢ m ∈ V ∧ n ∈ V → M = m ∧ N = n → M ∈ V ∧ N ∈ V
15 eleq1 ⊢ n = M → n ∈ V ↔ M ∈ V
16 15 eqcoms ⊢ M = n → n ∈ V ↔ M ∈ V
17 16 biimpd ⊢ M = n → n ∈ V → M ∈ V
18 eleq1 ⊢ m = N → m ∈ V ↔ N ∈ V
19 18 eqcoms ⊢ N = m → m ∈ V ↔ N ∈ V
20 19 biimpd ⊢ N = m → m ∈ V → N ∈ V
21 17 20 im2anan9 ⊢ M = n ∧ N = m → n ∈ V ∧ m ∈ V → M ∈ V ∧ N ∈ V
22 21 com12 ⊢ n ∈ V ∧ m ∈ V → M = n ∧ N = m → M ∈ V ∧ N ∈ V
23 22 ancoms ⊢ m ∈ V ∧ n ∈ V → M = n ∧ N = m → M ∈ V ∧ N ∈ V
24 14 23 jaod ⊢ m ∈ V ∧ n ∈ V → M = m ∧ N = n ∨ M = n ∧ N = m → M ∈ V ∧ N ∈ V
25 24 adantl ⊢ G ∈ UPGraph ∧ M ∈ U ∧ N ∈ W ∧ M N ∈ E ∧ m ∈ V ∧ n ∈ V → M = m ∧ N = n ∨ M = n ∧ N = m → M ∈ V ∧ N ∈ V
26 6 25 sylbid ⊢ G ∈ UPGraph ∧ M ∈ U ∧ N ∈ W ∧ M N ∈ E ∧ m ∈ V ∧ n ∈ V → M N = m n → M ∈ V ∧ N ∈ V
27 26 rexlimdvva ⊢ G ∈ UPGraph ∧ M ∈ U ∧ N ∈ W ∧ M N ∈ E → ∃ m ∈ V ∃ n ∈ V M N = m n → M ∈ V ∧ N ∈ V
28 4 27 mpd ⊢ G ∈ UPGraph ∧ M ∈ U ∧ N ∈ W ∧ M N ∈ E → M ∈ V ∧ N ∈ V