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 ∧ ( 𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑊 ) ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ) |